While classically lambda-expressions are seen as trees, people don't stop trying to use more general graphs for their representation (according to the authors, the ideas go back to Bourbaki in 1954).

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

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,

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 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 data

structure and algorithm is 180 lines of SML.

So it's efficient in both time and space, interactive, and simple to implement! What else is left to desire?

## Recent comments

20 min 57 sec ago

43 min 12 sec ago

1 hour 26 min ago

2 hours 22 min ago

2 hours 24 min ago

2 hours 57 min ago

4 hours 22 min ago

6 hours 56 min ago

9 hours 13 min ago

10 hours 50 min ago