Bottom-Up beta-Substitution: 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.<br /> <br />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.<br /> <br />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.<br /> <br />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.<br /> <br />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. <br /> <br />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.