Compilation of extended recursion in call-by-value functional languages

ABSTRACT

This paper formalizes and proves correct a compilation scheme for mutually-recursive definitions in call-by-value functional languages. This scheme supports a wider range of recursive definitions than standard call-by-value recursive definitions. We formalize our technique as a translation scheme to a lambda-calculus featuring in-place update of memory blocks, and prove the translation to be faithful.

REFERENCES

• 1: M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Lévy. Explicit substitutions. Journal of Functional ProgrammingJ. Func. Progr., 1(4):375--416, 1991.
• 2: Z. M. Ariola and S. Blom. Skew confluence and the lambda calculus with letrec. Annals of pure and applied logic, 117(1--3):95--178, 2002.
• 3: Zine-El-Abidine Benaissa , Pierre Lescanne , Kristoffer Høgsbro Rose, Modeling Sharing and Recursion for Weak Reduction Strategies Using Explicit Substitution, Proceedings of the 8th International Symposium on Programming Languages: Implementations, Logics, and Programs, p.393-407, September 24-27, 1996
• 4: Gérard Boudol, The Recursive Record Semantics of Objects Revisited, Proceedings of the 10th European Symposium on Programming Languages and Systems, p.269-283, April 02-06, 2001
• 5: G. Boudol and P. Zimmer. Recursion in the call-by-value lambda-calculus. Fixed Points in Computer ScienceFixed Points in Comp. Sc. 2002.
• 6: G. Cousineau , P.-L. Curien, The categorical abstract machine, Science of Computer Programming, v.8 n.2, p.173-202, April 1, 1987 [doi>10.1016/0167-6423(87)90020-7]
• 7: The Haskell language. http://www.haskell.org.
• 8: Tom Hirschowitz , Xavier Leroy, Mixin Modules in a Call-by-Value Setting, Proceedings of the 11th European Symposium on Programming Languages and Systems, p.6-20, April 08-12, 2002
• 9: T. Hirschowitz, X. Leroy, and J. B. Wells. On the implementation of recursion in call-by-value functional languages. Research report RR-4728, INRIA, February 2003.
• 10: T. Hirschowitz, X. Leroy, and J. B. Wells. A reduction semantics for call-by-value mixin modules. Research report RR-4682, INRIA, January 2003.
• 11: X. Leroy, D. Doligez, J. Garrigue, D. Rémy, and J. Vouillon. The OCaml 3.06 reference manual, 2002. Available at http://caml.inria.fr/.
• 12: X. Leroy, D. Doligez, J. Garrigue, and J. Vouillon. The Objective Caml system. Software and documentation available on the Web Logiciel et documentation disponibles sur le Web, http://caml.inria.fr/, 1996--2003.
• 13: Robin Milner , Mads Tofte , David Macqueen, The Definition of Standard ML, MIT Press, Cambridge, MA, 1997
• 14: Kristoffer Høgsbro Rose, Explicit Cyclic Substitutions, Proceedings of the Third International Workshop on Conditional Term Rewriting Systems, p.36-50, July 08-10, 1992
• 15: O. Waddell, D. Sarkar, and R. K. Dybvig. Robust and effective transformation of letrec. In Electronic proceedings of the 2002 Scheme Workshop, 2002. http://scheme2002.ccs.neu.edu/.

INDEX TERMS

Primary Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Program and recursion schemes

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.1 Formal Definitions and Theory
          Subjects: Syntax; Semantics
      D.3.3 Language Constructs and Features
          Subjects: Recursion
      D.3.4 Processors
          Subjects: Compilers

  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.2 Semantics of Programming Languages
          Subjects: Operational semantics

General Terms:
Design, Languages, Reliability, Theory

Keywords:
compilation, functional languages, recursion, semantics