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; Fri, 25 Aug 1995 16:06:08 +0100 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA087392616; Fri, 25 Aug 1995 08:56:56 -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 AA087292553; Fri, 25 Aug 1995 08:55:53 -0600 Received: from albatross.cl.cam.ac.uk (user drs1004 (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 25 Aug 1995 15:44:39 +0100 X-Mailer: exmh version 1.6.1 5/23/95 To: hol2000@leopard.cs.byu.edu Subject: More on theory signatures & remaking definitions in HOL In-Reply-To: Your message of "Mon, 10 Jul 1995 00:13:51 +0200." <95Jul10.001356met_dst.8082@sunbroy14.informatik.tu-muenchen.de> Mime-Version: 1.0 Content-Type: text/plain; charset="us-ascii" Date: Fri, 25 Aug 1995 15:44:36 +0100 From: Donald Syme Message-Id: <"swan.cl.cam.:030880:950825144656"@cl.cam.ac.uk> A while ago I suggested incorporating theory signature information into terms and types in order to allow conflicting definitions to be introduced into the system while preserving system integrity. Konrad mentioned the idea of allowing the redefiniton of a constant by tagging the defining theorem for the constant with a reference, and propogating this tag through every theorem which uses the definition. However, as he later pointed out to me, this doesn't work, and I thought it might me worth mentioning this on hol2000 "for the record". The problem is that many theorems about a constant do not utilise the defining theorem in their derivation. For instance, you can create a theorem using a constant simply usng REFL or SPEC. Given that functions like REFL and SPEC are essential to HOL, then the only way to stop bogus theorems is if bogus terms never come into existence. Anyway, that's an update on that topic. In terms of usability, I think the advantages of gettng away from the "incremental development" model of HOL are enormous - incremental systems do not allow backtracking/ undo/multiple theories. The scheme I am proposing would, when combined with a decent interface. I've been doing some experiments to see if it can be made efficient, which I think it can, but it needs more work. 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 -----------------------------------------------------------------------------