Term graph rewriting for implementing the λ-calculus refactored.

We retrace some history of using term graphs for implementing β-reduction in the λ-calculus. We refactor the following three high-lights from that history, illustrated by a prototype implementation:

• the classical (first) term graph implementation (Wadsworth), of β-reduction which we refactor through a term graph implementation G👁 of a well-behaved (e.g., orthogonal) class of TRSs 👁;
• implementing β-reduction through repeated weak-reduction (De Bruijn (Automath), Peyton Jones, Coquand, Grégoire & Leroy, Balabonski,...), which we show can be performed on 👁 through G👁
• implementing needed β-reduction (Huet & Lévy, Barendregt, Kennaway, Klop, Sleep,...) through a strategy for G👁 that we dub α-spine. By making use of union-find techniques for it, normal order reduction is shown to be linearly implementable.