Skip to main content
SpringerLink
Log in
Book cover

Asian Symposium on Programming Languages and Systems

APLAS 2019: Programming Languages and Systems pp 181–201Cite as

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

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNPSE,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.

We thank the anonymous reviewers for valuable comments and suggestions. This work was partially supported by JSPS KAKENHI Grant Numbers JP19J11926, JP15H02681, JP16K12409 and the Asahi Glass Foundation.

This is a preview of subscription content, 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 EPUB and 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

Learn about institutional subscriptions

Notes

  1. 1.

    https://github.com/fetburner/cbn

References

  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. 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/BFb0014548

    Chapter  Google Scholar 

  3. Ariola, Z.M., Felleisen, M.: The call-by-need lambda calculus. JFP 7(3), 265–301 (1997)

    MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  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. Boudol, G., Curien, P., Lavatelli, C.: A semantics for lambda calculi with resources. Math. Struct. Comput. Sci. 9(4), 437–482 (1999)

    Article  MathSciNet  Google Scholar 

  7. Breitner, J.: The adequacy of Launchbury’s natural semantics for lazy evaluation. JFP 28, e1 (2018)

    MathSciNet  MATH  Google Scholar 

  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)

    Article  MathSciNet  Google Scholar 

  9. Charguéraud, A.: The locally nameless representation. J. Autom. Reasoning 49(3), 363–408 (2012)

    Article  MathSciNet  Google Scholar 

  10. Church, A.: An unsolvable problem of elementary number theory. Am. J. Math. 58(2), 345–363 (1936)

    Article  MathSciNet  Google Scholar 

  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_72

    Chapter  Google Scholar 

  12. Curry, H.B., Feys, R.: Combinatory Logic, Studies in Logic and the Foundations of Mathematics, vol. 1. North-Holland, Amsterdam (1958)

    MATH  Google Scholar 

  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_3

    Chapter  Google Scholar 

  14. Hackett, J., Hutton, G.: Call-by-need is clairvoyant call-by-value. In: ICFP (2019, to appear)

    Google Scholar 

  15. Halim, S., Halim, F.: Competitive Programming, 3rd edn. Lulu, Morrisville (2013)

    Google Scholar 

  16. Johnsson, T.: Efficient compilation of lazy evaluation. In: ACM SIGPLAN Symposium on Compiler Construction, pp. 58–69 (1984)

    Article  Google Scholar 

  17. Kesner, D., Ríos, A., Viso, A.: Call-by-need, neededness and all that. In: FOSSACS, pp. 241–257 (2018)

    Google Scholar 

  18. Landin, P.J.: The mechanical evaluation of expressions. Comput. J. 6(4), 308–320 (1964)

    Article  Google Scholar 

  19. Launchbury, J.: A natural semantics for lazy evaluation. In: POPL, pp. 144–154 (1993)

    Google Scholar 

  20. Leroy, X., Grall, H.: Coinductive big-step operational semantics. Inf. Comput. 207(2), 284–304 (2009)

    Article  MathSciNet  Google Scholar 

  21. Maraist, J., Odersky, M., Wadler, P.: The call-by-need lambda calculus. JFP 8(3), 275–317 (1998)

    MathSciNet  MATH  Google Scholar 

  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_1

    Chapter  MATH  Google Scholar 

  23. Nakata, K., Hasegawa, M.: Small-step and big-step semantics for call-by-need. JFP 19(6), 699–722 (2009)

    MathSciNet  MATH  Google Scholar 

  24. Okasaki, C.: Purely Functional Data Structures. Cambridge University Press, Cambridge (1998)

    Book  Google Scholar 

  25. Ong, C.L.: Fully abstract models of the lazy lambda calculus. In: FOCS, pp. 368–376. IEEE Computer Society (1988)

    Google Scholar 

  26. Peyton Jones, S.: Implementing lazy functional languages on stock hardware: the spineless tagless G-machine. JFP 2(2), 127–202 (1992)

    MATH  Google Scholar 

  27. Pierce, B.C.: Types and Programming Languages, 1st edn. The MIT Press, Cambridge (2002)

    MATH  Google Scholar 

  28. Plotkin, G.D.: Call-by-name, call-by-value and the \(\lambda \)-calculus. TCS 1(2), 125–159 (1975)

    Article  MathSciNet  Google Scholar 

  29. Sestoft, P.: Deriving a lazy abstract machine. JFP 7(3), 231–264 (1997)

    MathSciNet  MATH  Google Scholar 

  30. Stelle, G., Stefanovic, D.: Verifiably lazy: verified compilation of call-by-need. In: IFL, pp. 49–58 (2018)

    Google Scholar 

  31. Wadsworth, C.P.: Semantics and pragmatics of the lambda calculus. Ph.D. thesis, Oxford University (1971)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Graduate School of Information Sciences, Tohoku University, Sendai, Japan

    Masayuki Mizuno & Eijiro Sumii

Authors
  1. Masayuki Mizuno
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Eijiro Sumii
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding authors

Correspondence to Masayuki Mizuno or Eijiro Sumii .

Editor information

Editors and Affiliations

  1. University of Kaiserslautern, Kaiserslautern, Germany

    Anthony Widjaja Lin

Rights and permissions

Reprints and permissions

Copyright information

© 2019 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Mizuno, M., Sumii, E. (2019). Formal Verifications of Call-by-Need and Call-by-Name Evaluations with Mutual Recursion. In: Lin, A. (eds) Programming Languages and Systems. APLAS 2019. Lecture Notes in Computer Science(), vol 11893. Springer, Cham. https://doi.org/10.1007/978-3-030-34175-6_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-34175-6_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-34174-9

  • Online ISBN: 978-3-030-34175-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation