Advertisement

Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part I: Denotational Semantics, Natural Semantics, and Abstract Machines

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

Abstract

We derive two big-step abstract machines, a natural semantics, and the valuation function of a denotational semantics based on the small-step abstract machine for Core Scheme presented by Clinger at PLDI’98. Starting from a functional implementation of this small-step abstract machine, (1) we fuse its transition function with its driver loop, obtaining the functional implementation of a big-step abstract machine; (2) we adjust this big-step abstract machine so that it is in defunctionalized form, obtaining the functional implementation of a second big-step abstract machine; (3) we refunctionalize this adjusted abstract machine, obtaining the functional implementation of a natural semantics in continuation-passing style; and (4) we closure-unconvert this natural semantics, obtaining a compositional continuation-passing evaluation function which we identify as the functional implementation of a denotational semantics in continuation-passing style. We then compare this valuation function with that of Clinger’s original denotational semantics of Scheme.

Keywords

Operational Semantic Symbolic Computation Functional Programming Abstract Machine Denotational Semantic 
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.
    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
  2. 2.
    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
  3. 3.
    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-3Google Scholar
  4. 4.
    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)MathSciNetCrossRefzbMATHGoogle Scholar
  5. 5.
    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
  6. 6.
    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
  7. 7.
    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
  8. 8.
    Biernacka, M., Danvy, O.: Towards Compatible and Interderivable Semantic Specifications for the Scheme Programming Language, Part II: Reduction Semantics and Abstract Machines. In: Palsberg, J. (ed.) Mosses’s Festschrift. LNCS, vol. 5700, pp. 186–206. Springer, Heidelberg (2009)Google Scholar
  9. 9.
    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
  10. 10.
    Biernacki, D., Danvy, O.: From interpreter to logic engine by defunctionalization. In: Bruynooghe, M. (ed.) LOPSTR 2003. LNCS, vol. 3018, pp. 143–159. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  11. 11.
    Clinger, W., Friedman, D.P., Wand, M.: A scheme for a higher-level semantic algebra. In: Reynolds, J., Nivat, M. (eds.) Algebraic Methods in Semantics, pp. 237–250. Cambridge University Press, Cambridge (1985)Google Scholar
  12. 12.
    Clinger, W., Hartheimer, A.H., Ost, E.M.: Implementation strategies for first-class continuations. Higher-Order and Symbolic Computation 12(1), 7–45 (1999); A preliminary version was presented at the 1988 ACM Conference on Lisp and Functional ProgrammingCrossRefzbMATHGoogle Scholar
  13. 13.
    Clinger, W., Rees, J. (eds.): Revised4 report on the algorithmic language Scheme. LISP Pointers IV(3), 1–55 (1991)CrossRefGoogle Scholar
  14. 14.
    Clinger, W.D.: Proper tail recursion and space efficiency. In: Cooper, K.D. (ed.) Proceedings of the ACM SIGPLAN 1998 Conference on Programming Languages Design and Implementation, Montréal, Canada, pp. 174–185. ACM Press, New York (1998)CrossRefGoogle Scholar
  15. 15.
    Danvy, O.: Formalizing implementation strategies for first-class continuations. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 88–103. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  16. 16.
    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 (2004); Recipient of the 2004 Peter Landin prize. Extended version available as the research report BRICS RS-03-33CrossRefGoogle Scholar
  17. 17.
    Danvy, O.: An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, Aarhus University, Aarhus, Denmark (October 2006)Google Scholar
  18. 18.
    Danvy, O., Filinski, A.: Representing control, a study of the CPS transformation. Mathematical Structures in Computer Science 2(4), 361–391 (1992)MathSciNetCrossRefzbMATHGoogle Scholar
  19. 19.
    Danvy, O., Millikin, K.: Refunctionalization at work. Research Report BRICS RS-08-4, Department of Computer Science, Aarhus University, Aarhus, Denmark (August 2007); To appear in Science of Computer Programming, extended versionGoogle Scholar
  20. 20.
    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
  21. 21.
    Danvy, O., Millikin, K.: Refunctionalization at Work. Science of Computer Programming 74(8), 534–549 (2009); Extended version available as the research report BRICS SCP09 MathSciNetCrossRefzbMATHGoogle Scholar
  22. 22.
    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
  23. 23.
    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 (2001)Google Scholar
  24. 24.
    Danvy, O., Yang, Z.: An operational investigation of the CPS hierarchy. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 224–242. Springer, Heidelberg (1999)CrossRefGoogle Scholar
  25. 25.
    de Bruin, A., de Vink, E.P.: Continuation semantics for Prolog with cut. In: Díaz, J., Orejas, F. (eds.) TAPSOFT 1989. LNCS, vol. 351, pp. 178–192. Springer, Heidelberg (1989)Google Scholar
  26. 26.
    Felleisen, M., Flatt, M.: Programming languages and lambda calculi (1989-2001) (unpublished lecture notes), http://www.ccs.neu.edu/home/matthias/3810-w02/readings.html (last accessed in April 2008)
  27. 27.
    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
  28. 28.
    Gasbichler, M., Knauel, E., Sperber, M.: How to add threads to a sequential language without getting tangled up. In: Flatt, M. (ed.) Proceedings of the Fourth ACM SIGPLAN Workshop on Scheme and Functional Programming, Technical report UUCS-03-023, School of Computing, University of Utah, Boston, Massachusetts, November 2003, pp. 30–47 (2003)Google Scholar
  29. 29.
    Griffin, T.G.: A formulae-as-types notion of control. In: Hudak, P. (ed.) Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming Languages, San Francisco, California, January 1990, pp. 47–58. ACM Press, New York (1990)Google Scholar
  30. 30.
    Harper, R., Duba, B.F., MacQueen, D.: Typing first-class continuations in ML. Journal of Functional Programming 3(4), 465–484 (1993); A preliminary version was presented at the Eighteenth Annual ACM Symposium on Principles of Programming Languages (POPL 1991)CrossRefGoogle Scholar
  31. 31.
    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
  32. 32.
    Hieb, R., Dybvig, R.K., Bruggeman, C.: Representing control in the presence of first-class continuations. In: Lang, B. (ed.) Proceedings of the ACM SIGPLAN 1990 Conference on Programming Languages Design and Implementation, White Plains, June 1990. SIGPLAN Notices, vol. 25(6), pp. 66–77. ACM Press, New York (1990)CrossRefGoogle Scholar
  33. 33.
    Johannsen, J.: An investigation of Abadi and Cardelli’s untyped calculus of objects. Master’s thesis, Department of Computer Science, Aarhus University, Aarhus, Denmark, BRICS research report RS-08-6 (June 2008)Google Scholar
  34. 34.
    Kelsey, R., Clinger, W., Rees, J.: Revised5 report on the algorithmic language Scheme. Higher-Order and Symbolic Computation 11(1), 7–105 (1998)CrossRefGoogle Scholar
  35. 35.
    Krivine, J.-L.: A call-by-name lambda-calculus machine. Higher-Order and Symbolic Computation 20(3), 199–207 (2007)MathSciNetCrossRefzbMATHGoogle Scholar
  36. 36.
    Landin, P.J.: The mechanical evaluation of expressions. The Computer Journal 6(4), 308–320 (1964)CrossRefzbMATHGoogle Scholar
  37. 37.
    Marlow, S., Peyton Jones, S.L.: Making a fast curry: push/enter vs. eval/apply for higher-order languages. In: Fisher, K. (ed.) Proceedings of the 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP 2004), September 2004. SIGPLAN Notices, vol. 39(9), pp. 4–15. ACM Press, New York (2004)Google Scholar
  38. 38.
    Matthews, J., Findler, R.B.: An operational semantics for Scheme. Journal of Functional Programming 18(1), 47–86 (2008)CrossRefzbMATHGoogle Scholar
  39. 39.
    Midtgaard, J.: Transformation, Analysis, and Interpretation of Higher-Order Procedural Programs. PhD thesis, BRICS PhD School, Aarhus University, Aarhus, Denmark (June 2007)Google Scholar
  40. 40.
    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
  41. 41.
    Milner, R., Tofte, M., Harper, R., MacQueen, D.: The Definition of Standard ML (Revised). MIT Press, Cambridge (1997)Google Scholar
  42. 42.
    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, BRICS research report RS-08-3 (May 2007)Google Scholar
  43. 43.
    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
  44. 44.
    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, January 2007. SIGPLAN Notices, vol. 42(1), pp. 143–154. ACM Press, New York (2007)Google Scholar
  45. 45.
    Plotkin, G.D.: Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science 1, 125–159 (1975)MathSciNetCrossRefzbMATHGoogle Scholar
  46. 46.
    Ramsdell, J.D.: An operational semantics for Scheme. LISP Pointers V(2), 6–10 (1992)CrossRefGoogle Scholar
  47. 47.
    Rees, J., Clinger, W. (eds.): Revised3 report on the algorithmic language Scheme. SIGPLAN Notices 21(12), 37–79 (1986)CrossRefGoogle Scholar
  48. 48.
    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 11(4), 363–397 (1998), with a foreword [50]Google Scholar
  49. 49.
    Reynolds, J.C.: Definitional interpreters for higher-order programming languages. Higher-Order and Symbolic Computation 11(4), 363–397 (1998); Reprinted from the proceedings of the 25th ACM National Conference (1972), with a foreword [50]CrossRefzbMATHGoogle Scholar
  50. 50.
    Reynolds, J.C.: Definitional interpreters revisited. Higher-Order and Symbolic Computation 11(4), 355–361 (1998)CrossRefzbMATHGoogle Scholar
  51. 51.
    Sperber, M., Kent Dybvig, R., Flatt, M., van Straaten, A. (eds.): Revised6 report on the algorithmic language Scheme (September 2007), http://www.r6rs.org/
  52. 52.
    Steele Jr., G.L.: Rabbit: A compiler for Scheme. Master’s thesis, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts, Technical report AI-TR-474 (May 1978)Google Scholar
  53. 53.
    Steele Jr., G.L., Sussman, G.J.: The revised report on Scheme, a dialect of Lisp. AI Memo 452, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts (January 1978)Google Scholar
  54. 54.
    Sussman, G.J., Steele Jr., G.L.: Scheme: An interpreter for extended lambda calculus. AI Memo 349, Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, Massachusetts (December 1975); Reprinted in Higher-Order and Symbolic Computation 11(4), 405–439 (1998), with a foreword [55]Google Scholar
  55. 55.
    Sussman, G.J., Steele Jr., G.L.: The first report on Scheme revisited. Higher-Order and Symbolic Computation 11(4), 399–404 (1998)CrossRefzbMATHGoogle Scholar
  56. 56.
    Wadler, P.: The essence of functional programming (invited talk). In: Appel, A.W. (ed.) Proceedings of the Nineteenth Annual ACM Symposium on Principles of Programming Languages, Albuquerque, New Mexico, January 1992, pp. 1–14. ACM Press, New York (1992)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2009

Authors and Affiliations

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

Personalised recommendations