To: seminaire@pauillac.inria.fr
From: Didier.Remy@inria.fr
Subject: SEM - INRIA : Cristal - 17/12/04 - Paris - FR
Vous pouvez vous abonner à nos annonces de séminaires
http://pauillac.inria.fr/seminaires/subscribe.html
S E M I N A I R E
___ .
/ ___ __ /_ _ / /| /| _ __ __ _ _
/ / / /_ / __| / ----- / |/ | / \ /_ / / \ | / __|
|___ / / __/ |_ |_/ |_ / | |_/__/ |_ |_/ |/ |_/
I N R I A - Rocquencourt
Salle de conférence du Bat 8.
Vendredi 17 decembre, 10h30
------------
Olin Shivers
------------
=================================================
Bottom-up beta reduction: uplinks and lambda-DAGs
=================================================
Terms of the lambda-calculus are one of the most important data structures
we have in computer science. Among their uses are representing program
terms, advanced type systems, and proofs in theorem provers. Unfortunately,
heavy use of this data structure can become intractable in time and space;
the typical culprit is the fundamental operation of beta reduction.
If we represent a lambda-calculus term as a DAG rather than a tree, we can
efficiently represent the sharing that arises from beta reduction, thus
avoiding combinatorial explosion in space. By adding uplinks from a child to
its parents, we can efficiently implement beta reduction in a bottom-up
manner, thus avoiding combinatorial explosion in time required to search the
term in a top-down fashion.
I will present an algorithm for performing beta reduction on lambda terms
represented as uplinked DAGs; describe its proof of correctness; discuss its
relation to alternate techniques such as Lamping graphs, the suspension
lambda-calculus (SLC) and director strings; and present some timings of an
implementation.
Besides being both fast and parsimonious of space, the algorithm is
particularly suited to applications such as compilers, theorem provers, and
type-manipulation systems that may need to examine terms in-between
reductions -- i.e., the "readback" problem for our representation is
trivial.
Like Lamping graphs, and unlike director strings or the suspension
lambda-calculus, the algorithm functions by side-effecting the term
containing the redex; the representation is not a "persistent" one.
The algorithm additionally has the charm of being quite simple; a complete
implementation of the core data structures and algorithms is 180 lines of
fairly straightforward SML.