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

[Benjamin Pierce <bcpierce@cis.upenn.edu>]

Fanning the fire on deBruijn indices...

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

There's an important difference, though, in the ways that these errors
show up: bugs in deBruijn-indexing schemes tend to manifest immediately
and catastrophically -- if you miss a 'shift' everything quickly gets all
screwed up and you can see that you did something wrong and fix it right
away -- while name-based implementations of substitution tend to fail
only six months later, when someone makes an unlucky choice of variable
names. 

There's a story that a substitution bug in the original LCS theorem
prover persisted for six *years* before anybody noticed...

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

I usually do this too.  The pretty-printer can also do a little
consistency checking on the deBruijn indices: each variable is
represented as a pair of its index and the expected size of the context;
if the printing routine sees that the actual context does not have this
size, it complains.  

One drawback of deBruijn indices that you did not mention is that, at
least when implemented naively, they are pretty expensive in terms of
the amount of consing that's required to perform substitutions. 

At the end of the day, I'm not that big a fan of *either* deBruijn or
named presentations of terms... both are pretty ugly to work with, in
different ways.  In fact, I find both distressing and fascinating that,
after so many years of thought by so many smart people, we're still in
such an unsatisfactory state wrt. binding.

    B