[opentheory-users] Multiple definitions in base package

[Joe Leslie-Hurd]

Hi Rob,

> > Declare a particular name to be special (e.g., "" or "_") for definition commands, such that when a symbol of this name is defined a reader may substitute a fresh name instead. Then when articles are generated by the opentheory tool it can check which symbols appear in exported theories, and squash all the others to "". This would allow readers with global symbol tables to read articles with internal definitions with no problems.
>
> First of all, a small technical point: when you contrast the functional kernel of the opentheory tool with the global symbol tables used by other tools, surely it is not the functional/imperative distinction that matters, but rather that other tools may not support local definitions in the theories managed by their global symbol tables.

That's true, the OpenTheory standard library does rely on theorem
provers being able to make local definitions that only feature in the
proofs of a theory, not the exported theorems. In principle, since the
principles of definition are conservative, local definitions could be
removed from any article, but possibly at a cost of making it bigger.

The proposal above is a way to ensure that the local definitions in
any article do not exhibit any instances of multiple symbols having
the same name. This does not present a problem for a purely functional
kernel, but hopefully will help theorem provers that record
definitions by name in a symbol table.

> That said, I don't see how your proposal could work unless the opentheory tool is guaranteeing that, if it defines objects with squashed names, then it will never refer to those objects. If there is more than one definition of a squashed name, the squashed name, "_" (say),  becomes overloaded and there is no way the reader can resolve the overloading. If the opentheory tool is going to guarantee not to refer to objects with squashed names, why does it bother to make the definitions at all?

The latter scenario is what happens in practice: let me explain. After
an article reads a defineConst command, the stack looks like:

Thm ( |- c = t ) :: Const c :: rest-of-stack

Typically, the next thing that happens is that the theorem and
constant are popped off the stack and saved in a dictionary. When a
term needs to be built using constant c, it is simply looked up in the
dictionary: the article doesn't (and indeed can't) look it up by name.
So for internal symbols, their name is really unimportant, and can be
replaced with any fresh name. In the purely functional OpenTheory
kernel, I won't need to change anything to deal with squashed names,
they can simply all be called "" (and be distinguished by their
definition). In a reader that maintains a symbol table, these internal
symbols can be given any fresh name to allow them to be recorded in
the symbol table with no clashes.

This is why I was confused when you wrote this before:

> > If the multiple definitions are causing problems then as a workaround you can pick an arbitrary new name for any symbols in the HOLLight namespace, because such symbols are guaranteed never to be appear in any exported theorem.
>
> Thanks for that, it may come in useful. It will only work if the repeated definitions all give alpha-equivalent defining properties.

Hopefully the above explains why you can pick new fresh names for
every definition, you don't have to pick the same name for each
(possibly different) definition of "HOLLight.NUMSUM".

So, do you think the proposed change will help with reading theories
into ProofPower?

Cheers,

Joe