[opentheory-users] Theorem meta-data

[Mario Carneiro]

I think I'm starting to see the philosophical distinction that Rob is
trying to make. The main body of commands in the current spec all change
the state of the OT virtual machine in some way, with the only exception
being the "pragma" command, which by contrast is required *not* to change
anything which is tracked by the virtual machine. That is, you are not
allowed to define a pragma that puts something on the stack, because then
the machine wouldn't operate correctly if you took the command out or used
a reader that didn't respect that pragma. The idea is simply to make this
division remain true in later versions of the standard.

Thus, "debug" can never be made an official command, because unless
standard out is made a part of the virtual machine, it will always be a
no-op with respect to the state variables which *are* in the virtual
machine specification. Similarly, "thmName" can only be made an official
command if the exported theorem list in the virtual machine state contains
name information.

In this case, it seems that the best way to incorporate "metadata" the way
you are trying to do would involve a new type annotated_thm, which contains
a thm object and a map of name -> object entries. The virtual machine
assumption list would still be a list of thm, but the theorem list would be
a list of annotated_thm, and your two-argument "thm" command would package
the theorem and metadata together and appendthe resulting annotated_thm
object to the theorem list.

This way, it becomes mandatory to respect the metadata of a theorem in
order to have correct semantics, so by the above-mentioned philosophy it
would have to be an "official" command and not a pragma. Under the current
model of the virtual machine, any metadata would have to be tracked outside
the machine itself, which falls under the behavior of a pragma.

One more remark: this is not a concern for article readers, but what should
an article merger do if the theorem is mentioned with the same metadata key
and different values? Your merging algorithm only works if the metadata is
for different keys or is the same in both theorem objects.

Mario

On Sat, Nov 8, 2014 at 7:24 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:

> Hi Rob,
>
> > 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)?
>
> Indeed, this is already supported. This command reads an article (of
> any version) from stdin and writes an equivalent article on stdout
> using version 6:
>
> opentheory info --article --output-version 6 article:-
>
> > 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?
>
> No, I wasn't: my intention was that the theorem meta-data would be
> interpreted in a reader-dependent way. The proposal was merely a
> standard format for representing meta-data as finite maps represented
> by nested lists of names, not processing it.
>
> > 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.
>
> It would certainly be possible to specify theorem meta-data using
> pragmas, and perhaps this is after all the best way to do it.
>
> However, in the spirit of yesterday's unsolicited philosophy lecture,
> I would like to take a stand against "standardized pragmas". Once a
> particular pragma has demonstrated its usefulness, my favoured
> approach would be to define a new command in the next version of the
> article spec standardizing its behaviour, rather than adding it to a
> set of standardized pragmas. This is what I meant when I said I saw
> pragmas as an experimental laboratory for new commands.
>
> Given this approach, there is no standardized behaviour for pragmas,
> and so the opentheory tool does not have the information to maintain
> them in articles it processes. Consider maintaining a "debug" pragma
> during processing that compresses an article by merging equivalent
> objects, or maintaining a "thmName" pragma during processing that
> reorders the exported theorems.
>
> My theorem meta-data proposal was an attempt to standardize the
> behaviour of thmName as a new command (i.e., the existing thm command
> with an extra argument) so that the opentheory tool could maintain the
> information during processing, but this discussion is persuading me
> that the benefit of the change may not be worth its cost.
>
> Cheers,
>
> Joe
>
> _______________________________________________
> 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/20141108/dd92ec0a/attachment-0001.html>