Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

Browse thread
Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: 2000-10-10 (12:05)
From: Pierre Weis <Pierre.Weis@i...>
Subject: Re: de Bruijn indices (Re: WWW Page of Team PLClub)
> 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,,