[opentheory-users] Theorem meta-data

[Joe Leslie-Hurd]

Since the proposal for attaching metadata to exported theorems did not
generate much enthusiasm, I propose shelving the idea for
consideration when developing future versions of the article spec.

Cheers,

Joe

On Sat, Nov 8, 2014 at 11:54 PM, Joe Leslie-Hurd <joe at gilith.com> wrote:
> Hi Mario,
>
>> This made me realize a potential issue in the current spec and even the
>> version 5 spec: the theorem export list is described as a "set", even though
>> my own implementation just treats it as a list. What is supposed to happen
>> if you export two alpha-equivalent theorems?
>
> Actually now I think about it alpha-equivalence is not relevant here.
> The thm command specifies a particular representative of the
> alpha-equivalence class, and that is exported from the article. So
> really the question becomes: what happens if you export two identical
> theorems, and the answer is that they get merged and only one of them
> is exported (it doesn't matter which).
>
>> With metadata, this becomes still more
>> complicated.
>
> With metadata only one of the theorems is exported like before, and
> its associated metadata would be formed by merging the metadata
> associated with the two theorems.
>
>> My java implementation would have issues with using a HashMap
>> for the thm keys of that map, because I have no hash function that respects
>> alpha-equivalence.
>
> For the reason above, this shouldn't be a problem.
>
>> Incidentally, are you in agreement with using a name -> object finite_map
>> for the metadata?
>
> Actually my proposal in
>
> http://www.gilith.com/opentheory/mailing-list/2014-November/000438.html
>
> was to use metadata with the following ML syntax
>
> datatype metadata = Metadata of (name, metadata) finite_map;
>
> represented using article lists, so for example the metadata
>
> name: head_def
> HOLLight:
>   name: HD
>   simplifier
>
> would be represented as
>
> [["name",[["head_def",[]]]],
>  ["HOLLight",[["name",[["HD",[]]],["simplifier",[]]]]]
>
> Merging two pieces of metadata would simply be the union of two finite
> maps, where if they map the same name then the inner finite maps are
> merged recursively. This has the desired idempotence property.
>
> The reason I don't want to use (name,object) finite_map is that
> objects can contain theorems and other data that affect logical
> dependencies between theories, and one of my design goals for metadata
> was to be transparent with respect to logical dependencies. The above
> scheme just involves names and lists, which has no effect on logical
> dependencies.
>
> Cheers,
>
> Joe