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; Wed, 25 May 1994 10:16:01 +0100 Received: by leopard.cs.byu.edu (1.37.109.8/16.2) id AA12416; Wed, 25 May 1994 03:13:35 -0600 Sender: hol2000-request@lal.cs.byu.edu Errors-To: hol2000-request@lal.cs.byu.edu Precedence: bulk Received: from swan.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.8/16.2) id AA12412; Wed, 25 May 1994 03:12:57 -0600 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Wed, 25 May 1994 10:12:31 +0100 To: hol2000@leopard.cs.byu.edu Subject: Re: Basic changes In-Reply-To: Your message of "Tue, 24 May 94 16:17:06 +0200." <94May24.161719met_dst.8129@sunbroy14.informatik.tu-muenchen.de> Date: Wed, 25 May 94 10:12:19 +0100 From: Richard Boulton Message-Id: <"swan.cl.cam.:061420:940525091240"@cl.cam.ac.uk> Konrad Slind writes: > IMHO, there could be some interesting changes made: > . > . > - term: a more detailed (and hence more efficient) lambda-calculus, > perhaps with pairing or records "built-in"; Currently there are only two kinds of branch node in the trees that represent terms: COMB (combinations, i.e., function applications) and ABS (lambda abstractions). As Konrad says, having other constructs as basic (when currently they are represented in terms of COMB and ABS) can make some things more efficient, and easier. However, there is a price: programs operating over terms become more complex because all the new cases have to be dealt with. In my opinion, one of the beauties of the HOL logic is the simplicity of just having COMB and ABS, and it is not something that should be given up lightly. Having said that, there is a strong case for making abstractions over tuples built-in. In fact, is there any reason why such a construct can't subsume the existing ABS, it being taken as the special case in which the tuple has one component? Richard.