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 VAA14885 for caml-red; Tue, 10 Oct 2000 21:17:40 +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 TAA13767 for ; Tue, 10 Oct 2000 19:31:52 +0200 (MET DST) Received: from igw8.watson.ibm.com (igw8.watson.ibm.com [198.81.209.20]) by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e9AHVpH09332 for ; Tue, 10 Oct 2000 19:31:52 +0200 (MET DST) Received: from sp1n189at0.watson.ibm.com (sp1n189at0.watson.ibm.com [9.2.104.62]) by igw8.watson.ibm.com (8.9.3/8.9.3/05-14-1999) with ESMTP id NAA07892 for ; Tue, 10 Oct 2000 13:31:50 -0400 Received: from nautilus-chet.watson.ibm.com (lig32-226-130-170.us.lig-dial.ibm.com [32.226.130.170]) by sp1n189at0.watson.ibm.com (8.9.3/Feb-20-98) with ESMTP id NAA22168 for ; Tue, 10 Oct 2000 13:31:48 -0400 Received: from nautilus.chet.org (localhost [127.0.0.1]) by nautilus-chet.watson.ibm.com (8.9.3/8.9.3/Debian 8.9.3-21) with ESMTP id NAA27342 for ; Tue, 10 Oct 2000 13:29:53 -0400 Message-Id: <200010101729.NAA27342@nautilus-chet.watson.ibm.com> X-Authentication-Warning: nautilus.chet.org: Host localhost [127.0.0.1] claimed to be nautilus.chet.org To: caml-list@inria.fr Subject: Re: de Bruijn indices In-reply-to: Your message of Tue, 10 Oct 2000 16:04:54 +0200. <200010101406.e9AE6Fj22755@concorde.inria.fr> Date: Tue, 10 Oct 2000 13:29:53 -0400 From: Chet Murthy Sender: weis@pauillac.inria.fr >>>>> "GH" == Gerard Huet writes: GH> 1. They lead to efficient implementations. My original GH> implementation of the constructive engine in Coq's early GH> versions used de Bruijn indices, and performed reasonably GH> well. It leads to a completely applicative implementation of GH> lambda-calculus, and the cost of lifting may be reduced by GH> Okasaki-like data structures. I still remember the day when GH> this super-hacker declared that he was going to replace all GH> this inefficient stuff by slick hashtables - only to undo GH> everything 2 months later because he was 30% slower. It turns out that deBruijn indices are *significantly* more efficient than explicit names. Moreover, the renaming operations that must be introduced to use explicit names are essentially the same as the "lifting", etc, operations used in deBruijn indices. I once modified Coq to use explicit names, and after spending a month or so, trying to make it as fast as Coq with deBruijn indices, switched back. That experiment, and finding that every _single_ avenue for improved performance, with explicit names, was a dead end, pretty much convinced me that deBruijn indices are much faster. Also, regarding human-readability, I think it is a red herring to ask whether the term Lambda("x",Ref 2) (which corresponds to something like ("lambda x. y") is more readable than Lambda("x",Var "y"). In both cases, without the "environment" that binds free variables to values, types, or "meanings" of some sort, the meaning of the term is undefined. So we need to keep these environments around, and once we have them, well, we can always just lookup the name, if want it. Moreover, it is only during debugging that having the "explicit name" actually buys us anything in readability. At runtime, if the program ever prints out something, it does so with respect to this "environment", so there's always a good name to use. If it is manipulating terms, well, it couldn't very well use the name for anything other than a lookup, since even in explicit names, the name can be modified, e.g. by alpha-conversion. Again, I started out as an "explicit name fanatic", and was converted to the "creed of deBruijn indices", by hard experience. I would recommend that before anyone write off deBruijn indices, they attempt to build a _large_ system (ok, so Coq isn't large by commercial standards, but by the standards of academic systems it ain't small) both ways. --chet--