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 MAA04553 for caml-red; Tue, 10 Oct 2000 12:29:27 +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 JAA05350 for <caml-list@pauillac.inria.fr>; Mon, 9 Oct 2000 09:19:59 +0200 (MET DST)
Received: from dynabook (207-245-78-253.dca.net [207.245.78.253])
	by concorde.inria.fr (8.10.0/8.10.0) with ESMTP id e997Jvn05380;
	Mon, 9 Oct 2000 09:19:57 +0200 (MET DST)
Received: from dynabook
	([127.0.0.1] helo=localhost ident=sumii)
	by dynabook with esmtp (Exim 3.12 #1 (Debian))
	id 13iXE4-00008T-00; Mon, 09 Oct 2000 03:19:56 -0400
To: Pierre.Weis@inria.fr
Cc: Xavier.Leroy@inria.fr, caml-list@inria.fr, sumii@saul.cis.upenn.edu
From: Eijiro Sumii <eijiro_sumii@anet.ne.jp>
Reply-To: sumii@saul.cis.upenn.edu
Subject: de Bruijn indices (Re: WWW Page of Team PLClub)
In-Reply-To: <200010070835.KAA28303@pauillac.inria.fr>
References: <20001006100731.12927@pauillac.inria.fr>
	<200010070835.KAA28303@pauillac.inria.fr>
X-Mailer: Mew version 1.94.1 on Emacs 20.7 / Mule 4.1 (AOI)
Mime-Version: 1.0
Content-Type: Text/Plain; charset=us-ascii
Content-Transfer-Encoding: 7bit
Message-Id: <20001009031955T.sumii@saul.cis.upenn.edu>
Date: Mon, 09 Oct 2000 03:19:55 -0400
X-Dispatcher: imput version 991025(IM133)
Sender: weis@pauillac.inria.fr

I don't actually use De Bruijn indices so often (because I usually use
higher-order abstract syntax whenever appropriate), but anyway...

> All this is perfectly true and correct, but in my humble opinion you
> forgot to mention the dark side of De Bruijn indices:

In my experience of writing some interpreters, compilers, type
checkers, partial evaluators, etc.,

> - they are perfect for machines but not convenient for human beings!
> (We cannot easily consider that the same variable have plenty of
> different names in an expression.)

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

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

Eijiro