From mboxrd@z Thu Jan 1 00:00:00 1970 Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id VAA14847 for caml-red; Tue, 10 Oct 2000 21:22:14 +0200 (MET DST) Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id UAA14224 for ; Tue, 10 Oct 2000 20:30:38 +0200 (MET DST) Received: from hebe.or.intel.com (hebe.or.intel.com [134.134.248.4]) by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e9AIUbH09965 for ; Tue, 10 Oct 2000 20:30:37 +0200 (MET DST) Received: from ichips-ra.pdx.intel.com (ichips-ra.pdx.intel.com [10.7.8.35]) by hebe.or.intel.com (8.9.1a+p1/8.9.1/d: relay.m4,v 1.31 2000/08/22 00:15:13 dmccart Exp $) with ESMTP id LAA03683 for ; Tue, 10 Oct 2000 11:42:55 -0700 (PDT) Received: from dhpc0010.pdx.intel.com (dhpc0010.pdx.intel.com [10.7.21.33]) by ichips-ra.pdx.intel.com (8.9.1a/8.9.1/d: internal.m4,v 1.2 1998/11/09 19:18:37 iwep Exp iwep $) with ESMTP id LAA19684; Tue, 10 Oct 2000 11:30:35 -0700 (PDT) Received: from ichips.intel.com (johnh@localhost [127.0.0.1]) by dhpc0010.pdx.intel.com (8.9.1a/8.9.1/d: client-ra.m4,v 1.1 1998/12/24 19:00:55 jamesw Exp jamesw $) with ESMTP id LAA25018; Tue, 10 Oct 2000 11:30:34 -0700 (PDT) Message-Id: <200010101830.LAA25018@dhpc0010.pdx.intel.com> To: caml-list@inria.fr cc: John Harrison Subject: Re: de Bruijn indices Date: Tue, 10 Oct 2000 11:30:32 -0700 From: John R Harrison Sender: weis@pauillac.inria.fr It's been interesting for me to see a discussion of de Bruijn versus name-carrying term representations, since it's an issue I've spent some time thinking about and on which I've changed my opinion at least once. The different versions of the HOL theorem proving system: HOL88 - http://www.cl.cam.ac.uk/Research/HVG/FTP/#hol88 hol90 - http://www.cl.cam.ac.uk/Research/HVG/FTP/#hol90 HOL Light - http://www.cl.cam.ac.uk/users/jrh/hol-light/index.html hol98 - http://www.cl.cam.ac.uk/Research/HVG/FTP/#hol98 have gone through several different term representations over the years: HOL88 - name-carrying hol90 - name-carrying at first then de Bruijn HOL Light - de Bruijn at first then name-carrying hol98 - de Bruijn at first then explicit substitutions The original HOL88 name-carrying implementation was probably inherited from Edinburgh or Cambridge LCF. This was quite satisfactory, but over the years several obscure bugs were found in variable renaming which could have caused unsoundness, an embarrassment in a system that stresses its logical consistency. To avoid having the soundness of the system depend on tricky programming, hol90 changed to using a de Bruijn representation. However, all versions of HOL maintain an abstract type of terms with a name-carrying interface, so the de Bruijn indices must be an internal detail that is hidden from the user. This makes de Bruijn terms grossly inefficient for very large abstraction-rich terms. The trivial operation of recursively descending a term can involve a quadratic amount of work, since each time a binder is traversed, a variable must be substituted for a de Bruijn index throughout the body. For this reason, although I was initially enthusiastic about de Bruijn terms, I rapidly decided they didn't fit with the HOL worldview and changed HOL Light (my small clean reimplementation of the system in CAML Light) back to a name-carrying approach. Very recently, Bruno Barras has been the driving force behind yet another term representation for hol98 that admits an efficient ML-style reduction algorithm. See: @INPROCEEDINGS{tphols2000-Barras, crossref = "tphols2000", title = "Programming and computing in {HOL}", author = "Bruno Barras", pages = "17--37"} @PROCEEDINGS{tphols2000, editor = "M. Aagaard and J. Harrison", booktitle = "Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000", series = "Lecture Notes in Computer Science", volume = 1869, year = 2000, publisher = "Springer-Verlag"} All of this goes to show that despite intensive activity in the field, the basic question of the most appropriate term representation -- even for a particular narrowly focused application -- is not yet clearly agreed on. Cheers, John.