[opentheory-users] new_specification

[Rob Arthan]

Ramana,

On 10 Mar 2014, at 12:41, Ramana Kumar <ramana at xrchz.net> wrote:

> On Mon, Mar 10, 2014 at 12:04 PM, Rob Arthan <rda at lemma-one.com> wrote:
> 1) Even though you never, ever, ever want to change it again, allow for the possibility by adding a new command “version” that pops a number off the stack. The number tells the virtual machine what version of the format the input file conforms to. In the absence of a “version” command, the default is 5 (i.e., the version before the “version” command was introduced).
> 
> I second this request! I believe Michael Norrish made a similar request earlier - oh, actually it was in a private email.
>  
> 2) Have a new command “diag” that is identical with “pop” as far as the virtual machine semantics is concerned but can be used in an implementation of the virtual machine to trigger some kind of diagnostic activity, like printing a report on the state of the virtual machine.
> 
> I implemented “diag” in the ProofPower reader and writer and I don’t believe I would have been able to get the writer working without it. It also gives a simple way of adding commentary to an article (you put the comment as a string followed by the diag command). Another reason for wanting it is that I think the article format has a potential use to do some useful application-specific things, e.g., I have clients who are interested in porting between a subset of Z in ProofPower and HOL4. “diag" would be helpful to give some application-specific hints to the reader, e.g., to tell it the name to use when it saves a theorem, without preventing the articles being compatible with other systems.
> 
> I also agree this would be useful. This has been discussed before: http://www.gilith.com/opentheory/mailing-list/2011-October/000167.html.

Thanks for the pointer. I wasn’t reading this list very actively at that time. You were using “pop" with a test for a special form of the stack to implement a diagnostic check. I think with my proposal you can implement that kind of thing and be sure that it won’t be fooled by “pop”s that accidentally occur with the stack in the special form. I don’t see any particular need to standardise the semantics other than to say that “diag” is equivalent to “pop” as far as the virtual machine semantics are concerned.

>  
>> I would consider changing the OpenTheory logical kernel to support it, particularly if HOL4 or ProofPower incorporated it as the primitive constant definition mechanism, but I'd be interested to hear what John has to say about it.
> 
> John, Ramana, Scott Owens and I talked about this a few months ago. There was general agreement to adopt the new constant definition mechanism once someone had confirmed my informal proof of correctness with a formal proof. Ramana has done that now. It is certainly only a matter of time before I implement it in ProofPower. It would be nice to be able to extend my OpenTheory reader/writer to handle it at the same time. 
> 
> Well, I have proved something about it, but I'm not sure it is as strong as what your informal proof said (which was conservativity) ;) Nevertheless I expect to prove that soon.

Great! Thanks for all your efforts on this.

>  
> Over to John and Ramana for the plans for HOL Light and ProofPower.
> 
> I have implemented the revised new_specification for HOL4 and plan to integrate it with the master development branch as soon as it is supported by OpenTheory. I don't want to do it before then because that would break HOL4's OpenTheory exporter (since I replaced new_definition with the new rule for specification, which has no OpenTheory analogue to export to as yet).
>  

I am in much the same position: I could emulate the new rule with the existing OpenTheory defineConst and the choice operator, but it would be a tedious throw-away piece of work, if we are agreed that OpenTheory needs to support the new rule. 

I would propose leaving defineConst in OpenTheory as it is trivial to implement in terms of the new rule, so articles conforming to version 5 will still work.

Out of interest, what have you called the new rule?

Regards,

Rob.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140310/e755cf56/attachment-0001.html>