[opentheory-users] Theorem meta-data

[Joe Leslie-Hurd]

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

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.

Cheers,

Joe

On Fri, Nov 7, 2014 at 6:01 PM, Mario Carneiro <di.gama at gmail.com> wrote:
> I think it will be more backwards-compatible to use a pragma instead, since
> this is already used by various interpreters. Regarding the arguments
> against pragmas:
>
>>
>> 2. It should be maintained by tools processing articles (when
>> possible). Note that pragmas are discarded by the opentheory tool, so
>> fail this test for encoding meta-data.
>
>
> This is easily fixed by making the opentheory tool not discard pragmas (or
> at least specific pragmas, see below).
>
>>
>> 3. It should be a standard scheme, not reader-dependent, so pragmas
>> also fail for this reason.
>
>
> The way to work a pragma into the standard is to reserve certain pragma
> names within the standard itself. For example, the current standard suggests
> the pragma ["thmName", name] for setting a theorem's name - in a revision to
> the standard, just require that this specific pragma be honored when
> possible, and leave the rest (any pragma not of this form) to be
> user-defined.
>
> For the current purpose, a pragma ["metadata", meta] would satisfy the
> desired conditions. The main drawbacks are that it is more verbose and also
> does not directly connect itself to the associated theorem, but it gains the
> ability to mark other statements, like intermediate theorems.
>
> Mario
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>