Delivery-Date: 
Sender: hol2000-request@lal.cs.byu.edu
Errors-To: hol2000-request@lal.cs.byu.edu
Precedence: list
From: Konrad Slind <slind@informatik.tu-muenchen.de>
To: donald.syme@cl.cam.ac.uk
Cc: hol2000@leopard.cs.byu.edu
In-Reply-To: <"swan.cl.cam.:092230:950708194115"@cl.cam.ac.uk> (message from Donald Syme on Sat, 8 Jul 1995 21:41:09 +0200)
Subject: Re: Theory signatures & remaking definitions in HOL
Message-Id: <95Jul10.001356met_dst.8082@sunbroy14.informatik.tu-muenchen.de>
Date: Mon, 10 Jul 1995 00:13:51 +0200


> As far as I can tell, the only really neat solution to this problem is
> to take the Isabelle approach and store references to context
> information inside types and terms (certified terms and types in
> Isabelle).  This eliminates the need for global constant and type
> symbol tables without a loss of security. In this setting, functions
> like "mk_comb" do a merge of theory signatures for the two terms.

Don is right -- this is a problem. However, may I quibble with his
proposed solution? My knee-jerk response is that working at the term and
type level may be too low. How about the following, which works at the
definition and inference level?

   Theorems have a new field `shade' in their representation. It's a
   list of references to the SML type defined

       datatype colour = WHITE | RED

   When a definition gets made, build a reference to WHITE and put it in
   the `shade' field. Whenever an inference gets made, union the shades
   of the input theorems. When a definition is remade, assign the
   reference in the shade cell of the old definition the colour
   RED. This will change the colour for all theorems proved (and
   definitions made) using the old definition. There is a "lazy" aspect
   to this approach, since the colour of any theorem will only be
   computed when a theory is finalized, or the user attempts to store it
   in a theory.

   This sort of classification could perhaps be lifted to the theory
   level, for reasons of efficiency. If a theory was "stable", i.e., its
   definitions were not going to ever change, then theorems of that
   theory would be WHITE, but carry no reference tags. That way,
   inference wouldn't necessarily get slower as the theory hierarchy
   became deeper.

I think ProofPower has a scheme that also works at the inference
level. They told me about it years ago, but I've forgotten the
details. Maybe I am remembering their solution?


Konrad.