[opentheory-users] Theorem meta-data

[Joe Leslie-Hurd]

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