Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: bulk
From: David Shepherd <des@inmos.co.uk>
Message-Id: <4995.9410110954@frogland.inmos.co.uk>
Subject: Re: adding definitions to closed theories
To: reetz@ira.uka.de (reetz)
Date: Tue, 11 Oct 1994 10:54:16 +0100 (BST)
Cc: hol2000@leopard.cs.byu.edu
In-Reply-To: <"i80fs2.ira.472:11.10.94.09.48.50"@ira.uka.de> from "reetz" at Oct 11, 94 10:48:39 am
Content-Type: text
Content-Length: 1965

reetz has said:
> David Shepherd writes:
> 
> >I think the problem here is that HOL maintains a global name
> >space for constants. Adding definitions can cause problems
> >as consider a theory TH1 which has as parents TH2 and TH3.
> >If indenpendently new definitions are added to TH2 and TH3
> >which each define the same name then there will be a clash
> >in TH1. If constants were identified by a pair of defining theory
> >and name then this might be less of a problem.
> 
> Another solution may be overloaded constants, i.e. in TH2
> a constant foo:type1 and in TH1 a constant foo:type2 can
> defined. Anyway, if I want to add a new constant to e.g. TH2,
> I don't see a problem in looking throw the WHOLE theory tree
> and not only to the parents of TH2 in searching for an
> (hopefully) not already existing constant of the same name.

That may be ok if you are the only user of the theories. But other
people (or other theories of yours) could have TH2 as a parent - you
can still get name clashes with them.

I think the only "safe" way to do this would be to identify constants
with their definitions so that two constants can be defined with the
same name but be distinguished because they reference differnt
definitions (as is standard practice in parse tree structure). The
current form of constants (name & type) cannot handle this so a 
restriction is needed - i.e. unique names. Extending this to simple
overloading via unique pair of (name,type) seems intuitive but I
suspect with type polymorphism this could be problematic. I think this
has been discussed at length before (probably in info-hol) ... I seem
to recall that the ICL people managed to do this.


--------------------------------------------------------------------------
david shepherd: des@inmos.co.uk                     tel: 0454-616616 x 638
                inmos ltd, 1000 aztec west, almondsbury, bristol, bs12 4sq
		"I  am  not  a  nut      ---      I  am  a  human  being."