[opentheory-users] Theorem meta-data

[Rob Arthan]

Joe,

On 8 Nov 2014, at 09:12, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Mario,
> 
> Thanks for your feedback on the proposal. I have given a lot of
> thought to your email, and in reply let me explain a little about my
> vision for the OpenTheory project.
> 
> Firstly, I see the goal of the project as evolving a set of standards
> for proofs and theories to capture the needs of people wanting to
> exchange theories between theorem prover implementations. So I'm not
> too worried about maintaining backward compatibility if there's a
> measurable improvement, just like the situation with removing the
> unnecessary free variables from the theorems produced by defineTypeOp.
> 
> Rob's suggestion of a version command makes incompatible changes in
> articles easy to deal with, and I will commit to ensuring that the
> opentheory tool will support all released versions of OpenTheory
> standards. My hope is that people developing tools will always choose
> the latest version of the standards, and not have to worry about
> processing earlier versions (perhaps using the opentheory tool to
> upgrade earlier versions if necessary).

I am looking forward to seeing how this works out when I finish
upgrading my reader/writer for ProofPower to version 6.  Will
it be possible to do the conversion with the opentheory tool
as a filter (so a script to import an article can just convert it
to its preferred version on the fly)?

> 
> So in the context of an evolving set of standards I see the pragma
> article command as a laboratory for testing out new ideas in different
> article readers, with the idea that once new features are tested they
> can be standardized as new commands that every reader must implement
> in the same way. For example, if most readers support a debug pragma
> then I see no problem with creating a debug command in future versions
> of the article standard that all readers must respect. In this role of
> a test laboratory that different readers process in different ways, it
> seems that the opentheory tool has no choice but to discard pragma
> commands when producing articles.
> 
> In the light of the above, and the requests I have heard to include
> theorem metadata in articles, I still see it as a good idea to propose
> an extra argument to the thm article command that all readers must
> process in the same way. I'd be interested in hearing your thoughts
> (and the thoughts of others on the list) on whether the specific
> proposal captures specific theorem metadata needs, or indeed whether
> there is enough added value to justify making a change at all.
> 

I agree with the idea that readers must implement each command in
the same way, but I take this as being relative to the representation
chosen for the OpenTheory virtual machine in a particular reader.
If you are going to say that the extra argument to the thm command
must be processed in the same way, then you are going to have
to extend the OpenTheory virtual machine to include the theorem
metadata, so that you can define that processing. Were you planning
to do that?

If you weren’t planning to change the virtual machine, then
this seems to me like a good candidate for a standardised
pragma as Mario suggests. First that means there is no
implementation overhead for anyone maintaining a reader
and who doesn’t want to use the metadata. Secondly, the
opentheory tool could duck the question of how to
combine multiple metadata: it could just include all the
relevant pragmas. Finally it seems intuitively right. since
readers that do use the metadata are likely to use it in
different ways, so it is a pragmatic matter, aside from
the core semantics of OpenTheory.

Regards,

Rob.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20141108/982376fb/attachment.html>