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 OAA06578 for caml-red; Tue, 10 Oct 2000 14:05:49 +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 MAA05027 for <caml-list@pauillac.inria.fr>; Tue, 10 Oct 2000 12:36:39 +0200 (MET DST)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e9AAabj15112;
	Tue, 10 Oct 2000 12:36:37 +0200 (MET DST)
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id MAA05015; Tue, 10 Oct 2000 12:36:36 +0200 (MET DST)
From: Pierre Weis <Pierre.Weis@inria.fr>
Message-Id: <200010101036.MAA05015@pauillac.inria.fr>
Subject: Re: de Bruijn indices (Re: WWW Page of Team PLClub)
In-Reply-To: <20001009031955T.sumii@saul.cis.upenn.edu> from Eijiro Sumii at "Oct 9, 100 03:19:55 am"
To: sumii@saul.cis.upenn.edu
Date: Tue, 10 Oct 2000 12:36:36 +0200 (MET DST)
Cc: caml-list@inria.fr
X-Mailer: ELM [version 2.4ME+ PL28 (25)]
MIME-Version: 1.0
Content-Type: text/plain; charset=US-ASCII
Content-Transfer-Encoding: 7bit
Sender: weis@pauillac.inria.fr

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

Hope you will not get the dark sides of both worlds!

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

You're right.

Still, I fooled a supposed ``perfectly debugged'' partial evaluator
with my first higher-order example (admittedly not a simple but a
rather subttle program, that forces you to recursively insert
lambda-terms and beta-reduce them, and could exercise your De Bruijn
indices lifter in a non standard way ...).

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://cristal.inria.fr/~weis/