{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:22Z","timestamp":1750306762292,"version":"3.41.0"},"reference-count":36,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2013,11,1]],"date-time":"2013-11-01T00:00:00Z","timestamp":1383264000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100006785","name":"Google","doi-asserted-by":"publisher","id":[{"id":"10.13039\/100006785","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2013,11]]},"abstract":"<jats:p>\n            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\n            <jats:italic>upfront<\/jats:italic>\n            instead of\n            <jats:italic>on demand<\/jats:italic>\n            . 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\n            <jats:italic>coincides with that of Turner's original reduction machine.<\/jats:italic>\n            The three syntactic theories presented here therefore properly account for combinatory graph reduction As We Know It.\n          <\/jats:p>\n          <jats:p>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.<\/jats:p>","DOI":"10.1145\/2528932","type":"journal-article","created":{"date-parts":[[2013,12,4]],"date-time":"2013-12-04T14:04:47Z","timestamp":1386165887000},"page":"1-27","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Three syntactic theories for combinatory graph reduction"],"prefix":"10.1145","volume":"14","author":[{"given":"Olivier","family":"Danvy","sequence":"first","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ian","family":"Zerny","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2013,11,28]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888254"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00185-L"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002724"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"e_1_2_1_5_1","doi-asserted-by":"crossref","first-page":"3","DOI":"10.3233\/FI-1996-263401","article-title":"Equational term graph rewriting","volume":"26","author":"Ariola Z. M.","year":"1996","unstructured":"Ariola , Z. M. and Klop , J. W. 1996 . Equational term graph rewriting . Fundamenta Informaticae 26 , 3 -- 4 , 207--240. Ariola, Z. M. and Klop, J. W. 1996. Equational term graph rewriting. Fundamenta Informaticae 26, 3--4, 207--240.","journal-title":"Fundamenta Informaticae"},{"key":"e_1_2_1_6_1","series-title":"Studies in Logic and the Foundation of Mathematics Series","volume-title":"The Lambda Calculus: Its Syntax and Semantics Revised Ed","author":"Barendregt H.","unstructured":"Barendregt , H. 1984. The Lambda Calculus: Its Syntax and Semantics Revised Ed . Studies in Logic and the Foundation of Mathematics Series , vol. 103 . North-Holland . Barendregt, H. 1984. The Lambda Calculus: Its Syntax and Semantics Revised Ed. Studies in Logic and the Foundation of Mathematics Series, vol. 103. North-Holland."},{"key":"e_1_2_1_7_1","volume-title":"Parallel Languages","author":"Barendregt H. P.","year":"1987","unstructured":"Barendregt , H. P. , Van Eekelen , M. C. J. D. , Glauert , J. R. W. , Kennaway , R. , Plasmeijer , M. J. , and Sleep , M. R . 1987 . Term graph rewriting. In PARLE, Parallel Architectures and Languages Europe, Volume II : Parallel Languages , J. de Bakker, A. J. Nijman, and P. C. Treleaven, Eds., Lecture Notes in Computer Science, vol. 259, Springer , 141--158. Barendregt, H. P., Van Eekelen, M. C. J. D., Glauert, J. R. W., Kennaway, R., Plasmeijer, M. J., and Sleep, M. R. 1987. Term graph rewriting. In PARLE, Parallel Architectures and Languages Europe, Volume II: Parallel Languages, J. de Bakker, A. J. Nijman, and P. C. Treleaven, Eds., Lecture Notes in Computer Science, vol. 259, Springer, 141--158."},{"key":"e_1_2_1_8_1","unstructured":"Biernacka M. Danvy O. and Blom S. 2001. Term graph rewriting -- Syntax and semantics. Ph.D. thesis Institute for Programming Research and Algorithmics Vrije Universiteit Amsterdam The Netherlands.  Biernacka M. Danvy O. and Blom S. 2001. Term graph rewriting -- Syntax and semantics. Ph.D. thesis Institute for Programming Research and Algorithmics Vrije Universiteit Amsterdam The Netherlands."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(91)90002-F"},{"key":"e_1_2_1_10_1","doi-asserted-by":"crossref","unstructured":"Chang S. Horn D. V. and \n      Felleisen M\n  . \n  2011\n  . Evaluating call by need on the control stack. In Proceedings of the 11th International Conference on Trends in Functional Programming. R. Page Z. Horvath and V. Zsok Eds. Lecture Notes in Computer Science vol. \n  6546 Springer 1--15.   Chang S. Horn D. V. and Felleisen M. 2011. Evaluating call by need on the control stack. In Proceedings of the 11 th International Conference on Trends in Functional Programming. R. Page Z. Horvath and V. Zsok Eds. Lecture Notes in Computer Science vol. 6546 Springer 1--15.","DOI":"10.1007\/978-3-642-22941-1_1"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.2307\/1968167"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1411204.1411206"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the 6th International Conference on Advanced Functional Programming (AFP'08)","volume":"5382","author":"Danvy O.","year":"2008","unstructured":"Danvy , O. 2008 b. From reduction-based to reduction-free normalization . In Proceedings of the 6th International Conference on Advanced Functional Programming (AFP'08) . P. Koopman, R. Plasmeijer, and D. Swierstra, Eds., Lecture Notes in Computer Science , vol. 5382 , Springer, 66--164. Danvy, O. 2008b. From reduction-based to reduction-free normalization. In Proceedings of the 6th International Conference on Advanced Functional Programming (AFP'08). P. Koopman, R. Plasmeijer, and D. Swierstra, Eds., Lecture Notes in Computer Science, vol. 5382, Springer, 66--164."},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2007.10.010"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12251-4_18"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2012.02.023"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/773184.773202"},{"key":"e_1_2_1_18_1","unstructured":"Danvy O. and Nielsen L. R. 2004. Refocusing in reduction semantics. Res. rep. BRICS RS-04-26 Department of Computer Science Aarhus University Aarhus Denmark. http:\/\/www.brics.dk\/RS\/04\/26\/BRICS-RS-04-26.pdf.  Danvy O. and Nielsen L. R. 2004. Refocusing in reduction semantics. Res. rep. BRICS RS-04-26 Department of Computer Science Aarhus University Aarhus Denmark. http:\/\/www.brics.dk\/RS\/04\/26\/BRICS-RS-04-26.pdf."},{"key":"e_1_2_1_19_1","first-page":"1","article-title":"Lambda-lifting in quadratic time","volume":"2004","author":"Danvy O.","year":"2004","unstructured":"Danvy , O. and Schultz , U. P. 2004 . Lambda-lifting in quadratic time . J. Funct. Logic Program. 2004 , 1 . http:\/\/danae.uni-muenster.de\/lehre\/kuchen\/JFLP\/. Danvy, O. and Schultz, U. P. 2004. Lambda-lifting in quadratic time. J. Funct. Logic Program. 2004, 1. http:\/\/danae.uni-muenster.de\/lehre\/kuchen\/JFLP\/.","journal-title":"J. Funct. Logic Program."},{"key":"e_1_2_1_20_1","doi-asserted-by":"crossref","unstructured":"Garcia R. Lumsdaine A. and Sabry A. 2010. Lazy evaluation and delimited control. Logical Methods Comput. Sci. 6 3:1 1--39.  Garcia R. Lumsdaine A. and Sabry A. 2010. Lazy evaluation and delimited control. Logical Methods Comput. Sci. 6 3:1 1--39.","DOI":"10.2168\/LMCS-6(3:1)2010"},{"key":"e_1_2_1_21_1","volume-title":"Dactl: An experimental graph rewriting language. In Proceedings of the 4th International Workshop on Graph-Grammars and Their Application to Computer Science. H. Ehrig, H.-J","author":"Glauert J. R. W.","year":"1990","unstructured":"Glauert , J. R. W. , Kennaway , R. , and Sleep , M. R . 1990 . Dactl: An experimental graph rewriting language. In Proceedings of the 4th International Workshop on Graph-Grammars and Their Application to Computer Science. H. Ehrig, H.-J . Kreowski, and G. Rozenberg, Eds., Lecture Notes in Computer Science Series, vol. 532 , Springer , New York, 378--395. Glauert, J. R. W., Kennaway, R., and Sleep, M. R. 1990. Dactl: An experimental graph rewriting language. In Proceedings of the 4th International Workshop on Graph-Grammars and Their Application to Computer Science. H. Ehrig, H.-J. Kreowski, and G. Rozenberg, Eds., Lecture Notes in Computer Science Series, vol. 532, Springer, New York, 378--395."},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178053"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129597002405"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1994.316084"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/5280.5292"},{"key":"e_1_2_1_26_1","volume-title":"Mathematical Centre Tracts","volume":"127","author":"Klop J. W.","year":"1980","unstructured":"Klop , J. W. 1980 . Combinatory reduction systems . Mathematical Centre Tracts , vol. 127 , Mathematisch Centrum, Amsterdam. Klop, J. W. 1980. Combinatory reduction systems. Mathematical Centre Tracts, vol. 127, Mathematisch Centrum, Amsterdam."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003037"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796809990219"},{"volume-title":"The Implementation of Functional Programming Languages","author":"Peyton Jones S. L.","key":"e_1_2_1_30_1","unstructured":"Peyton Jones , S. L. 1987. The Implementation of Functional Programming Languages . Prentice Hall International Series in Computer Science. Prentice-Hall International . Peyton Jones, S. L. 1987. The Implementation of Functional Programming Languages. Prentice Hall International Series in Computer Science. Prentice-Hall International."},{"volume-title":"Functional Programming and Parallel Graph Rewriting","author":"Plasmeijer M. J.","key":"e_1_2_1_31_1","unstructured":"Plasmeijer , M. J. and Van Eekelen , M. C. J. D. 1993. Functional Programming and Parallel Graph Rewriting . Addison-Wesley . Plasmeijer, M. J. and Van Eekelen, M. C. J. D. 1993. Functional Programming and Parallel Graph Rewriting. Addison-Wesley."},{"volume-title":"Department of Computer Science","author":"Plotkin G. D.","key":"e_1_2_1_32_1","unstructured":"Plotkin , G. D. 1981. A structural approach to operational semantics. Tech. rep. FN-19 , Department of Computer Science , Aarhus University , Aarhus, Denmark . Plotkin, G. D. 1981. A structural approach to operational semantics. Tech. rep. FN-19, Department of Computer Science, Aarhus University, Aarhus, Denmark."},{"key":"e_1_2_1_33_1","doi-asserted-by":"crossref","unstructured":"Plotkin G. D. 2004. The origins of structural operational semantics. J. Logic Algebraic Program. 60--61 3--15.  Plotkin G. D. 2004. The origins of structural operational semantics. J. Logic Algebraic Program. 60--61 3--15.","DOI":"10.1016\/j.jlap.2004.03.009"},{"volume-title":"Universit\u00e9 Pierre et Marie Curie (Paris VI)","author":"Robinet B.","key":"e_1_2_1_34_1","unstructured":"Robinet , B. 1974. Contribution \u00e0 l'\u00e9tude de r\u00e9alit\u00e9s informatiques. Th\u00e8se d'\u00e9tat , Universit\u00e9 Pierre et Marie Curie (Paris VI) , Paris, France . Robinet, B. 1974. Contribution \u00e0 l'\u00e9tude de r\u00e9alit\u00e9s informatiques. Th\u00e8se d'\u00e9tat, Universit\u00e9 Pierre et Marie Curie (Paris VI), Paris, France."},{"volume-title":"A note on mechanizing higher order logic. InMachine Intelligence","author":"Robinson J. A.","key":"e_1_2_1_35_1","unstructured":"Robinson , J. A. 1969. A note on mechanizing higher order logic. InMachine Intelligence , vol. 5 , B. Meltzer and D. Michie, Eds ., Edinburgh University Press , 123--133. Robinson, J. A. 1969. A note on mechanizing higher order logic. InMachine Intelligence, vol. 5, B. Meltzer and D. Michie, Eds., Edinburgh University Press, 123--133."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1002\/spe.4380090105"},{"volume-title":"Trends in Functional Programming","author":"Zerny I.","key":"e_1_2_1_37_1","unstructured":"Zerny , I. 2009. On graph rewriting, reduction and evaluation . In Trends in Functional Programming , vol. 10 , Z. Horvath, V. Zsok, P. Achten, and P. Koopman, Eds., Intellect Books , Komarno, Slovakia, 81--112. Zerny, I. 2009. On graph rewriting, reduction and evaluation. In Trends in Functional Programming, vol. 10, Z. Horvath, V. Zsok, P. Achten, and P. Koopman, Eds., Intellect Books, Komarno, Slovakia, 81--112."}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2528932","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2528932","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:45Z","timestamp":1750231725000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2528932"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,11]]},"references-count":36,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2013,11]]}},"alternative-id":["10.1145\/2528932"],"URL":"https:\/\/doi.org\/10.1145\/2528932","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2013,11]]},"assertion":[{"value":"2011-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2011-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-11-28","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}