[opentheory-users] new_specification

[Rob Arthan]

Joe,

On 25 Feb 2014, at 22:14, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Ramana,
> 
> I'd never read that note by Rob, and it's very clear and persuasive. Although I have a natural resistance to changing the article file format in any way, the proposed primitive constant definition mechanism does seem to offer an improvement in expressivity at a modest cost of being more complicated to explain.

If you are going to change the format, can I make two feature requests:

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

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

Over to John and Ramana for the plans for HOL Light and ProofPower.

Regards,

Rob.

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