deBruijn vs alpha-renaming


Subject: deBruijn vs alpha-renaming
From: Philippe Meunier (meunier@ccs.neu.edu)
Date: Wed Jan 30 2002 - 19:48:57 EST


Here is his rational for using deBruijn in the implementation of the
typecheckers but not in the theory part. The lines preceeded by ">"
is me asking, and his answers follow. Note: the page numbers/section
numbers I'm refering to are no longer valid, since the book has quite
changed since the time we had this discussion.

Philippe

>49, 5.1, way 1: "quite tricky and it is easy to introduce subtle bugs": well,
>using de Bruijn indices can be quite tricky too...

Yes, but the bugs that you get are not subtle! This is the main thing
I like about the deBruijn style: when you make a mistake with
shifting, things tend to fail catastrophically and you get a chance to
fix it. Substitution bugs tend to surface only months later, in very
particular circumstances. Here's my new version of that paragraph:

  We choose the second, which, in our experience, is the easiest to
  manage when we come to some of the more complex systems later in the
  book. It also has the advantage of tending to fail catastrophically
  when it is used incorrectly, which allows bugs to be noticed and
  corrected early. Bugs in implementations based on the first
  approach,
  by contrast, sometimes manifest months or years after they are
  introduced. Our formulation uses a well-known technique due to
  Nicolas de Bruijn~\cite{DeBruijn72}.

[note: this is the now more or less the last paragraph before section
6.1, page 76]

>58, 5.3: "would make even simple definitions nearly impenetrable". When
>I compare this with what you say for "way 1" on page 49, I end up with this:
>alpha-renaming is tricky to define/implement now, but it's more simple
>and intuitive to reason about so that's what we will use latter; de Bruijn
>indices are "simple" (for some funny value of "simple" meaning "well-known"
>or "mechanical implementation", since definition 5.1.6 and the E-BETA rule
>on page 54 are not that simple...) but we will not use them latter because
>it makes explanations in the book too difficult. So basically you end up
>with saying again that your code is going to be different from what you
>explain. I'm afraid that at the end of the book, people won't be able to
>see anymore the relationship between the code and the definitions in the
>book, or they will have just forgotten it and will have to constantly refer
>back to this chapter each time they look at the real code. So if you plan
>on using named variables throughout the book, use them throughout the code
>=>scrap de Bruijn, or make it a chapter showing how to precisely define
>substitution, but without any impact on the rest of the book and code.
>Besides, you cannot say at the beginning of the chapter that you won't use
>alpha-renaming because it's too tricky, and then say at the end of the
>chapter that you will use it nevertheless because de Bruijn indices would
>make your definitions too difficult to understand...
>Finally, if you define type systems using named variables, then implement
>them using de Bruijn indices, how easily can you later argue that soundness
>proofs for your type systems carry over to your code ? You say yourself that
>using these things correctly is tricky...

I need to explain this better. What I wanted to convey was this:

  * the deBruijn representation is better for implementation (from my
    point of view) and for being clear about formal definitions and
    proofs
  * once the deBruijn presentation is understood, it is convenient to
    use terms with named variables as a *shorthand* for underlying
    deBruijn terms.



This archive was generated by hypermail 2b28 : Wed Jan 30 2002 - 19:48:58 EST