Joint work with Olivier Danvy.

We present a purely syntactic theory of graph reduction for the canonical combinators S, K, and I, where graph vertices are represented with evaluation contexts and let expressions. We express this first syntactic theory as a storeless reduction semantics of combinatory terms. We then factor out the introduction of let expressions to denote as many graph vertices as possible *upfront* instead of *on demand*. The factored terms can be interpreted as term graphs in the sense of Barendregt et al. We express this second syntactic theory, which we prove equivalent to the first, as a storeless reduction semantics of combinatory term graphs. We then recast let bindings as bindings in a global store, thus shifting, in Strachey’s words, from denotable entities to storable entities. The store-based terms can still be interpreted as term graphs. We express this third syntactic theory, which we prove equivalent to the second, as a store-based reduction semantics of combinatory term graphs. We then refocus this store-based reduction semantics into a store-based abstract machine. The architecture of this store-based abstract machine *coincides with that of Turner’s original reduction machine*. The three syntactic theories presented here therefore properly account for combinatory graph reduction As We Know It.

These three syntactic theories scale to handling the Y combinator. This article therefore illustrates the scientific consensus of theoreticians and implementors about graph reduction: it is the same combinatory elephant.

Three Syntactic Theories for Combinatory Graph Reduction. ACM Transactions on Computational Logic. To appear. [BIB].

.
Three Syntactic Theories for Combinatory Graph Reduction. In María Alpuente, editor, Logic Based Program Synthesis and Transformation, 20th International Symposium, LOPSTR 2010, revised selected papers. LNCS, 6564, Springer, July 2010, 1–20. Invited talk. [DOI], [BIB], [PDF].

. Official website for LOPSTR’10.