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 KAA05252 for caml-red; Sat, 7 Oct 2000 10:35:41 +0200 (MET DST) Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id KAA00457 for ; Sat, 7 Oct 2000 10:35:22 +0200 (MET DST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e978ZLT02840; Sat, 7 Oct 2000 10:35:21 +0200 (MET DST) Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id KAA28303; Sat, 7 Oct 2000 10:35:21 +0200 (MET DST) From: Pierre Weis Message-Id: <200010070835.KAA28303@pauillac.inria.fr> Subject: Re: WWW Page of Team PLClub (Re: ICFP programming contest: results) In-Reply-To: <20001006100731.12927@pauillac.inria.fr> from Xavier Leroy at "Oct 6, 100 10:07:31 am" To: Xavier.Leroy@inria.fr (Xavier Leroy) Date: Sat, 7 Oct 2000 10:35:21 +0200 (MET DST) Cc: caml-list@inria.fr X-Mailer: ELM [version 2.4ME+ PL28 (25)] MIME-Version: 1.0 Content-Type: text/plain; charset=US-ASCII Content-Transfer-Encoding: 7bit Sender: weis@pauillac.inria.fr Xavier explained de Bruijn indices > Notice that a de Bruijn index is relative to the position of the > variable reference. Hence the same variable can be referenced by > different de Bruijn indices depending on context, e.g. > > fun x -> print_int x; fun y -> x + y > > becomes > fun -> print_int var0; fun -> var1 + var0 > ^^^^ ^^^^ > this is x this is x too! > > De Bruijn indices are interesting for several reasons. One is > that they totally eliminate any alpha-conversion problems: expressions > have unique representations, without any need to work modulo renaming of > bound variables; moreover, substitution of variables by non-closed > expressions works very well, without any risk of name clashes as in > the normal, name-based notation. > > Another reason is that if you represent the evaluation environment as > a stack, with each new binding simply pushing the bound value on top, > then the de Bruijn index for a variable is simply the position of the > variable's value in the stack, relative to the top of the stack. > (Substitute "list" for "stack" to deal with persistent, heap-allocated > environments, e.g. for closures.) This leads to very simple > translations into abstract machine code. All this is perfectly true and correct, but in my humble opinion you forgot to mention the dark side of De Bruijn indices: - they are perfect for machines but not convenient for human beings! (We cannot easily consider that the same variable have plenty of different names in an expression.) - you have to manipulate indices anyway to mimmick alpha-conversion when performing beta-reduction (the operation is named the ``lifting'' of De Bruijn indices), and you know that this is at least as difficult and error prone as performing alpha-renaming. As an example, consider the parallel (or multiple) beta-reduction: the problem is to calculate f e1 e2 ... en by substituting e1 e2 ... en, in the body of f, supposed to be defined by lambda expression with n binders fun -> fun -> ... -> body. The problem is to perform the reduction in one pass on the body of f. This operation is trivial if you use a conventional beta reducer, but it is surprisingly difficult if you use De Bruijn indices. - as a consequence of these two properties, debugging code that manipulates and transforms lambda code in De Bruijn form is just a nightmare (each time I had to do it, I ended by writing a pretty-printer that reverts De Bruijn notation to good old names for variables!) That's why I consider a ``tour de force'' the Caml Light compiler that uses De Bruijn indices for the whole language. However, remember the famous ``De Bruijn wins again!'' leitmotiv we used to ear in the building when someone was desesperately fighting with wrong indices generated by the compiler! Also consider that the Caml Light compiler does not optimize and symbolycally manipulate programs: that's devoted to the next ``tour de force'', the Objective Caml optimizing compiler, which does not use the De Bruijn indices notation for lambda terms... Pierre Weis INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/