[opentheory-users] Scalable LCF-style proof translation

[Alexander Krauss]

Hi Ramana, Hi Joe,

Thanks, Ramana, for summarizing our discussions at ITP here on the list.

Some more aspects:

- When we came up with our format, the goal was really to have the 
simplest thing possible to achieve our goal, i.e., good scalability and 
performance. Choosing OpenTheory right from the start would probably 
have forced us to make trade-offs here to be compliant with the format, 
which we did not want to make at this point.
However, we do not have sufficient data to say that it couldn't be done 
similarly with the OpenTheory format as it is now.

- So far, we haven't really tried to use the OpenTheory exporter from 
HOL Light on Flyspeck, mainly because it seemed to rely on all those 
annotations present in the sources, and having to put in these commands 
into the Flyspeck sources did not seem very attractive.

- In any case, I think in the long run it does not make sense to have 
two formats, and I am more than happy to give up our format if the cost 
is not too high.


On 07/26/2013 11:29 PM, Joe Leslie-Hurd wrote:
> 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?


I must pass this question on to Cezary, who made this specific 
experiment. I'm not even sure whether this is before or after 
compression... But just looking at the list of OpenTheory commands, it 
seems to me that building up substitutions as nested lists on the stack 
is rather complicated.


> 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.)

In fact they are generative in the sense that new constant objects are 
constructed each time. Optimizing this does not seem very relevant to 
me, so I guess we can ignore this for now.


>> Is there a good reason for the stack-based approach? I couldn't think of
>> any, but maybe I'm missing something.

Yes, I also wonder about whether there was a motivation beyond the 
conceptual simplicity that a command is always just a single token.


However, I have some further questions:


- I wonder which of the offline processing that we do currently is 
actually done similarly by the existing opentheory infrastructure. By 
looking at some opentheory tool help texts, I couldn't see the answer to 
this question. Most of the commands seem to be concerned with package 
management, which is unrelated. Currently, we do

   -- mark the last occurrence of any given object, to ensure deletion
   -- strip material that is not relevant for some "exported" theorem


- Do the existing exporters make use of the stack in any significant way 
apart from what is necessary to construct objects? How does the HOL 
Light exporter deal with sharing (between terms)? I assume for the HOL4 
exporter this is not an issue, since sharing can be observed directly. 
Is this correct?

- If I want to play with the tools, i.e., export some small theorem from 
HOL Light, apply some mapping (aka theory interpretation) and re-import 
into HOL4... Are there any step by step instructions that I can follow?

Thanks,
Alex