Defunctionalized interpreters for programming languages

ABSTRACT

This document illustrates how functional implementations of formal semantics (structural operational semantics, reduction semantics, small-step and big-step abstract machines, natural semantics, and denotational semantics) can be transformed into each other. These transformations were foreshadowed by Reynolds in "Definitional Interpreters for Higher-Order Programming Languages" for functional implementations of denotational semantics, natural semantics, and big-step abstract machines using closure conversion, CPS transformation, and defunctionalization. Over the last few years, the author and his students have further observed that functional implementations of small-step and of big-step abstract machines are related using fusion by fixed-point promotion and that functional implementations of reduction semantics and of small-step abstract machines are related using refocusing and transition compression. It furthermore appears that functional implementations of structural operational semantics and of reduction semantics are related as well, also using CPS transformation and defunctionalization. This further relation provides an element of answer to Felleisen's conjecture that any structural operational semantics can be expressed as a reduction semantics: for deterministic languages, a reduction semantics is a structural operational semantics in continuation style, where the reduction context is a defunctionalized continuation. As the defunctionalized counterpart of the continuation of a one-step reduction function, a reduction context represents the rest of the reduction, just as an evaluation context represents the rest of the evaluation since it is the defunctionalized counterpart of the continuation of an evaluation function.

REFERENCES

• 1: Mads Sig Ager. Partial Evaluation of String Matchers & Constructions of Abstract Machines. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, January 2006.
• 2: Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. From interpreter to compiler and virtual machine: a functional derivation. Research Report BRICS RS-03-14, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, March 2003.
• 3: Mads Sig Ager , Dariusz Biernacki , Olivier Danvy , Jan Midtgaard, A functional correspondence between evaluators and abstract machines, Proceedings of the 5th ACM SIGPLAN international conference on Principles and practice of declaritive programming, p.8-19, August 27-29, 2003, Uppsala, Sweden [doi>10.1145/888251.888254]
• 4: Mads Sig Ager , Olivier Danvy , Jan Midtgaard, A functional correspondence between call-by-need evaluators and lazy abstract machines, Information Processing Letters, v.90 n.5, p.223-232, 15 June 2004 [doi>10.1016/j.ipl.2004.02.012]
• 5: Mads Sig Ager , Olivier Danvy , Jan Midtgaard, A functional correspondence between monadic evaluators and abstract machines for languages with computational effects, Theoretical Computer Science, v.342 n.1, p.149-172, 6 September 2005 [doi>10.1016/j.tcs.2005.06.008]
• 6: Brian E. Aydemir, Aaron Bohannon, Matthew Fairbairn, J. Nathan Foster, Benjamin C. Pierce, Peter Sewell, Dimitrios Vytiniotis, Geoffrey Washburn, Stephanie Weirich, and Steve Zdancewic. Mechanized metatheory for the masses: The PoplMark challenge. In Joe Hurd and Thomas F. Melham, editors, Theorem Proving in Higher Order Logics, 18th International Conference, TPHOLs 2005, number 3603 in Lecture Notes in Computer Science, pages 50--65, Oxford, UK, August 2005. Springer.
• 7: Anindya Banerjee , Nevin Heintze , Jon G. Riecke, Design and Correctness of Program Transformations Based on Control-Flow Analysis, Proceedings of the 4th International Symposium on Theoretical Aspects of Computer Software, p.420-447, October 29-31, 2001
• 8: Małgorzata Biernacka. A Derivational Approach to the Operational Semantics of Functional Languages. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, January 2006.
• 9: Małgorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science, 1(2:5):1--39, November 2005. A preliminary version was presented at the Fourth ACM SIGPLAN Workshop on Continuations (CW'04).
• 10: Małgorzata Biernacka , Olivier Danvy, A concrete framework for environment machines, ACM Transactions on Computational Logic (TOCL), v.9 n.1, p.6-es, December 2007 [doi>10.1145/1297658.1297664]
• 11: Magorzata Biernacka , Olivier Danvy, A syntactic correspondence between context-sensitive calculi and abstract machines, Theoretical Computer Science, v.375 n.1-3, p.76-108, May, 2007 [doi>10.1016/j.tcs.2006.12.028]
• 12: Dariusz Biernacki. The Theory and Practice of Programming Languages with Delimited Continuations. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, December 2005.
• 13: Dariusz Biernacki and Olivier Danvy. From interpreter to logic engine by defunctionalization. In Maurice Bruynooghe, editor, Logic Based Program Synthesis and Transformation, 13th International Symposium, LOPSTR 2003, number 3018 in Lecture Notes in Computer Science, pages 143--159, Uppsala, Sweden, August 2003. Springer-Verlag.
• 14: John Clements , Matthias Felleisen, A tail-recursive machine with stack inspection, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.6, p.1029-1052, November 2004 [doi>10.1145/1034774.1034778]
• 15: W Clinger , D P Friedman , M Wand, A scheme for a higher-level semantic algebra, Algebraic methods in semantics, Cambridge University Press, New York, NY, 1986
• 16: William D. Clinger , Anne H. Hartheimer , Eric M. Ost, Implementation Strategies for First-Class Continuations, Higher-Order and Symbolic Computation, v.12 n.1, p.7-45, April 1999 [doi>10.1023/A:1010016816429]
• 17: P.-L. Curien, An abstract frame work for environment machines, Theoretical Computer Science, v.82 n.2, p.389-402, May 31, 1991 [doi>10.1016/0304-3975(91)90230-Y]
• 18: Olivier Danvy, Back to direct style, Science of Computer Programming, v.22 n.3, p.183-195, June 1994
• 19: Olivier Danvy, Formalizing Implementation Strategies for First-Class Continuations, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.88-103, April 02, 2000
• 20: Olivier Danvy. From reduction-based to reduction-free normalization. In Sergio Antoy and Yoshihito Toyama, editors, Proceedings of the Fourth International Workshop on Reduction Strategies in Rewriting and Programming (WRS'04), volume 124(2) of Electronic Notes in Theoretical Computer Science, pages 79--100, Aachen, Germany, May 2004. Elsevier Science. Invited talk.
• 21: Olivier Danvy. An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, University of Aarhus, Aarhus, Denmark, October 2006.
• 22: Olivier Danvy and Andrzej Filinski. Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science, 2(4):361--391, 1992.
• 23: Olivier Danvy , Jacob Johannsen, Inter-deriving Semantic Artifacts for Object-Oriented Programming, Proceedings of the 15th international workshop on Logic, Language, Information and Computation, July 01-04, 2008, Edinburgh, UK [doi>10.1007/978-3-540-69937-8_1]
• 24: Olivier Danvy and Kevin Millikin. Refunctionalization at work. Research Report BRICS RS-08-4, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, August 2007. To appear in Science of Computer Programming, extended version.
• 25: Olivier Danvy , Kevin Millikin, On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion, Information Processing Letters, v.106 n.3, p.100-109, April, 2008 [doi>10.1016/j.ipl.2007.10.010]
• 26: Olivier Danvy , Lasse R. Nielsen, Defunctionalization at work, Proceedings of the 3rd ACM SIGPLAN international conference on Principles and practice of declarative programming, p.162-174, September 05-07, 2001, Florence, Italy [doi>10.1145/773184.773202]
• 27: Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics. Research Report BRICS RS-04-26, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, November 2004. 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.
• 28: Olivier Danvy , Ulrik P. Schultz, Lambda-dropping: transforming recursive equations into programs with block structure, Theoretical Computer Science, v.248 n.1-2, p.243-287, October 2000 [doi>10.1016/S0304-3975(00)00054-2]
• 29: Matthias Felleisen, The calculi of lambda-nu-cs conversion: a syntactic theory of control and state in imperative higher-order programming languages, Indiana University, Indianapolis, IN, 1987
• 30: Matthias Felleisen and Matthew Flatt. Programming languages and lambda calculi. Unpublished lecture notes available at http://www.ccs.neu.edu/home/matthias/3810-w02/readings.html and last accessed in April 2008, 1989-2001.
• 31: Matthias Felleisen and Daniel P. Friedman. Control operators, the SECD machine, and the λ-calculus. In Martin Wirsing, editor, Formal Description of Programming Concepts III, pages 193--217. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986.
• 32: Paul Graunke , Robert Bruce Findler , Shriram Krishnamurthi , Matthias Felleisen, Automatically Restructuring Programs for the Web, Proceedings of the 16th IEEE international conference on Automated software engineering, p.211, November 26-29, 2001
• 33: Timothy G. Griffin, A formulae-as-type notion of control, Proceedings of the 17th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.47-58, December 1989, San Francisco, California, United States [doi>10.1145/96709.96714]
• 34: Bruce Duba , Robert Harper , David MacQueen, Typing first-class continuations in ML, Proceedings of the 18th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.163-173, January 21-23, 1991, Orlando, Florida, United States [doi>10.1145/99583.99608]
• 35: Christopher T. Haynes , Daniel P. Friedman , Mitchell Wand, Continuations and coroutines, Proceedings of the 1984 ACM Symposium on LISP and functional programming, p.293-298, August 06-08, 1984, Austin, Texas, United States [doi>10.1145/800055.802046]
• 36: R. Hieb , R. Kent Dybvig , Carl Bruggeman, Representing control in the presence of first-class continuations, Proceedings of the ACM SIGPLAN 1990 conference on Programming language design and implementation, p.66-77, June 1990, White Plains, New York, United States
• 37: Graham Hutton , Joel Wright, What is the meaning of these constant interruptions?, Journal of Functional Programming, v.17 n.6, p.777-792, November 2007 [doi>10.1017/S0956796807006363]
• 38: Jacob Johannsen. An investigation of Abadi and Cardelli's untyped calculus of objects. Master's thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, June 2008. BRICS research report RS-08-6.
• 39: Thomas Johnsson, Lambda lifting: transforming programs to recursive equations, Proc. of a conference on Functional programming languages and computer architecture, p.190-203, January 1985, Nancy, France
• 40: Gilles Kahn, Natural Semantics, Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, p.22-39, February 19-21, 1987
• 41: H. Abelson , R. K. Dybvig , C. T. Haynes , G. J. Rozas , N. I. Adams Iv , D. P. Friedman , E. Kohlbecker , G. L. Steele, Jr. , D. H. Bartley , R. Halstead , D. Oxley , G. J. Sussman , G. Brooks , C. Hanson , K. M. Pitman , M. Wand, Revised Report on the Algorithmic Language Scheme, Higher-Order and Symbolic Computation, v.11 n.1, p.7-105, August 1998 [doi>10.1023/A:1010051815785]
• 42: Jean-Louis Krivine, A call-by-name lambda-calculus machine, Higher-Order and Symbolic Computation, v.20 n.3, p.199-207, September 2007 [doi>10.1007/s10990-007-9018-9]
• 43: George Kuan , David MacQueen, Efficient type inference using ranked type variables, Proceedings of the 2007 workshop on Workshop on ML, October 05-05, 2007, Freiburg, Germany [doi>10.1145/1292535.1292538]
• 44: Jan Midtgaard. Transformation, Analysis, and Interpretation of Higher-Order Procedural Programs. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, June 2007.
• 45: Kevin Millikin. A Structured Approach to the Transformation, Normalization and Execution of Computer Programs. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, May 2007.
• 46: Johan Munk. A study of syntactic and semantic artifacts and its application to lambda definability, strong normalization, and weak normalization in the presence of state. Master's thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, May 2007. BRICS research report RS-08-3.
• 47: Lasse R. Nielsen. A denotational investigation of defunctionalization. Research Report BRICS RS-00-47, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, December 2000.
• 48: Lasse R. Nielsen. A study of defunctionalization and continuation-passing style. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-7.
• 49: Hanne Riis Nielson , Flemming Nielson, Semantics with applications: a formal introduction, John Wiley & Sons, Inc., New York, NY, 1992
• 50: Atsushi Ohori , Isao Sasano, Lightweight fusion by fixed point promotion, Proceedings of the 34th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 17-19, 2007, Nice, France
• 51: Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125--159, 1975.
• 52: Gordon D. Plotkin. A structural approach to operational semantics. Technical Report FN-19, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, September 1981.
• 53: François Pottier , Nadji Gauthier, Polymorphic typed defunctionalization and concretization, Higher-Order and Symbolic Computation, v.19 n.1, p.125-162, March 2006 [doi>10.1007/s10990-006-8611-7]
• 54: John C. Reynolds, Definitional interpreters for higher-order programming languages, Proceedings of the ACM annual conference, p.717-740, August 01-01, 1972, Boston, Massachusetts, United States [doi>10.1145/800194.805852]
• 55: John C. Reynolds, Definitional Interpreters Revisited, Higher-Order and Symbolic Computation, v.11 n.4, p.355-361, December 1998 [doi>10.1023/A:1010075320153]
• 56: Guy L. Steele, Jr., Rabbit: A Compiler for Scheme, Massachusetts Institute of Technology, Cambridge, MA, 1978
• 57: Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory, MIT Press, Cambridge, MA, 1977
• 58: Alan Turing. On computable numbers, with an application to the Entscheidungsproblem. Proceedings of the London Mathematical Society, 42(2):230--265, 1936-37. Corrections in Volume 43, pages 544-546, 1937.
• 59: Philip Wadler, The essence of functional programming, Proceedings of the 19th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-14, January 19-22, 1992, Albuquerque, New Mexico, United States [doi>10.1145/143165.143169]
• 60: Mitchell Wand, Continuation-Based Program Transformation Strategies, Journal of the ACM (JACM), v.27 n.1, p.164-180, Jan. 1980 [doi>10.1145/322169.322183]
• 61: Mitchell Wand, Deriving Target Code as a Representation of Continuation Semantics, ACM Transactions on Programming Languages and Systems (TOPLAS), v.4 n.3, p.496-517, July 1982 [doi>10.1145/357172.357179]
• 62: Mitchell Wand, Semantics-directed machine architecture, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.234-241, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582179]
• 63: Mitchell Wand, A semantic prototyping system, Proceedings of the 1984 SIGPLAN symposium on Compiler construction, p.213-221, June 17-22, 1984, Montreal, Canada
• 64: Mitchell. Wand, From interpreter to compiler: a representational derivation, on Programs as data objects, p.306-324, April 1986, Copenhagen, Denmark
• 65: Glynn Winskel, The formal semantics of programming languages: an introduction, MIT Press, Cambridge, MA, 1993

INDEX TERMS

Primary Classification:
  D. Software
  D.1 PROGRAMMING TECHNIQUES
      D.1.1 Applicative (Functional) Programming

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Semantics

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Design, Languages, Theory

Keywords:
big-step abstract machines, context-sensitive reduction semantics, continuations, cps transformation, defunctionalization, interruptions, natural semantics, reduction semantics, refocusing, small-step abstract machines, structural operational semantics