Skip to main content
SpringerLink
Log in

From Reduction-Based to Reduction-Free Normalization

  • Chapter
Advanced Functional Programming (AFP 2008)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 5832))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abadi, M., Cardelli, L.: A Theory of Objects. Monographs in Computer Science. Springer, Heidelberg (1996)

    Book  MATH  Google Scholar 

  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. 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. 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-3

    Article  MathSciNet  MATH  Google Scholar 

  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

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  8. Bertot, Y.: Coq in a hurry. CoRR (May 2006), http://arxiv.org/abs/cs/0603118v2

  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)

    Chapter  Google Scholar 

  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. 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)

    MathSciNet  MATH  Google Scholar 

  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-3

    Article  MathSciNet  MATH  Google Scholar 

  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-18

    Article  MathSciNet  MATH  Google Scholar 

  14. Biernacka, M., Danvy, O.: Towards compatible and interderivable semantic specifications for the Scheme programming language, Part II: Reduction semantics and abstract machines

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  17. Church, A.: The Calculi of Lambda-Conversion. Princeton University Press, Princeton (1941)

    MATH  Google Scholar 

  18. Clinger, W.: 2008 ACM SIGPLAN Workshop on Scheme and Functional Programming, Victoria, British Columbia (September 2008)

    Google Scholar 

  19. Curien, P.-L.: An abstract framework for environment machines. Theoretical Computer Science 82, 389–402 (1991)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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 talk

    Google Scholar 

  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 talk

    Google Scholar 

  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)

    Chapter  Google Scholar 

  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. 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. 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. Danvy, O.: Towards compatible and interderivable semantic specifications for the Scheme programming language, Part I: Denotational semantics, natural semantics, and abstract machines

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  30. Danvy, O., Filinski, A.: Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science 2(4), 361–391 (1992)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Chapter  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    MathSciNet  MATH  Google Scholar 

  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-04

    Article  MathSciNet  MATH  Google Scholar 

  36. Danvy, O., Millikin, K., Nielsen, L.R.: On one-pass CPS transformations. Journal of Functional Programming 17(6), 793–812 (2007)

    Article  MathSciNet  MATH  Google Scholar 

  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-23

    Google Scholar 

  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. 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. 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. 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. Friedman, D.P., Wand, M.: Essentials of Programming Languages, 3rd edn. MIT Press, Cambridge (2008)

    MATH  Google Scholar 

  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. Hardin, T., Maranget, L., Pagano, B.: Functional runtime systems within the lambda-sigma calculus. Journal of Functional Programming 8(2), 131–172 (1998)

    Article  MathSciNet  MATH  Google Scholar 

  45. Hatcliff, J., Danvy, O.: Thunks and the λ-calculus. Journal of Functional Programming 7(3), 303–319 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  47. Huet, G.: The zipper. Journal of Functional Programming 7(5), 549–554 (1997)

    Article  MathSciNet  MATH  Google Scholar 

  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-6

    Google Scholar 

  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. 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)

    Chapter  Google Scholar 

  51. Kinoshita, Y.: A bicategorical analysis of E-categories. Mathematica Japonica 47(1), 157–169 (1998)

    MathSciNet  MATH  Google Scholar 

  52. Lafont, Y.: Logiques, Catégories et Machines. PhD thesis, Université de Paris VII, Paris, France (January 1988)

    Google Scholar 

  53. Landin, P.J.: The mechanical evaluation of expressions. The Computer Journal 6(4), 308–320 (1964)

    Article  MATH  Google Scholar 

  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)

    Article  MathSciNet  MATH  Google Scholar 

  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)

    Chapter  Google Scholar 

  56. McCarthy, J.: Recursive functions of symbolic expressions and their computation by machine, part I. Communications of the ACM 3(4), 184–195 (1960)

    Article  MATH  Google Scholar 

  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. 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. Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)

    Google Scholar 

  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 1970

    Article  MathSciNet  Google Scholar 

  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-3

    Google Scholar 

  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-7

    Google Scholar 

  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. Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1, 125–159 (1975)

    Article  MathSciNet  MATH  Google Scholar 

  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. Plotkin, G.D.: The origins of structural operational semantics. Journal of Logic and Algebraic Programming 60-61, 3–15 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  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. Reynolds, J.C.: Definitional interpreters revisited. Higher-Order and Symbolic Computation 11(4), 355–361 (1998)

    Article  MATH  Google Scholar 

  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. 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. 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. Stoy, J.E.: Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge (1977)

    MATH  Google Scholar 

  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)

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Aarhus University, Aabogade 34, DK, 8200, Aarhus N, Denmark

    Olivier Danvy

Authors
  1. Olivier Danvy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute for Computing and Information Sciences, Radboud University Nijmegen, Heijendaalseweg 135, 6525, Nijmegen, AJ, The Netherlands

    Pieter Koopman  & Rinus Plasmeijer  & 

  2. Department of Information and Computing Sciences, Utrecht Universiy, Padualaan 14, 3584, Utrecht, CH, The Netherlands

    Doaitse Swierstra

Rights and permissions

Reprints and permissions

Copyright information

© 2009 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Danvy, O. (2009). From Reduction-Based to Reduction-Free Normalization. In: Koopman, P., Plasmeijer, R., Swierstra, D. (eds) Advanced Functional Programming. AFP 2008. Lecture Notes in Computer Science, vol 5832. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-04652-0_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-04652-0_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-04651-3

  • Online ISBN: 978-3-642-04652-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation