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:  Gerard Huet <Gerard.Huet@i...> 
Subject:  Re: de Bruijn indices 
In defense of de Bruijn indices : 1. They lead to efficient implementations. My original implementation of the constructive engine in Coq's early versions used de Bruijn indices, and performed reasonably well. It leads to a completely applicative implementation of lambdacalculus, and the cost of lifting may be reduced by Okasakilike data structures. I still remember the day when this superhacker declared that he was going to replace all this inefficient stuff by slick hashtables  only to undo everything 2 months later because he was 30% slower. 2. The apparent complexity of lifting is to my view an inherent complexity of substitution, which you have better face up rather than put under the rug of name management of symbol tables, for which you will have to pay the price in unexpected places. And when the going gets rough, at least your DB indices behave well in natural recursions. When I set to understand fully Bohm's theorem, down to programming a running Bohm discriminator, I used DB indices, which generalise well to Bohm trees (ie potentially infinite lambdaterms). I do not think I would have succeded in programming this stuff without this explicit and concrete control on variable references. And I could even publish the code itself, which is available as commented Caml code in the paper: G. Huet An Analysis of Bohm's theorem, Theoretical Computer Science 121 (1993) 145167. 3. You can do proofs by induction on the corresponding structure, and thus prove metatheoretical results in a direct and clean way. You can even hope to actually mechanise the formal development. See for instance: G. Huet "Residual theory in lambda calculus: a formal development". J. Functional programming 4,3 (1994) 371394. where a fair portion of the syntactic theory of betareduction is done completely formally, using DB indices again. Gérard