Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:   (:) 
From:  Pierre Weis <Pierre.Weis@i...> 
Subject:  Re: WWW Page of Team PLClub (Re: ICFP programming contest: results) 
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 alphaconversion problems: expressions > have unique representations, without any need to work modulo renaming of > bound variables; moreover, substitution of variables by nonclosed > expressions works very well, without any risk of name clashes as in > the normal, namebased 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, heapallocated > 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 alphaconversion when performing betareduction (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 alpharenaming. As an example, consider the parallel (or multiple) betareduction: 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 prettyprinter 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/