Three Syntactic Theories for Combinatory Graph Reduction

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperConference 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 syntactic theory as a reduction semantics, which we refocus into the first storeless abstract machine for combinatory graph reduction, which we refunctionalize into the first storeless natural semantics for combinatory graph reduction.We then factor out the introduction of let expressions to denote as many graph vertices as possible upfront instead of on demand, resulting in a second syntactic theory, this one of term graphs in the sense of Barendregt et al. The corresponding storeless abstract machine and natural semantics follow mutatis mutandis. We then interpret let expressions as operations over a global store (thus shifting, in Strachey's words, from denotable entities to storable entities), resulting in a third syntactic theory. The structure of the store-based abstract machine corresponding to this third syntactic theory oincides with that of Turner's original reduction machine. The three syntactic theories presented here The three syntactic heories presented here therefore have the following computational reality: they properly account for combinatory graph reduction As We Know It. We also outline how to extend the overall inter-derivation with the Y combinator.

Original languageEnglish
Book seriesLecture Notes in Computer Science
Pages (from-to)1-20
Number of pages20
Publication statusPublished - 2011
EventInternational Symposium onLogic-Based Program Synthesis andTransformation. LOPSTR 2010 - Castle of Hagenberg, Austria
Duration: 23 Jul 201025 Jul 2010
Conference number: 20


ConferenceInternational Symposium onLogic-Based Program Synthesis andTransformation. LOPSTR 2010
CityCastle of Hagenberg

Bibliographical note

Title of the vol.: Logic-Based Program Synthesis and Transformation. Proceedings / Maria Alpuente (ed.)
ISBN: 978-3-642-20550-7

See relations at Aarhus University Citationformats

ID: 22348890