Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[Pierre Weis <Pierre.Weis@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/