[opentheory-users] Scalable LCF-style proof translation

[Joe Leslie-Hurd]

Hi Ramana,

Thanks for drawing my attention to this paper, it's nice to see a
collection of detailed performance statistics for the OpenTheory style
of low-level proof logging.

>From looking at the article formats it seems to be mainly stylistic
differences, such as OpenTheory using of a stack and dictionary
whereas K&K use only a dictionary (this reminds me of the difference
between JVM and Dalvik bytecodes). In OpenTheory it's up to the reader
to decide how to process definitions: they're not inherently
generative. The OpenTheory reader implements a purely functional
logical kernel, so its definitions are generative, but reading an
article into HOL Light would make definitions that update the global
symbol table.

Given these minor differences, I'm intrigued by the statement in the conclusion:

"In our development we defined a new format for proof exchange traces, despite
the existence of other exchange formats. We have tried writing the
proof trace in the
OpenTheory format, and it was roughly 10 times bigger."

Cezary, Alex: Would it be possible to share this proof trace in the
two formats, so I can see what difference is responsible for the
blow-up?

Cheers,

Joe

On Wed, Jul 24, 2013 at 5:51 AM, Ramana Kumar <Ramana.Kumar at cl.cam.ac.uk> wrote:
> 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
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>