Unlimp: Uniqueness as a Leitmotiv for Implementation

Stefan Kahrs

Abstract: When evaluation in functional programming languages is explained using lambda-calculus and/or term rewriting systems, expressions and function definitions are often defined as terms, that is as trees. Similarly, the collection of all terms is defined as a forest, that is a directed, acyclic graph where every vertex has at most one incoming edge. Concrete implementations usually drop the last restriction (and sometimes acyclicity as well), i.e. many terms can share a common subterm, meaning that different paths of subterm edges reach the same vertex in the graph. Any vertex in such a graph represents a term. A term is represented uniquely in such a graph if there are no two different vertices representing it. Such a representation can be established by using hash-consing for the creation of heap objects. We investigate the consequences of adopting uniqueness in this sense as a leitmotiv for implementation (called Unlimp), i.e. not allowing any two different vertices in a graph to represent the same term.

This file is a slightly modified version of the LFCS Technical Report. This version appeared in the Proceedings of the 4th International Symposium on Programming Language Implementation and Logic Programming, Leuven, August 1992. Pages 115-129. Editors M. Bruynooghe and M. Wirsing.

LFCS report ECS-LFCS-92-219, June 1992.

Previous | Index | Next