Return-Path: Delivery-Date: Received: from bescot.cl.cam.ac.uk (user exim (mailer)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Thu, 21 Dec 1995 18:43:46 +0000 Received: from leopard.cs.byu.edu [128.187.2.182] by bescot.cl.cam.ac.uk with esmtp (Exim 0.27 #1) id E0tSpws-0006wu-00; Thu, 21 Dec 1995 18:42:54 +0000 Received: by leopard.cs.byu.edu (1.37.109.15/16.2) id AA042587800; Thu, 21 Dec 1995 07:56:40 -0700 Sender: info-hol-request@lal.cs.byu.edu Errors-To: info-hol-request@lal.cs.byu.edu Precedence: list Received: from smew.cl.cam.ac.uk by leopard.cs.byu.edu with SMTP (1.37.109.15/16.2) id AA042557797; Thu, 21 Dec 1995 07:56:37 -0700 Received: from coot.cl.cam.ac.uk [128.232.0.75] (jrh) by smew.cl.cam.ac.uk with esmtp (Exim 0.25 #2) id E0tSmQ4-0000V6-00; Thu, 21 Dec 1995 14:56:32 +0000 X-Uri: To: info-hol@leopard.cs.byu.edu In-Reply-To: Your message of "Wed, 20 Dec 1995 16:01:47 +0100." <"acid0.fzi..122:20.11.95.15.02.00"@fzi.de> Date: Thu, 21 Dec 1995 14:56:22 +0100 From: John Harrison Message-Id: This quadratic blowup for building and breaking apart abstractions is one of the big problems with using de Bruijn terms in a system like HOL. It's very useful to have a way of dealing with it, but of course, a more radical alternative would be to return to using name-carrying syntax. Here, the "mk_abs" and "dest_abs" operations take constant time. There are pros and cons for de Bruijn terms; at the moment I'm of the opinion that the cons outweigh the pros, the con you mention being the most prominent. The topic is worthy of more study. There are other kinds of term representation too, e.g. de Bruijn terms which also use indices for *free* variables. I think some systems do something like that, but I may be wrong. John.