[opentheory-users] Multiple definitions in base package

[Rob Arthan]

Joe,

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

> Hi Rob,
> 
> I've given this some thought, because this redefinition problem can occur in a number of ways. As we have just seen on the other thread
> 
> http://www.gilith.com/opentheory/mailing-list/2014-March/000373.html
> 
> it is not constrained to a single article file, but also occurs when importing a sequence of articles that define symbols for "internal" use.
> 
> What would you think of the following scheme, which involves a change to the article standard?
> 
> 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 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?

Regards,

Rob.
 
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140327/7b49ea1d/attachment.html>