Abstract:
Terms of the lambdacalculus 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 lambdacalculus 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 bottomup manner, thus avoiding combinatorial explosion in time required to search the term in a topdown 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 lambdacalculus (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 typemanipulation systems that may need to examine terms inbetween reductions  i.e., the "readback" problem for our representation is trivial.
Like Lamping graphs, and unlike director strings or the suspension lambdacalculus, the algorithm functions by sideeffecting 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.
