[opentheory-users] Multiple definitions in base package

[Rob Arthan]

Joe,

On 27 Mar 2014, at 22:27, Joe Leslie-Hurd <joe at gilith.com> wrote:

> 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.
>> 
> …

> 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. …

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



Thanks for explaining how this is supposed to work. I am not sure I fully understand why the opentheory tool has to have abstraction mechanisms (local definitions) that aren’t supported by other HOL implementations.

However, if you feel it is necessary to have a notion of local definitions, then I would suggest we be more explicit about it. I think the article spec should say that there is a local namespace: names beginning “Local.” (say) belong to the local namespace. Once a name in the local namespace has been introduced as a quoted string, all subsequent references to the name are via a dictionary access. Thus the local namespace supports overloading, the dictionary being used to resolve the overloading. A reader may make an arbitrary choice of how to map a local name when it encounters one, providing it avoids clashes with names in other namespaces.

To help trace what is going on, rather than replacing the name you got from HOL Light or whatever by “” or “_”, I suggest you prefix the original name with “Local.”.

Regards,

Rob.

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140330/fac285a0/attachment.html>