I don't actually use De Bruijn indices so often (because I usually use
higher-order abstract syntax whenever appropriate), but anyway...

> All this is perfectly true and correct, but in my humble opinion you
> forgot to mention the dark side of De Bruijn indices:

In my experience of writing some interpreters, compilers, type
checkers, partial evaluators, etc.,

> - 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.)

this inconvenience can be mitigated by including _both_ a name (for
human use) and an index (for machine use) in each variable, and

> - 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.

such errors in lifting, shifting, etc. of De Bruijn indices are much
easier to find than those in alpha-conversion, because they lead to
immediate problems (which occurs in simple programs) rather than
subtle ones (which occurs in only programs that "shadow" variables in
particular ways).

Eijiro