Abstract
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. 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. 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, which we express as a reduction semantics. This store-based reduction semantics corresponds to a store-based abstract machine whose architecture 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Ager, M.S., Biernacki, D., Danvy, O., Midtgaard, J.: A functional correspondence between evaluators and abstract machines. In: Miller, D. (ed.) Proceedings of the Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP 2003), Uppsala, Sweden, August 2003, pp. 8–19. ACM Press, New York (2003)
Ariola, Z.M., Arvind: Properties of a first-order functional language with sharing. Theoretical Computer Science 146(1-2), 69–108 (1995)
Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. Journal of Functional Programming 7(3), 265–301 (1997)
Ariola, Z.M., Felleisen, M., Maraist, J., Odersky, M., Wadler, P.: A call-by-need lambda calculus. In: Lee, P. (ed.) Proceedings of the Twenty-Second Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, January 1995, pp. 233–246. ACM Press, New York (1995)
Ariola, Z.M., Klop, J.W.: Equational term graph rewriting. Fundamenta Informaticae 26(3/4), 207–240 (1996)
Barendregt, H.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundation of Mathematics, vol. 103, revised edition. North-Holland, Amsterdam (1984)
Barendregt, H.P., van Eekelen, M.C.J.D., Glauert, J.R.W., Kennaway, R., Plasmeijer, M.J., Sleep, M.R.: Term graph rewriting. In: de Bakker, J., Nijman, A.J., Treleaven, P.C. (eds.) PARLE 1987. LNCS, vol. 259, pp. 141–158. Springer, Heidelberg (1987)
Blom, S.: Term Graph Rewriting – Syntax and Semantics. PhD thesis, Institute for Programming Research and Algorithmics, Vrije Universiteit, Amsterdam, The Netherlands (Mar 2001)
Curry, H.B.: Apparent variables from the standpoint of Combinatory Logic. Annals of Mathematics 34, 381–404 (1933)
Danvy, O.: Defunctionalized interpreters for programming languages. In: Thiemann, P. (ed.) Proceedings of the 2008 ACM SIGPLAN International Conference on Functional Programming (ICFP 2008), Victoria, British Columbia, September 2008. SIGPLAN Notices, vol. 43(9), pp. 131–142. ACM Press, New York (2008) (invited talk)
Danvy, O.: From reduction-based to reduction-free normalization. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds.) AFP 2008. LNCS, vol. 5832, pp. 66–164. Springer, Heidelberg (2009)
Danvy, O., Millikin, K.: On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion. Information Processing Letters 106(3), 100–109 (2008)
Danvy, O., Millikin, K., Munk, J., Zerny, I.: Defunctionalized interpreters for call-by-need evaluation. In: Blume, M., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 240–256. Springer, Heidelberg (2010)
Danvy, O., Nielsen, L.R.: Defunctionalization at work. In: Søndergaard, H. (ed.) Proceedings of the Third International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP 2001), Firenze, Italy, September 2001, pp. 162–174. ACM Press, New York (2001); Extended version available as the research report BRICS RS-01-23
Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. Research Report BRICS RS-04-26, Department of Computer Science, Aarhus University, Aarhus, Denmark, A preliminary version appeared in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science, vol. 59.4 (November 2004)
Garcia, R., Lumsdaine, A., Sabry, A.: Lazy evaluation and delimited control. In: Pierce, B.C. (ed.) Proceedings of the Thirty-Sixth Annual ACM Symposium on Principles of Programming Languages, Savannah, GA, January 2009. SIGPLAN Notices, vol. 44(1), pp. 153–164. ACM Press, New York (2009)
Glauert, J.R.W., Kennaway, R., Sleep, M.R.: Dactl: An experimental graph rewriting language. In: Ehrig, H., Kreowski, H.-J., Rozenberg, G. (eds.) Graph Grammars 1990. LNCS, vol. 532, pp. 378–395. Springer, Heidelberg (1991)
Hatcliff, J., Danvy, O.: A generic account of continuation-passing styles. In: Boehm, H.-J. (ed.) Proceedings of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, Portland, Oregon, January 1994, pp. 458–471. ACM Press, New York (1994)
Hatcliff, J., Danvy, O.: A computational formalization for partial evaluation. Mathematical Structures in Computer Science, 507–541 (1997)
Jeffrey, A.: A fully abstract semantics for concurrent graph reduction. In: Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science, Paris, France, July 1994, pp. 82–91. IEEE Computer Society Press, Los Alamitos (1994)
Klop, J.W.: Combinatory Reduction Systems. Mathematical Centre Tracts, vol. 127. Mathematisch Centrum, Amsterdam (1980)
Koopman, P.W.M.: Functional Programs as Executable Specifications. PhD thesis, University of Nijmegen, Nijmegen, The Netherlands (1990)
Lawall, J.L., Mairson, H.G.: On global dynamics of optimal graph reduction. In: Tofte, M. (ed.) Proceedings of the 1997 ACM SIGPLAN International Conference on Functional Programming, Amsterdam, The Netherlands, June 1997. SIGPLAN Notices, vol. 32(8), pp. 188–195. ACM Press, New York (1997)
Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. Journal of Functional Programming 8(3), 275–317 (1998)
Nakata, K., Hasegawa, M.: Small-step and big-step semantics for call-by-need. Journal of Functional Programming 19(6), 699–722 (2009)
Peyton Jones, S.L.: The Implementation of Functional Programming Languages. Prentice Hall International Series in Computer Science. Prentice-Hall International, Englewood Cliffs (1987)
Plasmeijer, M.J., van Eekelen, M.C.J.D.: Functional Programming and Parallel Graph Rewriting. Addison-Wesley, Reading (1993)
Robinet, B.: Contribution à l’étude de réalités informatiques. Thèse d’état, Université Pierre et Marie Curie (Paris VI), Paris, France (May 1974)
Robinson, J.A.: A note on mechanizing higher order logic. In: Meltzer, B., Michie, D. (eds.) Machine Intelligence, vol. 5, pp. 123–133. Edinburgh University Press, Edinburgh (1969)
Turner, D.A.: A new implementation technique for applicative languages. Software—Practice and Experience 9(1), 31–49 (1979)
Zerny, I.: On graph rewriting, reduction and evaluation. In: Horváth, Z., Zsók, V., Achten, P., Koopman, P. (eds.) Trends in Functional Programming, Komárno, Slovakia, June 2009, vol. 10, Intellect Books, Bristol (2009); Granted the best student-paper award of TFP 2009 (to appear)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Danvy, O., Zerny, I. (2011). Three Syntactic Theories for Combinatory Graph Reduction. In: Alpuente, M. (eds) Logic-Based Program Synthesis and Transformation. LOPSTR 2010. Lecture Notes in Computer Science, vol 6564. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-20551-4_1
Download citation
DOI: https://doi.org/10.1007/978-3-642-20551-4_1
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-20550-7
Online ISBN: 978-3-642-20551-4
eBook Packages: Computer ScienceComputer Science (R0)