Return-Path: Delivery-Date: Received: from leopard.cs.byu.edu (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Sat, 8 Jul 1995 20:54:11 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA062052442; Sat, 8 Jul 1995 13:40:42 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: list Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with ESMTP (1.37.109.15/16.2) id AA062022431; Sat, 8 Jul 1995 13:40:31 -0600 Received: from albatross.cl.cam.ac.uk (user drs1004 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Sat, 8 Jul 1995 20:41:13 +0100 X-Mailer: exmh version 1.5.2 12/21/94 To: hol2000@leopard.cs.byu.edu Subject: Theory signatures & remaking definitions in HOL Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Sat, 08 Jul 1995 20:41:09 +0100 From: Donald Syme Message-Id: <"swan.cl.cam.:092230:950708194115"@cl.cam.ac.uk> Well, it's about time someone wrote something to hol2000... While discussing TkHolWorkbench with users, one of the most common requests has been some sort of mechanism to allow definitions to be modified and remade. Lots of hacks suggest themselves, but most seem ultimately unsatisfactory. The basic problem is the presence of the global symbol tables for constants and types, and the fact that objects of type "type", "term" and "thm" do not have their dependency on the symbol table recorded in their structure. 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. Redefining constants and types can then be done by creating new theory signatures and reproving effected results. The old theory signatures can get thrown away. Dependency management of results (i.e. how many things need to get reproved/redefined) then becomes an issue, but at least solutions begin to seem possible. In terms of space I think this can be implemented quite efficiently - the Isabelle implementation being the place to look. What I'm wondering is whether anyone has done any studies on how much this approach effects performance? It would be interesting to know what the tradeoffs are. Certainly the benefits of removing the global symbol tables and replacing them with non-global theory signatures could be large. Don Syme ----------------------------------------------------------------------------- At the lab: At home: The Computer Laboratory Trinity Hall New Museums Site CB2 1TJ University of Cambridge Cambridge, UK CB2 3QG, Cambridge, UK Ph: +44 (0) 1223 334688 Ph: +44 (0) 1223 302521 http://www.cl.cam.ac.uk/users/drs1004/ email: Donald.Syme@cl.cam.ac.uk -----------------------------------------------------------------------------