[opentheory-users] new_specification

[Ramana Kumar]

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.


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


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


>
> Regards,
>
> Rob.
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140310/b152bb43/attachment.html>