From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id TAA12525 for caml-red; Tue, 10 Oct 2000 19:04:42 +0200 (MET DST)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id QAA08531 for <caml-list@pauillac.inria.fr>; Tue, 10 Oct 2000 16:06:17 +0200 (MET DST)
Received: from HUET-GERA1P (huet-gera2p.inria.fr [128.93.20.113])
	by concorde.inria.fr (8.10.0/8.10.0) with SMTP id e9AE6Fj22755;
	Tue, 10 Oct 2000 16:06:15 +0200 (MET DST)
Message-Id: <200010101406.e9AE6Fj22755@concorde.inria.fr>
X-Sender: huet@pop-rocq.inria.fr
X-Mailer: QUALCOMM Windows Eudora Pro Version 4.0.2 
Date: Tue, 10 Oct 2000 16:04:54 +0200
To: sumii@saul.cis.upenn.edu
From: Gerard Huet <Gerard.Huet@inria.fr>
Subject: Re: de Bruijn indices 
Cc: caml-list@inria.fr
References: <20001009031955T.sumii@saul.cis.upenn.edu>
Mime-Version: 1.0
Content-Type: text/plain; charset="iso-8859-1"
Content-Transfer-Encoding: quoted-printable
Sender: weis@pauillac.inria.fr

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 lambda-calculus, and the cost of lifting may be reduced
by Okasaki-like data structures. I still remember the day when this
super-hacker 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
lambda-terms). 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) 145-167.

3. You can do proofs by induction on the corresponding structure, and thus
prove meta-theoretical 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) 371-394.
where a fair portion of the syntactic theory of beta-reduction is done
completely formally, using DB indices again.=20

G=E9rard