Lambda the Ultimate

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?