Record Details

Bottom-Up beta-Substitution: Uplinks and lambda-DAGs

BRICS Report Series

View Archive Info
 
 
Field Value
 
Title Bottom-Up beta-Substitution: Uplinks and lambda-DAGs
 
Creator Shivers, Olin
Wand, Mitchell
 
Description 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. We 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.
 
Publisher Aarhus University
 
Contributor —
 
Date 2004-12-11
 
Type info:eu-repo/semantics/article
info:eu-repo/semantics/publishedVersion
—
 
Format application/pdf
 
Identifier https://tidsskrift.dk/brics/article/view/21863
10.7146/brics.v11i38.21863
 
Source BRICS Report Series; No 38 (2004): RS-38 Bottom-Up beta-Substitution: Uplinks and lambda-DAGs
BRICS Report Series; No 38 (2004): RS-38 Bottom-Up beta-Substitution: Uplinks and lambda-DAGs
1601-5355
0909-0878
 
Language eng
 
Relation https://tidsskrift.dk/brics/article/view/21863/19290
 
Rights Copyright (c) 2015 BRICS Report Series