[opentheory-users] Multiple definitions in base package

[Joe Leslie-Hurd]

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.

Thoughts?

Cheers,

Joe

On Wed, Mar 19, 2014 at 7:55 AM, Rob Arthan <rda at lemma-one.com> wrote:

> Joe,
>
> On 18 Mar 2014, at 17:49, Joe Leslie-Hurd <joe at gilith.com> wrote:
>
> Hi Rob,
>
> The HOLLight.* symbols are "auxiliary" type operators and constants that
> are used in proofs but not exported by any theory. So it's not unreasonable
> that it is defined multiple times in subtheories of base. However, what is
> surprising is that the article compression algorithm implemented in the
> opentheory tool does not fold the multiple definitions into a single
> definition.
>
> Thanks for the report: I'll look into the problem. This code will need
> reworking anyway to process the new article commands.
>
> 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.
>
> I think the article format definition should specify whether redefinition
> is allowed (and I would vote strongly for a constraint forbidding
> redefinition).
>
> Regards,
>
> Rob.
>
>
> _______________________________________________
> opentheory-users mailing list
> opentheory-users at gilith.com
> http://www.gilith.com/opentheory/mailing-list
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.gilith.com/opentheory/mailing-list/attachments/20140327/8e545b45/attachment-0001.html>