Three Syntactic Theories for Combinatory Graph Reduction

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

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 rst 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
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 rst, 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
scientic consensus of theoreticians and implementors about graph reduction: it is the same combinatory
Original languageEnglish
Article number29
JournalA C M Transactions on Computational Logic
Number of pages28
Publication statusPublished - 2013

    Research areas

  • reduction-based normalization, reduction-free normalization, reduction semantics, abstract machines, reduction context, evaluation contexts, continuations, continuation-passing style (CPS, CPS transformation, defunctionalization, refunctionalization, refocusing

See relations at Aarhus University Citationformats

ID: 44466820