Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: bulk
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: donald.syme@cl.cam.ac.uk, info-hol@leopard.cs.byu.edu
In-Reply-To: <"swan.cl.cam.:095140:950213101737"@cl.cam.ac.uk> (message from Donald Syme on Mon, 13 Feb 1995 11:17:25 +0100)
Subject: Re: new_parent bugs in hol90.7 and hol88 2.02
Message-Id: <95Feb13.185055met.8081@sunbroy14.informatik.tu-muenchen.de>
Date: Mon, 13 Feb 1995 18:50:47 +0100


> > 
> > In hol90.7, new_parent doesn't seem to work if the specified parent
> > is already an ancestor of the current theory.  This is different to
> > hol88.  Is this a bug or a feature?
> 
> I would say that it's the correct behaviour; "new_parent" ought to do
> nothing if the nominated theory is already an ancestor. Maybe a wrapper
> routine around "new_parent" like the following would be helpful.
> ...

> I'm not sure about this.  The best reason to directly add a parent
> which is already an ancestor is for clarity - i.e. to show that a
> theory uses another theory directly, and not merely as an artifact of
> it being an ancestor via a third theory.  Ancestors are different from
> parents, right?  For instance they will be shown differently in a
> graphical representation of the theory tree.  The HOL theory tree
> tends to represent the implementation of the HOL logic rather than the
> user's preception of the logic.  Adding new parents is one of the only
> ways of adjusting the theory tree to reflect the real logical
> structure.


It's debatable. (I guess that's why we're debating it, huh?) One could
argue that declaring a new parent is a way of making resources
available; if they are already there, nothing needs to be done. The
actual resources used can be ascertained in other ways, for instance by
instrumenting the functions that explicitly bring objects in from
theories.

Konrad.