[opentheory-users] Scalable LCF-style proof translation

[Ramana Kumar]

So, the first observation is a difference in the article formats:

Currently, OpenTheory articles are programs for a virtual stack machine.
Stack objects may live inside the dictionary and be referenced (by an
explicit ref command) by integer keys, or they can be used directly without
going into the dictionary.

By contrast, K&K articles are programs for a virtual machines without a
stack.
The arguments to commands are given inline with the commands, and are
always integer keys (i.e., every object is in the dictionary) or literal
names.

This simplifies and shortens the article format and processing. There are
fewer kinds of object (just terms, types, theorems, and names; whereas
OpenTheory also requires numbers and lists) and no stack manipulation
commands.

(Also, I suspect K&K constants are identical if they have the same name;
they aren't generative (identity depends on construction provenance) as in
OT. This is more intuitive to my taste.)

Is there a good reason for the stack-based approach? I couldn't think of
any, but maybe I'm missing something.
One thing the stack gives you is the ability to share sub-objects like
lists of terms; but I don't think this is worthwhile. (With K&K you of
course can still share the main objects (terms,types,thms).)


On Tue, Jul 23, 2013 at 11:37 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk>wrote:

> Cezary Kaliszyk and Alexander Krauss have done a lovely piece of work that
> was just presented at ITP 2013 (
> http://cl-informatik.uibk.ac.at/users/cek/docs/kaliszyk-itp13.pdf) about
> efficient import from HOL Light into Isabelle/HOL.
>
> Their approach has many similarities to OpenTheory, and their proof trace
> format is not too different from OpenTheory article format, and indeed in
> Alex's talk he said integration with OpenTheory would be a worthy goal.
>
> The performance of their method is very impressive, and certainly faster
> than using OpenTheory as it is now, so I think it would greatly benefit
> OpenTheory to adopt and standardise K&K's ideas.
>
> I write this message to ask OpenTheory users for their comments on this
> proposal, and to make a call for volunteers to help with the
> integration/adoption. As a first step, perhaps we could just make a list of
> the differences from how OpenTheory currently works, to see what needs to
> be done.
>
> Ramana
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20130724/e8b0fee4/attachment.html>