Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[David McClain]

Hi, Congratulations!!!!

Could you provide a reference to de Bruijin indexing? I recall reading about
it some time ago, and after having searched my books here, I cannot find any
references to it. So I probably saw it in a paper some time ago... Anyway, I
would be interested since I have an interpreter name-lookup problem here
too.

Thanks in advance,

Congrats!!!

- David McClain

-----Original Message-----
From: eijiro_sumii@anet.ne.jp <eijiro_sumii@anet.ne.jp>
To: caml-list@inria.fr <caml-list@inria.fr>
Cc: jgm@cs.cornell.edu <jgm@cs.cornell.edu>; vouillon@saul.cis.upenn.edu
<vouillon@saul.cis.upenn.edu>; vgapeyev@seas.upenn.edu
<vgapeyev@seas.upenn.edu>; hahosoya@saul.cis.upenn.edu
<hahosoya@saul.cis.upenn.edu>; sumii@saul.cis.upenn.edu
<sumii@saul.cis.upenn.edu>
Date: Wednesday, October 04, 2000 10:26 PM
Subject: WWW Page of Team PLClub (Re: ICFP programming contest: results)


>Dear Camlers,
>
>> By the way, we are going to make a web page to describe what we did in
>> detail.  We'll announce it in this list when it's ready.
>
>Here it is.
>
>  http://www.cis.upenn.edu/~sumii/icfp/
>
>Enjoy,
>
>Team PLClub
>
>P.S.  Could you please add a link to the web page above in the contest
>result page (http://www.cs.cornell.edu/icfp/contest_results.htm), Greg?
>

Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[Stefan Monnier]

>>>>> "David" == David McClain <dmcclain@azstarnet.com> writes:
> Could you provide a reference to de Bruijin indexing? I recall reading about

On a related note, how would that compare (performancewise) to an
approach like "abstract syntax" (represent a function not
as (<id>, <exp>) and neither as <exp> (as in the case of deBruijn)
but as fn x => <exp>) ?


        Stefan

Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[Xavier Leroy]

David McClain asks:

> Could you provide a reference to de Bruijin indexing? I recall reading about
> it some time ago, and after having searched my books here, I cannot find any
> references to it.

The idea behind de Bruijn indices is to represent variable references
not by name, but by the number of binders to cross to get at the
binder for the variable in question.  An example shoud make this
clearer:

        fun x -> fun y -> x + y

is represented in de Bruijn notation as

        fun -> fun -> var1 + var0

"var1" means "go up one binder", so this refers to the variable bound
by the first "fun".
"var0" means "go to the closest binder", so this refers to the
variable bound by the second "fun".

Notice that a de Bruijn index is relative to the position of the
variable reference.  Hence the same variable can be referenced by
different de Bruijn indices depending on context, e.g.

        fun x -> print_int x; fun y -> x + y

becomes
        fun -> print_int var0; fun -> var1 + var0
                         ^^^^         ^^^^
                       this is x     this is x too!

De Bruijn indices are interesting for several reasons.  One is
that they totally eliminate any alpha-conversion problems: expressions
have unique representations, without any need to work modulo renaming of
bound variables; moreover, substitution of variables by non-closed
expressions works very well, without any risk of name clashes as in
the normal, name-based notation.

Another reason is that if you represent the evaluation environment as
a stack, with each new binding simply pushing the bound value on top,
then the de Bruijn index for a variable is simply the position of the
variable's value in the stack, relative to the top of the stack.
(Substitute "list" for "stack" to deal with persistent, heap-allocated
environments, e.g. for closures.)  This leads to very simple
translations into abstract machine code.

Stefan Monnier asks:

> On a related note, how would that compare (performancewise) to an
> approach like "abstract syntax" (represent a function not
> as (<id>, <exp>) and neither as <exp> (as in the case of deBruijn)
> but as fn x => <exp>) ?

My feeling is that higher-order abstract syntax isn't applicable to
the GML language, because the language has variable assignment, which
I don't see how to fit in the h.o.a.s. representation.

- Xavier Leroy

Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[eijiro_sumii]

> > Could you provide a reference to de Bruijin indexing?

Xavier kindly gave a nice explanation.:) Thanks!

> On a related note, how would that compare (performancewise) to an
> approach like "abstract syntax" (represent a function not
> as (<id>, <exp>) and neither as <exp> (as in the case of deBruijn)
> but as fn x => <exp>) ?

As far as I know, to use that "higher-order abstract syntax" approach,
we have to _translate_ a GML program into a Caml code and evaluate it
at runtime.  That is exactly what I did in the "compiling" version
(PLClubCN) of our entry, but it didn't work well because the
compilation itself (including ocamlopt.opt) took some time, which
didn't pay.

Eijiro

automatic translation in Team PLClub ICFP'2000 entry

[Julian Assange]

> compilation itself (including ocamlopt.opt) took some time, which
> didn't pay.

There must be an adapative break even point though. e.g if you're
n/m pixils done in s seconds, and the average cost of compilation
is c times the simple rendering speed per line and the average speedup
is q, then subtracting the pixils already done, work out whether

	(m-n) * p < c*lines*p' + (m-n)*p*q
	where
		p = (m-n)/s 		rendering speed
		p' =			simple rendering speed (speed of
					a delay loop or uncomplicated pixel etc)
					

		
And if so, compile.

Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[Pierre Weis]

Xavier explained de Bruijn indices

> Notice that a de Bruijn index is relative to the position of the
> variable reference.  Hence the same variable can be referenced by
> different de Bruijn indices depending on context, e.g.
> 
>         fun x -> print_int x; fun y -> x + y
> 
> becomes
>         fun -> print_int var0; fun -> var1 + var0
>                          ^^^^         ^^^^
>                        this is x     this is x too!
> 
> De Bruijn indices are interesting for several reasons.  One is
> that they totally eliminate any alpha-conversion problems: expressions
> have unique representations, without any need to work modulo renaming of
> bound variables; moreover, substitution of variables by non-closed
> expressions works very well, without any risk of name clashes as in
> the normal, name-based notation.
> 
> Another reason is that if you represent the evaluation environment as
> a stack, with each new binding simply pushing the bound value on top,
> then the de Bruijn index for a variable is simply the position of the
> variable's value in the stack, relative to the top of the stack.
> (Substitute "list" for "stack" to deal with persistent, heap-allocated
> environments, e.g. for closures.)  This leads to very simple
> translations into abstract machine code.

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

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

- 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. As an example, consider
the parallel (or multiple) beta-reduction: the problem is to calculate
f e1 e2 ... en by substituting e1 e2 ... en, in the body of f,
supposed to be defined by lambda expression with n binders fun -> fun
-> ... -> body. The problem is to perform the reduction in one pass on
the body of f. This operation is trivial if you use a conventional
beta reducer, but it is surprisingly difficult if you use De Bruijn
indices.

- as a consequence of these two properties, debugging code that
manipulates and transforms lambda code in De Bruijn form is just a
nightmare (each time I had to do it, I ended by writing a
pretty-printer that reverts De Bruijn notation to good old names for
variables!)

That's why I consider a ``tour de force'' the Caml Light compiler that
uses De Bruijn indices for the whole language. However, remember the
famous ``De Bruijn wins again!'' leitmotiv we used to ear in the
building when someone was desesperately fighting with wrong indices
generated by the compiler!

Also consider that the Caml Light compiler does not optimize and
symbolycally manipulate programs: that's devoted to the next ``tour de
force'', the Objective Caml optimizing compiler, which does not use
the De Bruijn indices notation for lambda terms...

Pierre Weis

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

Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[Markus Mottl]

On Sat, 07 Oct 2000, Pierre Weis wrote:
> Also consider that the Caml Light compiler does not optimize and
> symbolycally manipulate programs: that's devoted to the next ``tour de
> force'', the Objective Caml optimizing compiler, which does not use
> the De Bruijn indices notation for lambda terms...

This sounds interesting! - May I ask what optimisations are considered?
Will there be documentation for the (new) intermediate representation on
which optimisations operate? It would be really important to have
information about side effects there, too.

I could imagine playing around with such representations in LambdaProlog
(extremely convenient for prototyping transformation systems). I don't know
whether anything useful will come out, but it may be fun - for others as
well.

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[Pierre Weis]

> Markus Mottl wrote:

> On Sat, 07 Oct 2000, Pierre Weis wrote:
> > Also consider that the Caml Light compiler does not optimize and
> > symbolycally manipulate programs: that's devoted to the next ``tour de
> > force'', the Objective Caml optimizing compiler, which does not use
> > the De Bruijn indices notation for lambda terms...
> 
> This sounds interesting! - May I ask what optimisations are considered?

Classical: inlining, type-directed optimizations for primitives,
compile time beta-reductions, constant folding, ...

A bit more hairy: direct calls to functions (including curried
functions and functions whose argument is a tuple), 0-cfa like
analysis to access globals in modules, ...

Xavier is the right man to tell you what's going on inside the compiler,
but you can also read the compiler's source files ...

> Will there be documentation for the (new) intermediate representation on
> which optimisations operate? It would be really important to have
> information about side effects there, too.

Yes, you need a purity analysis for some of those optimizations...

> I could imagine playing around with such representations in LambdaProlog
> (extremely convenient for prototyping transformation systems). I don't know
> whether anything useful will come out, but it may be fun - for others as
> well.

I'm sure many people will be interested at reading your code and
conclusions about implementing transformations in Lambdaprolog ...

Best regards,

Pierre Weis

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

Re: automatic translation in Team PLClub ICFP'2000 entry

[eijiro_sumii]

> > compilation itself (including ocamlopt.opt) took some time, which
> > didn't pay.
> 
> There must be an adapative break even point though. e.g if you're
...
> And if so, compile.

Right, I actually tried that, but the "even point" was too high -- as
I wrote in our web page, my translator produced too complex Caml
programs, and ocaml{c,opt}{,.opt} often aborted after several minutes,
saying "out of registers" or "out of memory" or something like that...
I should probably have modified the translator to produce simpler
programs, but I didn't have the time to do that.

Eijiro

Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[John Max Skaller]

Pierre Weis wrote:

> the body of f. This operation is trivial if you use a conventional
> beta reducer, but it is surprisingly difficult if you use De Bruijn
> indices.

	Just out of curiousity, what do you mean
by a 'difficult' algorithm?

	To explain my question in slightly more depth: given
some fixed problems with known algorithms, all these algorithms,
in the first instance, have equal 'difficulty', namely,  'trivial':
if the algorithm is known, it can be implemented. (In general,
coding a known algorithm is so easy compared with other programming
tasks that I would classify coding by how laborious it is: the only
'difficulty' involved is staying awake long enough to finish the job :-)

	It is sometimes difficult to _find_ an algorithm for a problem,
and one may say that some algorithms are 'inflexible' in the sense
that small variations in the problem make finding a solution
by considering the 'original' algorithm difficult.

	It may also be hard to tranform a correct algorithm into
a more efficient version.

	Also, it is clear that some algorithms are difficult to
understand. And, some algorithms, coded incorrectly, may be difficult
to debug.
 
-- 
John (Max) Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
checkout Vyper http://Vyper.sourceforge.net
download Interscript http://Interscript.sourceforge.net

Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[Benjamin Pierce]

Fanning the fire on deBruijn indices...

> - 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. As an example, consider
> ...

There's an important difference, though, in the ways that these errors
show up: bugs in deBruijn-indexing schemes tend to manifest immediately
and catastrophically -- if you miss a 'shift' everything quickly gets all
screwed up and you can see that you did something wrong and fix it right
away -- while name-based implementations of substitution tend to fail
only six months later, when someone makes an unlucky choice of variable
names. 

There's a story that a substitution bug in the original LCS theorem
prover persisted for six *years* before anybody noticed...

> - as a consequence of these two properties, debugging code that
> manipulates and transforms lambda code in De Bruijn form is just a
> nightmare (each time I had to do it, I ended by writing a
> pretty-printer that reverts De Bruijn notation to good old names for
> variables!)

I usually do this too.  The pretty-printer can also do a little
consistency checking on the deBruijn indices: each variable is
represented as a pair of its index and the expected size of the context;
if the printing routine sees that the actual context does not have this
size, it complains.  

One drawback of deBruijn indices that you did not mention is that, at
least when implemented naively, they are pretty expensive in terms of
the amount of consing that's required to perform substitutions. 

At the end of the day, I'm not that big a fan of *either* deBruijn or
named presentations of terms... both are pretty ugly to work with, in
different ways.  In fact, I find both distressing and fascinating that,
after so many years of thought by so many smart people, we're still in
such an unsatisfactory state wrt. binding.

    B

de Bruijn indices (Re: WWW Page of Team PLClub)

[Eijiro Sumii]

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

Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)

[Pierre Weis]

> Pierre Weis wrote:
> 
> > the body of f. This operation is trivial if you use a conventional
> > beta reducer, but it is surprisingly difficult if you use De Bruijn
> > indices.
> 
> 	Just out of curiousity, what do you mean
> by a 'difficult' algorithm?

I did not mention the word algorithm. I meant here that implementing
the parallel beta-reduction is not a trivial kind of iteration (map or
fold) on the basic one step beta-reducer (if you do want to obtain a
one pass reduction).

BTW (joking):

Definition: an algorithm is said to be difficult iff it it not
trivial to implement in Caml !

> 	To explain my question in slightly more depth: given
> some fixed problems with known algorithms, all these algorithms,
> in the first instance, have equal 'difficulty', namely,  'trivial':
> if the algorithm is known, it can be implemented. (In general,
> coding a known algorithm is so easy compared with other programming
> tasks that I would classify coding by how laborious it is: the only
> 'difficulty' involved is staying awake long enough to finish the job :-)

So, let's me tell a story about this ``difficult'' problem: having
problems to implement the parallel beta-reduction using the De Bruijn
indices, I looked in the litterature and found a thesis that claimed
to specify this transformation and used it in the rest of the
thesis. So, I turned the specification into a piece of Caml program;
it gave wrong answers. Fortunately, I had the thesis's author at hand;
hence, we sat together at the terminal and double-checked the
implementation wrt the specification; we were not able to find any
discrepancy in the program; then we changed the specification; then we
changed the program accordingly; it was still giving wrong answers on
some examples!

I gave up, and revert to multiple calls to the beta-reducer (and
accordingly to inefficient multiple rewritings of the function body).

I do not claim this problem is impossible to solve; I just claimed it
is ``surprisingly difficult'' compared to the trivial solution you
give to the same problem when you use a conventional beta-reducer.  It
is at least so difficult that a carefully written thesis may give a
wrong specification of the solution, even if it has been reviewed by
experts of the domain.

I think the De Bruijn indices solution to this problem may not be
worth the efforts it needs.

> 	It is sometimes difficult to _find_ an algorithm for a problem,
> and one may say that some algorithms are 'inflexible' in the sense
> that small variations in the problem make finding a solution
> by considering the 'original' algorithm difficult.

That's exactly what I observed for parallel beta-reduction in one pass.

> 	It may also be hard to tranform a correct algorithm into
> a more efficient version.

That's exactly the intention in using parallel beta-reduction in one pass.

> 	Also, it is clear that some algorithms are difficult to
> understand. And, some algorithms, coded incorrectly, may be difficult
> to debug.

Also true with De Bruijn indices transformations.

So, this problem meets all your criteria: that's why I think we can
say ``it is a surprisingly difficult problem''.

Pierre Weis

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

Re: de Bruijn indices (Re: WWW Page of Team PLClub)

[Pierre Weis]

> 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/

Re: de Bruijn indices

[Gerard Huet]

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. 

Gérard

Re: de Bruijn indices

[Chet Murthy]

>>>>> "GH" == Gerard Huet <Gerard.Huet@inria.fr> writes:

    GH> 1. They lead to efficient implementations. My original
    GH> implementation of the constructive engine in Coq's early
    GH> versions used de Bruijn indices, and performed reasonably
    GH> well. It leads to a completely applicative implementation of
    GH> lambda-calculus, and the cost of lifting may be reduced by
    GH> Okasaki-like data structures. I still remember the day when
    GH> this super-hacker declared that he was going to replace all
    GH> this inefficient stuff by slick hashtables - only to undo
    GH> everything 2 months later because he was 30% slower.

It turns out that deBruijn indices are *significantly* more efficient
than explicit names.  Moreover, the renaming operations that must be
introduced to use explicit names are essentially the same as the
"lifting", etc, operations used in deBruijn indices.

I once modified Coq to use explicit names, and after spending a month
or so, trying to make it as fast as Coq with deBruijn indices,
switched back.

That experiment, and finding that every _single_ avenue for improved
performance, with explicit names, was a dead end, pretty much
convinced me that deBruijn indices are much faster.

Also, regarding human-readability, I think it is a red herring to ask
whether the term Lambda("x",Ref 2) (which corresponds to something
like ("lambda x. y") is more readable than Lambda("x",Var "y").

In both cases, without the "environment" that binds free variables to
values, types, or "meanings" of some sort, the meaning of the term is
undefined.  So we need to keep these environments around, and once we
have them, well, we can always just lookup the name, if want it.

Moreover, it is only during debugging that having the "explicit name"
actually buys us anything in readability.  At runtime, if the program
ever prints out something, it does so with respect to this
"environment", so there's always a good name to use.  If it is
manipulating terms, well, it couldn't very well use the name for
anything other than a lookup, since even in explicit names, the name
can be modified, e.g. by alpha-conversion.

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.

--chet--

Re: de Bruijn indices

[John Max Skaller]

Chet Murthy wrote:
> 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)

Actually, if you multiply the size of Coq by 10, to get the equivalent
size for a C/C++ program, it isn't that small by commercial standands
either. :-)

-- 
John (Max) Skaller, mailto:skaller@maxtal.com.au
10/1 Toxteth Rd Glebe NSW 2037 Australia voice: 61-2-9660-0850
checkout Vyper http://Vyper.sourceforge.net
download Interscript http://Interscript.sourceforge.net

Re: de Bruijn indices

[John R Harrison]

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.

Re: de Bruijn indices

[Trevor Jim]

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

Re: de Bruijn indices

[Benjamin C. Pierce]

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

This is pretty much how the Pict front end works.  We started out with a
standard deBruijn representation, but later switched to a scheme where,
during parsing, we choose a globally unique spelling for each bound name
(they're not *that* ugly).  We have to do a little work later to make
sure that uniqueness is maintained, but it seems faster on the whole.

       B
       
       

RE: de Bruijn indices

[Greg Morrisett]

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

But alpha-conversion is a form of substitution...  

> 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.
> 
> Of course, it would result in uggggggly names -- uglier than deBruijn
> numbers, unless similar tricks were played in pretty-printing.

This is essentially what we did in TAL -- each variable had
a string-based name and a number field.  Numbers defaulted
to zero (and weren't printed).  When we needed to alpha-convert 
something, we incremented a global counter and used this for
the new number (keeping the string the same.)  You do end
up with foo_12349 this way, but only if something has to be
alpha-converted -- and that turned out to be pretty rare.

Again, I haven't re-implemented things with De Bruijn, and
would like too.  It may be that TAL would run faster with
a well-implemented scheme.  

Two side notes:

1. The reason I can't easily re-implement TAL using de Bruijn
instead of explicit names, is that I exposed my term datatypes
to make pattern matching easy.  If I'd been coding in something
like Java, I suspect I would've abstracted terms enough that
re-writing the code would've been easier.  One problem with
ML is that the convenience of pattern matching tends to direct
you (or at least me) to expose too much representation information.
Abstract patterns would help a lot...

2. I seem to recall that there are subtle issues with
typed calculi (especially dependently-typed calculi) and
de Bruijn?  Certainly explicit substitutions are tricky
in this setting...

-Greg

Re: de Bruijn indices

[Chet Murthy]

>>>>> "GM" == Greg Morrisett <jgm@cs.cornell.edu> writes:

    GM> Well, I can say from my own experience that de Bruijn isn't
    GM> always best.  Neither NuPRL nor the TAL type-checker uses
    GM> indices, prefering named variables instead.  For both,
    GM> preserving original names is really useful when debugging.

I can't speak to TAL.  I _can_ speak for Nuprl, having implemented a
version of Nuprl in SML/NJ in 1990, and having re-implemented it, by a
process of iterative migration, in Coq, in 1992-1994.

Explicit names were *significantly* slower than deBruijn indices.  The
costs were there, even though I did the standard tricks of caching
free-vars under binders, and even though I wrote the most careful code
I could think of to make explicit names faster.

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.

Of course, it would result in uggggggly names -- uglier than deBruijn
numbers, unless similar tricks were played in pretty-printing.

--chet--

Re: de Bruijn indices

[Markus Mottl]

On Wed, 11 Oct 2000, Simon Peyton-Jones wrote:
> Indeed, if any participant of this discussion is so motivated, I would
> dearly love to publish a paper about the practical aspects of
> efficient management of substitution and bound variables in the
> Journal of Functional Programming.  It doesn't have to be a "new idea".
> Just articulating the unpublished experience and laying out design tradeoffs
> that we've seen in this discussion would be excellent. 

The developers of the Teyjus-implementation of LambdaProlog have tried
very hard to develop better ways of handling bindings, especially what
concerns higher-order unification - this is a highly performance-critical
aspect of LambdaProlog, which allows reasoning about higher-order abstract
syntax. They could surely contribute valuable input on their experience.
Some interesting papers on this topic can be found on their sites.

The main architects of Teyjus and LambdaProlog (Gopalan Nadathur and
Dale Miller):

  http://www-users.cs.umn.edu/~gopalan
  http://www.cse.psu.edu/~dale

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

RE: de Bruijn indices

[Simon Peyton-Jones]

| comparisons.  I really think the community needs a bunch
| of "systems" paper on this topic that do a careful examination 
| of the tradeoffs for important applications like type-checkers,
| compilers, and theorem provers.  Like realistic techniques
| for garbage collection, too much is locked in the brains of 
| implementors.

Indeed, if any participant of this discussion is so motivated, I would
dearly love to publish a paper about the practical aspects of
efficient management of substitution and bound variables in the
Journal of Functional Programming.  It doesn't have to be a "new idea".
Just articulating the unpublished experience and laying out design tradeoffs
that we've seen in this discussion would be excellent. 

Send me a paper!  (Or send it to Greg, who's also a JFP editor.)

Simon

Re: de Bruijn indices

[John R Harrison]

It's been interesting for me to see a discussion of de Bruijn versus
name-carrying term representations, since it's an issue I've spent some
time thinking about and on which I've changed my opinion at least once. The
different versions of the HOL theorem proving system:

  HOL88     - http://www.cl.cam.ac.uk/Research/HVG/FTP/#hol88
  hol90     - http://www.cl.cam.ac.uk/Research/HVG/FTP/#hol90
  HOL Light - http://www.cl.cam.ac.uk/users/jrh/hol-light/index.html
  hol98     - http://www.cl.cam.ac.uk/Research/HVG/FTP/#hol98

have gone through several different term representations over the years:

  HOL88     - name-carrying
  hol90     - name-carrying at first then de Bruijn
  HOL Light - de Bruijn at first then name-carrying
  hol98     - de Bruijn at first then explicit substitutions

The original HOL88 name-carrying implementation was probably inherited
from Edinburgh or Cambridge LCF. This was quite satisfactory, but over
the years several obscure bugs were found in variable renaming which
could have caused unsoundness, an embarrassment in a system that
stresses its logical consistency. To avoid having the soundness of the
system depend on tricky programming, hol90 changed to using a de Bruijn
representation.

However, all versions of HOL maintain an abstract type of terms with a
name-carrying interface, so the de Bruijn indices must be an internal
detail that is hidden from the user. This makes de Bruijn terms grossly
inefficient for very large abstraction-rich terms. The trivial operation
of recursively descending a term can involve a quadratic amount of work,
since each time a binder is traversed, a variable must be substituted
for a de Bruijn index throughout the body. For this reason, although I
was initially enthusiastic about de Bruijn terms, I rapidly decided they
didn't fit with the HOL worldview and changed HOL Light (my small clean
reimplementation of the system in CAML Light) back to a name-carrying
approach.

Very recently, Bruno Barras has been the driving force behind yet
another term representation for hol98 that admits an efficient ML-style
reduction algorithm. See:

  @INPROCEEDINGS{tphols2000-Barras,
        crossref        = "tphols2000",
        title           = "Programming and computing in {HOL}",
        author          = "Bruno Barras",
        pages           = "17--37"}

  @PROCEEDINGS{tphols2000,
        editor          = "M. Aagaard and J. Harrison",
        booktitle       = "Theorem Proving in Higher Order Logics:
                           13th International Conference, TPHOLs 2000",
        series          = "Lecture Notes in Computer Science",
        volume          = 1869,
        year            = 2000,
        publisher       = "Springer-Verlag"}

All of this goes to show that despite intensive activity in the field,
the basic question of the most appropriate term representation -- even
for a particular narrowly focused application -- is not yet clearly
agreed on.

Cheers,

John.

RE: de Bruijn indices

[Greg Morrisett]

Well, I can say from my own experience that de Bruijn 
isn't always best.  Neither NuPRL nor the TAL type-checker
uses indices, prefering named variables instead.  For
both, preserving original names is really useful when
debugging.  

When implementing TAL, I assumed de Bruijn would be faster,
since what we do is a lot of (a) comparisons between
terms, (b) lots of beta-reductions.  To make comparisons
go fast, it's important to make the common case pointer
equality.  Like Shao, we found hash consing to be very
effective for this.  

At first blush, it seems that using de Bruijn would be better 
in this situation, as any two alpha-equivalent terms will
hash-cons together.  However, it was fairly easy to arrange
most of the alpha-equivalent terms to use the same names
(TAL is the output of a compiler after all), so we could
get good hash-consing to start with -- all we had to do 
was preserve it.  Furthermore, there's the potential to get
more hash-consing with a named scheme.  For instance, for
(\y.\z.y z) and (\z.\y.y z), you can at least share the
"y z".  Not so for de Bruijn.

The way we made substitution work well and fast was, like
Simon, to keep track of the free variables of a term.  
(We computed this information lazily and then memoized it
in the term.)  Shao did something similar in the Flint
IL.  This had two effects:  one, we could minimize re-naming
bound variables, and two, we could cut off substitution
earlier.  I'm not sure how these optimizations translate
into a de Bruijn setting (I'm sure there's some way, but
I haven't thought it through.)

I also tried out a form of explicit substitutions with
the named scheme (Shao did this in the Flint IL), but
found that the overhead was not worth it.  I think in
part this was because we were forced to do deep
sub-type comparisons on terms, and hence, had to push
the substitutions down to the leaves.  I think if you
buy into de Bruijn, then you more or less have to buy
into explicit substitutions too.

On the other hand, we never got around to implementing
a de Bruijn version of the type-checker.  I would like
to do this someday and also try the higher-order abstract 
syntax tricks.

The folks at CMU are working on an interface that allows
you to choose which representation you want.  Like the
Flint folks and us, they hope to do some detailed
comparisons.  I really think the community needs a bunch
of "systems" paper on this topic that do a careful examination 
of the tradeoffs for important applications like type-checkers,
compilers, and theorem provers.  Like realistic techniques
for garbage collection, too much is locked in the brains of 
implementors.

-Greg

Re: de Bruijn indices

[Markus Mottl]

On Thu, 05 Oct 2000, Patrick M Doane wrote:
> You should take a look at Frank Pfenning's course notes for his class on
> Computation and Deduction. The chapter on compilation covers the use of de
> Bruijn indices as well some interesting judgements abouts the compilation
> process. This chapter is located at:

De Bruijn indices are, btw., also explained (and implemented) in the
tutorial "Functional Programming using Caml Light" in Chapter 12:

  http://caml.inria.fr/tutorial/index.html

People who are interested in optimum performance for handling bindings
might also want to try out Christophe Raffalli's "bindlib":

  http://www.lama.univ-savoie.fr/sitelama/Membres/pages_web/RAFFALLI/bindlib.html

It's said to be even more efficient.

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl

Re: de Bruijn indices

[Patrick M Doane]

> Could you provide a reference to de Bruijin indexing? I recall reading
> about it some time ago, and after having searched my books here, I
> cannot find any references to it. So I probably saw it in a paper some
> time ago... Anyway, I would be interested since I have an interpreter
> name-lookup problem heretoo.

You should take a look at Frank Pfenning's course notes for his class on
Computation and Deduction. The chapter on compilation covers the use of de
Bruijn indices as well some interesting judgements abouts the compilation
process. This chapter is located at:

  http://www.cs.cmu.edu/~fp/courses/comp-ded/notes/chap6.pdf

The rest of the course notes are excellent for those interested in
formally representing theorems about programming languages in a logical
framework. 

Patrick Doane