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 NAA20625 for caml-red; Fri, 13 Oct 2000 13:50:16 +0200 (MET DST)
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id UAA13378 for <caml-list@pauillac.inria.fr>; Thu, 12 Oct 2000 20:19:08 +0200 (MET DST)
Received: from mail-blue.research.att.com (mail-blue.research.att.com [135.207.30.102])
	by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e9CIJ7f25083
	for <caml-list@inria.fr>; Thu, 12 Oct 2000 20:19:08 +0200 (MET DST)
Received: from bigmail.research.att.com (bigmail.research.att.com [135.207.30.101])
	by mail-blue.research.att.com (Postfix) with ESMTP
	id D894E4CE23; Thu, 12 Oct 2000 14:19:06 -0400 (EDT)
Received: from raptor.research.att.com.research.att.com (raptor.research.att.com [135.207.23.32])
	by bigmail.research.att.com (8.8.8/8.8.8) with ESMTP id OAA05113;
	Thu, 12 Oct 2000 14:19:06 -0400 (EDT)
To: Chet Murthy <chet@watson.ibm.com>
Cc: caml-list@inria.fr
Subject: Re: de Bruijn indices
References: <200010121457.KAA04527@nautilus-chet.watson.ibm.com>
From: Trevor Jim <trevor@research.att.com>
Date: 12 Oct 2000 14:19:06 -0400
In-Reply-To: Chet Murthy's message of "Thu, 12 Oct 2000 10:57:56 -0400"
Message-ID: <dr93di1c485.fsf@raptor.research.att.com>
User-Agent: Gnus/5.0806 (Gnus v5.8.6) Emacs/20.6
MIME-Version: 1.0
Content-Type: text/plain; charset=us-ascii
Sender: weis@pauillac.inria.fr

Chet Murthy <chet@watson.ibm.com> writes:

> It wasn't the substitution that was killing me, but the
> alpha-conversion, and checks for alpa-conversion.
> 
> Now, there _is_ possibly one way of doing explicit names that would be
> fast enough to be a contender -- where the names are chosen uniquely,
> using a global counter, so no capture check is required.  I can
> imagine that that would be fast.

We used exactly this strategy in the optimizer of SML/NJ (see Journal
of Functional Programming 7(5), September 1997 for some more detail).
Variable names are essentially a string plus a counter, e.g.,
foo15432.  Only compiler writers see these names, so the ugliness of
the output was not a big concern.

A "hidden" expense is that you have to preserve the following critical
invariant through optimization: every variable is bound at most once
in the program.  In our work, we were inlining functions used exactly
once, and the invariant is trivially preserved by this optimization.
In general beta reduction, binding occurrences are duplicated, and so
we have to do alpha renaming there.

I can't comment on how this compares in speed to de Bruijn indices.


-Trevor