Affiliations: College of Computer and Information Science, Northeastern University, 360 Huntington Avenue, Room 202 WVH, Boston, MA 02115, USA. [email protected] | College of Computer and Information Science, Northeastern University, 360 Huntington Avenue, Room 202 WVH, Boston, MA 02115, USA. [email protected]
Note: [] Address for correspondence: College of Computer and Information Science, Northeastern University, 360 Huntington Avenue, Room 202 WVH, Boston, MA 02115, USA
Abstract: If we represent a λ-calculus term as a DAG rather than a tree, we can efficiently represent the sharing that arises from β-reduction, thus avoiding combinatorial explosion in space. By adding uplinks from a child to its parents, we can efficiently implement β-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 β-reduction on λ-terms represented as uplinked DAGs; describe its proof of correctness; discuss its relation to alternate techniques such as Lamping graphs, explicit-substitution calculi 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 λ 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 data structure and algorithm is 180 lines of SML.
