From: Xavier Leroy <Xavier.Leroy@inria.fr>
To: David McClain <dmcclain@azstarnet.com>,
eijiro_sumii@anet.ne.jp, caml-list@inria.fr,
monnier+lists/caml/news/@RUM.CS.YALE.EDU
Subject: Re: WWW Page of Team PLClub (Re: ICFP programming contest: results)
Date: Fri, 6 Oct 2000 10:07:31 +0200 [thread overview]
Message-ID: <20001006100731.12927@pauillac.inria.fr> (raw)
In-Reply-To: <001f01c02eb7$b41c99c0$210148bf@dylan>; from David McClain on Thu, Oct 05, 2000 at 03:33:26AM -0700
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
next prev parent reply other threads:[~2000-10-07 7:37 UTC|newest]
Thread overview: 26+ messages / expand[flat|nested] mbox.gz Atom feed top
2000-10-05 10:33 David McClain
2000-10-05 20:20 ` Stefan Monnier
2000-10-06 19:26 ` eijiro_sumii
2000-10-07 8:19 ` automatic translation in Team PLClub ICFP'2000 entry Julian Assange
2000-10-07 16:30 ` eijiro_sumii
2000-10-06 8:07 ` Xavier Leroy [this message]
2000-10-07 8:35 ` WWW Page of Team PLClub (Re: ICFP programming contest: results) Pierre Weis
2000-10-07 9:55 ` Markus Mottl
2000-10-07 10:24 ` Pierre Weis
2000-10-08 21:26 ` John Max Skaller
2000-10-10 10:23 ` Pierre Weis
2000-10-09 5:51 ` Benjamin Pierce
2000-10-09 7:19 ` de Bruijn indices (Re: WWW Page of Team PLClub) Eijiro Sumii
2000-10-10 10:36 ` Pierre Weis
2000-10-10 14:04 ` de Bruijn indices Gerard Huet
2000-10-10 17:29 ` Chet Murthy
2000-10-11 22:35 ` John Max Skaller
-- strict thread matches above, loose matches on Subject: below --
2000-10-05 22:46 WWW Page of Team PLClub (Re: ICFP programming contest: results) David McClain
2000-09-21 7:12 ICFP programming contest: results Xavier Leroy
2000-09-24 3:36 ` Eijiro Sumii
2000-10-04 18:40 ` WWW Page of Team PLClub (Re: ICFP programming contest: results) eijiro_sumii
2000-10-05 21:19 ` malc
2000-10-06 9:46 ` Julian Assange
2000-10-06 19:10 ` eijiro_sumii
2000-10-06 20:13 ` eijiro_sumii
2000-10-06 20:05 ` eijiro_sumii
[not found] ` <200010070759.JAA00538@pauillac.inria.fr>
2000-10-07 16:21 ` eijiro_sumii
2000-10-08 21:06 ` Pierre Weis
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=20001006100731.12927@pauillac.inria.fr \
--to=xavier.leroy@inria.fr \
--cc=caml-list@inria.fr \
--cc=dmcclain@azstarnet.com \
--cc=eijiro_sumii@anet.ne.jp \
--cc=monnier+lists/caml/news/@RUM.CS.YALE.EDU \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox