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 NAA21246 for caml-red; Fri, 13 Oct 2000 13:52:38 +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 VAA13649 for <caml-list@pauillac.inria.fr>; Thu, 12 Oct 2000 21:09:24 +0200 (MET DST)
Received: from hebe.or.intel.com (hebe.or.intel.com [134.134.248.4])
	by nez-perce.inria.fr (8.10.0/8.10.0) with ESMTP id e9CJ9Nf25460
	for <caml-list@inria.fr>; Thu, 12 Oct 2000 21:09:23 +0200 (MET DST)
Received: from ichips-ra.pdx.intel.com (ichips-ra-hme8.intel.com [10.7.13.35])
	by hebe.or.intel.com (8.9.1a+p1/8.9.1/d: relay.m4,v 1.31 2000/08/22 00:15:13 dmccart Exp $) with ESMTP id MAA03510
	for <caml-list@inria.fr>; Thu, 12 Oct 2000 12:21:41 -0700 (PDT)
Received: from dhpc0010.pdx.intel.com (dhpc0010.pdx.intel.com [10.7.21.33])
	by ichips-ra.pdx.intel.com (8.9.1a/8.9.1/d: internal.m4,v 1.2 1998/11/09 19:18:37 iwep Exp iwep $) with ESMTP id MAA28953;
	Thu, 12 Oct 2000 12:09:21 -0700 (PDT)
Received: from ichips.intel.com (johnh@localhost [127.0.0.1])
	by dhpc0010.pdx.intel.com (8.9.1a/8.9.1/d: client-ra.m4,v 1.1 1998/12/24 19:00:55 jamesw Exp jamesw $) with ESMTP id MAA12368;
	Thu, 12 Oct 2000 12:09:20 -0700 (PDT)
Message-Id: <200010121909.MAA12368@dhpc0010.pdx.intel.com>
To: caml-list@inria.fr
cc: John Harrison <johnh@ichips.intel.com>
Subject: Re: de Bruijn indices
Date: Thu, 12 Oct 2000 12:09:19 -0700
From: John R Harrison <johnh@ichips.intel.com>
Sender: weis@pauillac.inria.fr


Chet writes:

| It wasn't the substitution that was killing me, but the
| alpha-conversion, and checks for alpa-conversion.

I find that quite hard to understand. Profiles I've done in HOL Light
indicate that alpha conversion is not that common, and in the vast
majority of successful alpha-equivalence tests the two terms are
actually equal. Indeed after descending a couple of levels, subterms are
usually pointer-equal. Likewise, unsuccessful alpha-equivalence tests
almost always happen when the terms differ grossly near the top level.
Thus, in practice alpha-conversion is little done while
alpha-equivalence testing even of huge terms is not far from being
constant time. Are the typical profiles in Nuprl or Coq so very
different?

Substitution is less efficient than with dB terms, but I've found it
generally acceptable in practice, and certainly a price worth paying for
the conceptual simplicity of presenting a name-carrying interface to the
user rather than exposing floating dB indices.

| Again, I started out as an "explicit name fanatic", and was converted
| to the "creed of deBruijn indices", by hard experience.  I would
| recommend that before anyone write off deBruijn indices, they attempt
| to build a _large_ system (ok, so Coq isn't large by commercial
| standards, but by the standards of academic systems it ain't small)
| both ways.

Surely the size of the system is irrelevant: what matters is the size of
the problems it deals with. But anyway, from my own experience (and I
don't think HOL Light is smaller than Coq according to any plausible
metric) the Damascene conversion happened the other way round.

Cheers,

John.