[opentheory-users] Theorem meta-data

[Joe Leslie-Hurd]

Hi Mario,

Reading your post, thank you for clarifying the "pragmas can't change
the state but all other commands must" position, which I agree with in
essence.

Also, I think I may have been misleading in my earlier email. My
proposal would certainly involve changing the type of the exported
theorems from

thm set

to

(thm, metadata) finite_map

in the definition of the virtual machine, and so my proposed extra
argument to the thm command indeed have an effect on the state of the
virtual machine. When I said the behaviour would be reader-dependent I
misspoke, the article reader would have defined behaviour, but how the
theorem metadata was processed would depend on the theorem prover
implementation.

The proposed type of exported theorems above makes it clear that we
need a way to merge metadata if two alpha-equivalent theorems are
exported. It also shows that two different theorems may have identical
metadata without causing confusion.

Cheers,

Joe


On Sat, Nov 8, 2014 at 5:25 PM, Mario Carneiro <di.gama at gmail.com> wrote:
> 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
>
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>