Advertisement

From Reduction-Based to Reduction-Free Normalization

  • Olivier Danvy
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5832)

Abstract

We document an operational method to construct reduction-free normalization functions. Starting from a reduction-based normalization function from a reduction semantics, i.e., the iteration of a one-step reduction function, we successively subject it to refocusing (i.e., deforestation of the intermediate successive terms in the reduction sequence), equational simplification, refunctionalization (i.e., the converse of defunctionalization), and direct-style transformation (i.e., the converse of the CPS transformation), ending with a reduction-free normalization function of the kind usually crafted by hand. We treat in detail four simple examples: calculating arithmetic expressions, recognizing Dyck words, normalizing lambda-terms with explicit substitutions and call/cc, and flattening binary trees.

The overall method builds on previous work by the author and his students on a syntactic correspondence between reduction semantics and abstract machines and on a functional correspondence between evaluators and abstract machines. The measure of success of these two correspondences is that each of the inter-derived semantic artifacts (i.e., man-made constructs) could plausibly have been written by hand, as is the actual case for several ones derived here.

Keywords

Abstract Syntax Abstract Machine Reduction Sequence Reduction Semantic Explicit Substitution 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    Abadi, M., Cardelli, L.: A Theory of Objects. Monographs in Computer Science. Springer, Heidelberg (1996)CrossRefzbMATHGoogle Scholar
  2. 2.
    Ager, M.S.: Partial Evaluation of String Matchers & Constructions of Abstract Machines. PhD thesis, BRICS PhD School, Department of Computer Science, Aarhus University, Aarhus, Denmark (January 2006)Google Scholar
  3. 3.
    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)Google Scholar
  4. 4.
    Ager, M.S., Danvy, O., Midtgaard, J.: A functional correspondence between call-by-need evaluators and lazy abstract machines. Information Processing Letters 90(5), 223–232 (2004); Extended version available as the research report BRICS RS-04-3MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    Ager, M.S., Danvy, O., Midtgaard, J.: A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theoretical Computer Science 342(1), 149–172 (2005); Extended version available as the research report BRICS RS-04-28 MathSciNetCrossRefzbMATHGoogle Scholar
  6. 6.
    Asai, K.: Binding-time analysis for both static and dynamic expressions. New Generation Computing 20(1), 27–51 (2002); A preliminary version is available in the proceedings of SAS 1999 (LNCS 1694)CrossRefzbMATHGoogle Scholar
  7. 7.
    Balat, V., Danvy, O.: Memoization in type-directed partial evaluation. In: Batory, D., Consel, C., Taha, W. (eds.) GPCE 2002. LNCS, vol. 2487, pp. 78–92. Springer, Heidelberg (2002)CrossRefGoogle Scholar
  8. 8.
    Bertot, Y.: Coq in a hurry. CoRR (May 2006), http://arxiv.org/abs/cs/0603118v2
  9. 9.
    Beylin, I., Dybjer, P.: Extracting a proof of coherence for monoidal categories from a proof of normalization for monoids. In: Berardi, S., Coppo, M. (eds.) TYPES 1995. LNCS, vol. 1158, pp. 47–61. Springer, Heidelberg (1996)CrossRefGoogle Scholar
  10. 10.
    Biernacka, M.: A Derivational Approach to the Operational Semantics of Functional Languages. PhD thesis, BRICS PhD School, Department of Computer Science, Aarhus University, Aarhus, Denmark (January 2006)Google Scholar
  11. 11.
    Biernacka, M., Biernacki, D., Danvy, O.: An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science 1(2:5), 1–39 (2005); A preliminary version was presented at the Fourth ACM SIGPLAN Workshop on Continuations (CW 2004)MathSciNetzbMATHGoogle Scholar
  12. 12.
    Biernacka, M., Danvy, O.: A concrete framework for environment machines. ACM Transactions on Computational Logic 9(1), Article #6, 1–30 (2007); Extended version available as the research report BRICS RS-06-3MathSciNetCrossRefzbMATHGoogle Scholar
  13. 13.
    Biernacka, M., Danvy, O.: A syntactic correspondence between context-sensitive calculi and abstract machines. Theoretical Computer Science 375(1-3), 76–108 (2007); Extended version available as the research report BRICS RS-06-18MathSciNetCrossRefzbMATHGoogle Scholar
  14. 14.
    Biernacka, M., Danvy, O.: Towards compatible and interderivable semantic specifications for the Scheme programming language, Part II: Reduction semantics and abstract machinesGoogle Scholar
  15. 15.
    Biernacki, D.: The Theory and Practice of Programming Languages with Delimited Continuations. PhD thesis, BRICS PhD School, Department of Computer Science, Aarhus University, Aarhus, Denmark (December 2005)Google Scholar
  16. 16.
    Biernacki, D., Danvy, O.: From interpreter to logic engine by defunctionalization. In: Bruynooghe, M. (ed.) LOPSTR 2004. LNCS, vol. 3018, pp. 143–159. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  17. 17.
    Church, A.: The Calculi of Lambda-Conversion. Princeton University Press, Princeton (1941)zbMATHGoogle Scholar
  18. 18.
    Clinger, W.: 2008 ACM SIGPLAN Workshop on Scheme and Functional Programming, Victoria, British Columbia (September 2008)Google Scholar
  19. 19.
    Curien, P.-L.: An abstract framework for environment machines. Theoretical Computer Science 82, 389–402 (1991)MathSciNetCrossRefzbMATHGoogle Scholar
  20. 20.
    Danvy, O.: Back to direct style. Science of Computer Programming 22(3), 183–195 (1994); A preliminary version was presented at the Fourth European Symposium on Programming (ESOP 1992)MathSciNetCrossRefzbMATHGoogle Scholar
  21. 21.
    Danvy, O.: From reduction-based to reduction-free normalization. In: Antoy, S., Toyama, Y. (eds.) Proceedings of the Fourth International Workshop on Reduction Strategies in Rewriting and Programming (WRS 2004), Aachen, Germany, May 2004. Electronic Notes in Theoretical Computer Science, vol. 124(2), pp. 79–100. Elsevier Science, Amsterdam (2004), Invited talkGoogle Scholar
  22. 22.
    Danvy, O.: On evaluation contexts, continuations, and the rest of the computation. In: Thielecke, H. (ed.) Proceedings of the Fourth ACM SIGPLAN Workshop on Continuations, CW 2004 (2004); Technical report CSR-04-1, Department of Computer Science, Queen Mary’s College, pp. 13–23, Venice, Italy (January 2004), Invited talkGoogle Scholar
  23. 23.
    Danvy, O.: A rational deconstruction of Landin’s SECD machine. In: Grelck, C., Huch, F., Michaelson, G.J., Trinder, P. (eds.) IFL 2004. LNCS, vol. 3474, pp. 52–71. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  24. 24.
    Danvy, O.: An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, Aarhus University, Aarhus, Denmark (October 2006)Google Scholar
  25. 25.
    Danvy, O.: Special Issue on the Krivine Abstract Machine, part I. Higher-Order and Symbolic Computation, vol. 20(3). Springer, Heidelberg (2007)Google Scholar
  26. 26.
    Danvy, O.: Defunctionalized interpreters for programming languages. In: Thiemann, P. (ed.) Proceedings of the 2008 ACM SIGPLAN International Conference on Functional Programming (ICFP 2008), SIGPLAN Notices, Victoria, British Columbia, September 2008, vol. 43(9), pp. 131–142. ACM Press, New York (2008), Invited talk Google Scholar
  27. 27.
    Danvy, O.: Towards compatible and interderivable semantic specifications for the Scheme programming language, Part I: Denotational semantics, natural semantics, and abstract machinesGoogle Scholar
  28. 28.
    Danvy, O., Dybjer, P. (eds.): Proceedings of the 1998 APPSEM Workshop on Normalization by Evaluation (NBE 1998), BRICS Note Series NS-98-8, Gothenburg, Sweden, May 1998. BRICS, Department of Computer Science. Aarhus University (1998), http://www.brics.dk/~nbe98/programme.html
  29. 29.
    Danvy, O., Filinski, A.: Abstracting control. In: Wand, M. (ed.) Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, Nice, France, June 1990, pp. 151–160. ACM Press, New York (1990)CrossRefGoogle Scholar
  30. 30.
    Danvy, O., Filinski, A.: Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science 2(4), 361–391 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  31. 31.
    Danvy, O., Johannsen, J.: Inter-deriving semantic artifacts for object-oriented programming. In: Hodges, W., de Queiroz, R. (eds.) Logic, Language, Information and Computation. LNCS (LNAI), vol. 5110, pp. 1–16. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  32. 32.
    Danvy, O., Lawall, J.L.: Back to direct style II: First-class continuations. In: Clinger, W. (ed.) Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, LISP Pointers, San Francisco, California, June 1992, vol. V(1), pp. 299–310. ACM Press, New York (1992)CrossRefGoogle Scholar
  33. 33.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  34. 34.
    Danvy, O., Millikin, K.: A rational deconstruction of Landin’s SECD machine with the J operator. Logical Methods in Computer Science 4(4:12), 1–67 (2008)MathSciNetzbMATHGoogle Scholar
  35. 35.
    Danvy, O., Millikin, K.: Refunctionalization at work. Science of Computer Programming 74(8), 534–549 (2009); Extended version available as the research report BRICS RS-08-04MathSciNetCrossRefzbMATHGoogle Scholar
  36. 36.
    Danvy, O., Millikin, K., Nielsen, L.R.: On one-pass CPS transformations. Journal of Functional Programming 17(6), 793–812 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  37. 37.
    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-23Google Scholar
  38. 38.
    Danvy, O., Nielsen, L.R.: Refocusing in reduction semantics. Research Report BRICS RS-04-26, Department of Computer Science, Aarhus University, 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 Google Scholar
  39. 39.
    Felleisen, M.: The Calculi of λ-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages, PhD thesis. Computer Science Department, Indiana University, Bloomington, Indiana (August 1987)Google Scholar
  40. 40.
    Felleisen, M., Flatt, M.: Programming languages and lambda calculi (1989-2001), http://www.ccs.neu.edu/home/matthias/3810-w02/readings.html (last accessed in April 2008)
  41. 41.
    Felleisen, M., Friedman, D.P.: Control operators, the SECD machine, and the λ-calculus. In: Wirsing, M. (ed.) Formal Description of Programming Concepts III, pp. 193–217. Elsevier Science Publishers B.V (North-Holland), Amsterdam (1986)Google Scholar
  42. 42.
    Friedman, D.P., Wand, M.: Essentials of Programming Languages, 3rd edn. MIT Press, Cambridge (2008)zbMATHGoogle Scholar
  43. 43.
    Ganz, S.E., Friedman, D.P., Wand, M.: Trampolined style. In: Lee, P. (ed.) Proceedings of the 1999 ACM SIGPLAN International Conference on Functional Programming, Paris, France, September 1999. SIGPLAN Notices, vol. 34(9), pp. 18–27. ACM Press, New York (1999)Google Scholar
  44. 44.
    Hardin, T., Maranget, L., Pagano, B.: Functional runtime systems within the lambda-sigma calculus. Journal of Functional Programming 8(2), 131–172 (1998)MathSciNetCrossRefzbMATHGoogle Scholar
  45. 45.
    Hatcliff, J., Danvy, O.: Thunks and the λ-calculus. Journal of Functional Programming 7(3), 303–319 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  46. 46.
    Haynes, C.T., Friedman, D.P., Wand, M.: Continuations and coroutines. In: Steele Jr., G.L. (ed.) Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming, Austin, Texas, August 1984, pp. 293–298. ACM Press, New York (1984)CrossRefGoogle Scholar
  47. 47.
    Huet, G.: The zipper. Journal of Functional Programming 7(5), 549–554 (1997)MathSciNetCrossRefzbMATHGoogle Scholar
  48. 48.
    Johannsen, J.: An investigation of Abadi and Cardelli’s untyped calculus of objects. Master’s thesis, Department of Computer Science, Aarhus University, Aarhus, Denmark (June 2008); BRICS research report RS-08-6Google Scholar
  49. 49.
    Kahn, G.: Natural semantics. In: Brandenburg, F.-J., Vidal-Naquet, G., Wirsing, M. (eds.) STACS 1987. LNCS, vol. 247, pp. 22–39. Springer, Heidelberg (1987)Google Scholar
  50. 50.
    Kesner, D.: The theory of calculi with explicit substitutions revisited. In: Duparc, J., Henzinger, T.A. (eds.) CSL 2007. LNCS, vol. 4646, pp. 238–252. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  51. 51.
    Kinoshita, Y.: A bicategorical analysis of E-categories. Mathematica Japonica 47(1), 157–169 (1998)MathSciNetzbMATHGoogle Scholar
  52. 52.
    Lafont, Y.: Logiques, Catégories et Machines. PhD thesis, Université de Paris VII, Paris, France (January 1988)Google Scholar
  53. 53.
    Landin, P.J.: The mechanical evaluation of expressions. The Computer Journal 6(4), 308–320 (1964)CrossRefzbMATHGoogle Scholar
  54. 54.
    Marlow, S., Peyton Jones, S.L.: Making a fast curry: push/enter vs. eval/apply for higher-order languages. Journal of Functional Programming 16(4-5), 415–449 (2006); A preliminary version was presented at the 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP 2004) (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  55. 55.
    Martin-Löf, P.: About models for intuitionistic type theories and the notion of definitional equality. In: Proceedings of the Third Scandinavian Logic Symposium (1972). Studies in Logic and the Foundation of Mathematics, vol. 82, pp. 81–109. North-Holland, Amsterdam (1975)CrossRefGoogle Scholar
  56. 56.
    McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, part I. Communications of the ACM 3(4), 184–195 (1960)CrossRefzbMATHGoogle Scholar
  57. 57.
    Midtgaard, J.: Transformation, Analysis, and Interpretation of Higher-Order Procedural Programs. PhD thesis, BRICS PhD School, Aarhus University, Aarhus, Denmark (June 2007)Google Scholar
  58. 58.
    Millikin, K.: A Structured Approach to the Transformation, Normalization and Execution of Computer Programs. PhD thesis, BRICS PhD School, Aarhus University, Aarhus, Denmark (May 2007)Google Scholar
  59. 59.
    Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)Google Scholar
  60. 60.
    Morris, F.L.: The next 700 formal language descriptions. Lisp and Symbolic Computation 6(3/4), 249–258 (1993); Reprinted from a manuscript dated 1970MathSciNetCrossRefGoogle Scholar
  61. 61.
    Munk, J.: 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, Department of Computer Science, Aarhus University, Aarhus, Denmark (May 2007); BRICS research report RS-08-3Google Scholar
  62. 62.
    Nielsen, L.R.: A study of defunctionalization and continuation-passing style. PhD thesis, BRICS PhD School, Department of Computer Science, Aarhus University, Aarhus, Denmark (July 2001), BRICS DS-01-7Google Scholar
  63. 63.
    Ohori, A., Sasano, I.: Lightweight fusion by fixed point promotion. In: Felleisen, M. (ed.) Proceedings of the Thirty-Fourth Annual ACM Symposium on Principles of Programming Languages, Nice, France, January 2007. SIGPLAN Notices, vol. 42(1), pp. 143–154. ACM Press, New York (2007)Google Scholar
  64. 64.
    Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1, 125–159 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  65. 65.
    Plotkin, G.D.: A structural approach to operational semantics. Technical Report FN-19, Department of Computer Science, Aarhus University, Aarhus, Denmark, (September 1981); Reprinted in the Journal of Logic and Algebraic Programming 60-61, 17-139 (2004), with a foreword [66]Google Scholar
  66. 66.
    Plotkin, G.D.: The origins of structural operational semantics. Journal of Logic and Algebraic Programming 60-61, 3–15 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  67. 67.
    Reynolds, J.C.: Definitional interpreters for higher-order programming languages. In: Proceedings of 25th ACM National Conference, Boston, Massachusetts, pp. 717–740 (1972); Reprinted in Higher-Order and Symbolic Computation, vol. 11(4), pp. 363-397 (1998), with a foreword [68]Google Scholar
  68. 68.
    Reynolds, J.C.: Definitional interpreters revisited. Higher-Order and Symbolic Computation 11(4), 355–361 (1998)CrossRefzbMATHGoogle Scholar
  69. 69.
    Steele Jr., G.L.: Lambda, the ultimate declarative. AI Memo 379, Artificial Intelligence Laboratory, Cambridge, Massachusetts, November 1976. Massachusetts Institute of Technology (1976)Google Scholar
  70. 70.
    Steele Jr., G.L.: Rabbit: A compiler for Scheme. Master’s thesis, Artificial Intelligence Laboratory, Cambridge, Massachusetts, May 1978. Massachusetts Institute of Technology (1978); Technical report AI-TR-474 Google Scholar
  71. 71.
    Steele Jr., G.L., Sussman, G.J.: Lambda, the ultimate imperative. AI Memo 353, Artificial Intelligence Laboratory. Massachusetts Institute of Technology, Cambridge, Massachusetts (March 1976)Google Scholar
  72. 72.
    Stoy, J.E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge (1977)zbMATHGoogle Scholar
  73. 73.
    Xiao, Y., Sabry, A., Ariola, Z.M.: From syntactic theories to interpreters: Automating proofs of unique decomposition. Higher-Order and Symbolic Computation 14(4), 387–409 (2001)CrossRefzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

  • Olivier Danvy
    • 1
  1. 1.Department of Computer ScienceAarhus UniversityAarhus NDenmark

Personalised recommendations