Advertisement

Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion

  • Masayuki MizunoEmail author
  • Eijiro SumiiEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11893)

Abstract

We present new proofs—formalized in the Coq proof assistant—of the correspondence among call-by-need and (various definitions of) call-by-name evaluations of \(\lambda \)-calculus with mutually recursive bindings.

For non-strict languages, the equivalence between high-level specifications (call-by-name) and typical implementations (call-by-need) is of foundational interest. A particular milestone is Launchbury’s natural semantics of call-by-need evaluation and proof of its adequacy with respect to call-by-name denotational semantics, which are recently formalized in Isabelle/HOL by Breitner (2018). Equational theory by Ariola et al. is another well-known formalization of call-by-need. Mutual recursion is especially challenging for their theory: reduction is complicated by the traversal of dependency (the “need” relation), and the correspondence of call-by-name and call-by-need reductions becomes non-trivial, requiring sophisticated structures such as graphs or infinite trees.

In this paper, we give arguably simpler proofs solely based on (finite) terms and operational semantics, which are easier to handle for proof assistants (Coq in our case). Our proofs can be summarized as follows: (1) we prove the equivalence between Launchbury’s call-by-need semantics and heap-based call-by-name natural semantics, where we define a sufficiently (but not too) general correspondence between the two heaps, and (2) we also show the correspondence among three styles of call-by-name semantics: (i) the natural semantics used in (1); (ii) closure-based natural semantics that informally corresponds to Launchbury’s denotational semantics; and (iii) conventional substitution-based semantics.

References

  1. 1.
    Abramsky, S.: The lazy lambda calculus. In: Turner, D.A. (ed.) Research Topics in Functional Programming, pp. 65–116. Addison-Wesley Publishing Co., Boston (1990)Google Scholar
  2. 2.
    Ariola, Z.M., Blom, S.: Cyclic lambda calculi. In: Abadi, M., Ito, T. (eds.) TACS 1997. LNCS, vol. 1281, pp. 77–106. Springer, Heidelberg (1997).  https://doi.org/10.1007/BFb0014548CrossRefGoogle Scholar
  3. 3.
    Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. JFP 7(3), 265–301 (1997)MathSciNetzbMATHGoogle Scholar
  4. 4.
    Barendregt, H.P., Kennaway, R., Klop, J.W., Sleep, M.R.: Needed reduction and spine strategies for the lambda calculus. Inf. Comput. 75(3), 191–231 (1987)MathSciNetCrossRefGoogle Scholar
  5. 5.
    Birkedal, L., Tofte, M., Vejlstrup, M.: From region inference to von Neumann machines via region representation inference. In: POPL, pp. 171–183 (1996)Google Scholar
  6. 6.
    Boudol, G., Curien, P., Lavatelli, C.: A semantics for lambda calculi with resources. Math. Struct. Comput. Sci. 9(4), 437–482 (1999)MathSciNetCrossRefGoogle Scholar
  7. 7.
    Breitner, J.: The adequacy of Launchbury’s natural semantics for lazy evaluation. JFP 28, e1 (2018)MathSciNetzbMATHGoogle Scholar
  8. 8.
    de Bruijn, N.G.: Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae (Proc.) 75(5), 381–392 (1972)MathSciNetCrossRefGoogle Scholar
  9. 9.
    Charguéraud, A.: The locally nameless representation. J. Autom. Reasoning 49(3), 363–408 (2012)MathSciNetCrossRefGoogle Scholar
  10. 10.
    Church, A.: An unsolvable problem of elementary number theory. Am. J. Math. 58(2), 345–363 (1936)MathSciNetCrossRefGoogle Scholar
  11. 11.
    Coquand, T.: Infinite objects in type theory. In: Barendregt, H., Nipkow, T. (eds.) TYPES 1993. LNCS, vol. 806, pp. 62–78. Springer, Heidelberg (1994).  https://doi.org/10.1007/3-540-58085-9_72CrossRefGoogle Scholar
  12. 12.
    Curry, H.B., Feys, R.: Combinatory Logic, Studies in Logic and the Foundations of Mathematics, vol. 1. North-Holland, Amsterdam (1958)zbMATHGoogle Scholar
  13. 13.
    Giménez, E.: Codifying guarded definitions with recursive schemes. In: Dybjer, P., Nordström, B., Smith, J. (eds.) TYPES 1994. LNCS, vol. 996, pp. 39–59. Springer, Heidelberg (1995).  https://doi.org/10.1007/3-540-60579-7_3CrossRefGoogle Scholar
  14. 14.
    Hackett, J., Hutton, G.: Call-by-need is clairvoyant call-by-value. In: ICFP (2019, to appear)Google Scholar
  15. 15.
    Halim, S., Halim, F.: Competitive Programming, 3rd edn. Lulu, Morrisville (2013)Google Scholar
  16. 16.
    Johnsson, T.: Efficient compilation of lazy evaluation. In: ACM SIGPLAN Symposium on Compiler Construction, pp. 58–69 (1984)CrossRefGoogle Scholar
  17. 17.
    Kesner, D., Ríos, A., Viso, A.: Call-by-need, neededness and all that. In: FOSSACS, pp. 241–257 (2018)Google Scholar
  18. 18.
    Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6(4), 308–320 (1964)CrossRefGoogle Scholar
  19. 19.
    Launchbury, J.: A natural semantics for lazy evaluation. In: POPL, pp. 144–154 (1993)Google Scholar
  20. 20.
    Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284–304 (2009)MathSciNetCrossRefGoogle Scholar
  21. 21.
    Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. JFP 8(3), 275–317 (1998)MathSciNetzbMATHGoogle Scholar
  22. 22.
    Mizuno, M., Sumii, E.: Formal verification of the correspondence between call-by-need and call-by-name. In: Gallagher, J.P., Sulzmann, M. (eds.) FLOPS 2018. LNCS, vol. 10818, pp. 1–16. Springer, Cham (2018).  https://doi.org/10.1007/978-3-319-90686-7_1CrossRefzbMATHGoogle Scholar
  23. 23.
    Nakata, K., Hasegawa, M.: Small-step and big-step semantics for call-by-need. JFP 19(6), 699–722 (2009)MathSciNetzbMATHGoogle Scholar
  24. 24.
    Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)CrossRefGoogle Scholar
  25. 25.
    Ong, C.L.: Fully abstract models of the lazy lambda calculus. In: FOCS, pp. 368–376. IEEE Computer Society (1988)Google Scholar
  26. 26.
    Peyton Jones, S.: Implementing lazy functional languages on stock hardware: the spineless tagless G-machine. JFP 2(2), 127–202 (1992)zbMATHGoogle Scholar
  27. 27.
    Pierce, B.C.: Types and Programming Languages, 1st edn. The MIT Press, Cambridge (2002)zbMATHGoogle Scholar
  28. 28.
    Plotkin, G.D.: Call-by-name, call-by-value and the \(\lambda \)-calculus. TCS 1(2), 125–159 (1975)MathSciNetCrossRefGoogle Scholar
  29. 29.
    Sestoft, P.: Deriving a lazy abstract machine. JFP 7(3), 231–264 (1997)MathSciNetzbMATHGoogle Scholar
  30. 30.
    Stelle, G., Stefanovic, D.: Verifiably lazy: verified compilation of call-by-need. In: IFL, pp. 49–58 (2018)Google Scholar
  31. 31.
    Wadsworth, C.P.: Semantics and pragmatics of the lambda calculus. Ph.D. thesis, Oxford University (1971)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Graduate School of Information SciencesTohoku UniversitySendaiJapan

Personalised recommendations