research-article

Open access

Foundations of strong call by need

Authors:

Thibaut Balabonski,

Pablo Barenbaum,

Eduardo Bonelli,

Delia KesnerAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 1, Issue ICFP

Article No.: 20, Pages 1 - 29

https://doi.org/10.1145/3110264

Published: 29 August 2017 Publication History

Abstract

We present a call-by-need strategy for computing strong normal forms of open terms (reduction is admitted inside the body of abstractions and substitutions, and the terms may contain free variables), which guarantees that arguments are only evaluated when needed and at most once. The strategy is shown to be complete with respect to β-reduction to strong normal form. The proof of completeness relies on two key tools: (1) the definition of a strong call-by-need calculus where reduction may be performed inside any context, and (2) the use of non-idempotent intersection types. More precisely, terms admitting a β-normal form in pure lambda calculus are typable, typability implies (weak) normalisation in the strong call-by-need calculus, and weak normalisation in the strong call-by-need calculus implies normalisation in the strong call-by-need strategy. Our (strong) call-by-need strategy is also shown to be conservative over the standard (weak) call-by-need.

References

[1]

Beniamino Accattoli. 2012. An Abstract Factorization Theorem for Explicit Substitutions. In 23rd International Conference on Rewriting Techniques and Applications (RTA’12), May 28 - June 2, 2012, Nagoya, Japan (LIPIcs), Ashish Tiwari (Ed.), Vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 6–21.

[2]

Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. 2014. Distilling abstract machines. In Proceedings of the 19th ACM SIGPLAN international conference on Functional programming (ICFP’14), Gothenburg, Sweden, September 1-3, 2014, Johan Jeuring and Manuel M. T. Chakravarty (Eds.). ACM, 363–376.

Digital Library

[3]

Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. 2015. A Strong Distillery. In Programming Languages and Systems - 13th Asian Symposium (APLAS’15), Pohang, South Korea, November 30 - December 2, 2015. (LNCS), Xinyu Feng and Sungwoo Park (Eds.), Vol. 9458. Springer Verlag, 231–250.

[4]

Beniamino Accattoli and Giulio Guerrieri. 2016. Open Call-by-Value. In Programming Languages and Systems - 14th Asian Symposium (APLAS’16), Hanoi, Vietnam, November 21-23, 2016. (LNCS), Atsushi Igarashi (Ed.), Vol. 10017. Springer, 206–226.

[5]

Beniamino Accattoli and Delia Kesner. 2010. The Structural lambda-Calculus. In Computer Science Logic, 24th International Workshop (CSL’10), 19th Annual Conference of the EACSL, Brno, Czech Republic, August 23-27, 2010. (LNCS), Anuj Dawar and Helmut Veith (Eds.), Vol. 6247. Springer Verlag, 381–395.

[6]

Beniamino Accattoli and Ugo Dal Lago. 2016. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Logical Methods in Computer Science 12, 1 (2016), 1–46.

[7]

Zena M. Ariola and Matthias Felleisen. 1997. The Call-By-Need Lambda Calculus. Journal of Functional Programming 7, 3 (1997), 265–301.

Digital Library

[8]

Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. 1995. The Call-by-Need Lambda Calculus. In Conference Record of POPL’95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, San Francisco, California, USA, January 23-25, 1995, Ron K. Cytron and Peter Lee (Eds.). ACM Press, 233–246.

Digital Library

[9]

Andrea Asperti and Stefano Guerrini. 1998. The Optimal Implementation of Functional Programming Languages. Cambridge Tracts in Theoretical Computer Science, Vol. 45. Cambridge University Press.

Digital Library

[10]

Thibaut Balabonski. 2013. Weak optimality, and the meaning of sharing. In ACM SIGPLAN International Conference on Functional Programming (ICFP’13), Boston, MA, USA - September 25 - 27, 2013, Greg Morrisett and Tarmo Uustalu (Eds.). ACM, 263–274.

Digital Library

[11]

Hendrik Pieter Barendregt, Jan A. Bergstra, Jan Willem Klop, and Henri Volken. 1976. Some Notes on Lambda Reduction. Technical Report 22. University of Utrecht, Department of mathematics. 13–53 pages.

[12]

B. Barras. 2017. Personal Communication. (February 2017).

[13]

Alexis Bernadet and Stéphane Lengrand. 2011. Complexity of strongly normalising λ-terms via non-idempotent intersection types. In Foundations of Software Science and Computation Structures (FOSSACS) (LNCS), Martin Hofmann (Ed.), Vol. 6604. Springer Verlag, 88–107.

[14]

Alexis Bernadet and Stéphane Lengrand. 2013. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science 9, 4 (2013), 1–46.

[15]

Mathieu Boespflug, Maxime Dénès, and Benjamin Grégoire. 2011. Full Reduction at Full Throttle. In Certified Programs and Proofs - First International Conference (CPP’11), Kenting, Taiwan, December 7-9, 2011. (LNCS), Jean-Pierre Jouannaud and Zhong Shao (Eds.), Vol. 7086. Springer, 362–377.

Digital Library

[16]

Antonio Bucciarelli, Delia Kesner, and Daniel Ventura. 2017. Non-Idempotent Intersection Types for the Lambda-Calculus. Logic Journal of the IGPL (2017). To appear.

[17]

Stephen Chang and Matthias Felleisen. 2012. The Call-by-Need Lambda Calculus, Revisited. In Programming Languages and Systems - 21st European Symposium on Programming (ESOP’12), Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2012, Tallinn, Estonia, March 24 - April 1, 2012. (LNCS), Helmut Seidl (Ed.), Vol. 7211. Springer Verlag, 128–147.

[18]

Mario Coppo and Mariangiola Dezani-Ciancaglini. 1980. An extension of the basic functionality theory for the λ-calculus. Notre Dame Journal of Formal Logic 21, 4 (1980), 685–693.

[19]

Mario Coppo, Mariangiola Dezani-Ciancaglini, and Betti Venneri. 1981. Functional Characters of Solvable Terms. Mathematical Logic Quarterly 27, 2-6 (1981), 45–58.

[20]

Pierre Crégut. 1990. An Abstract Machine for Lambda-Terms Normalization. In LISP and Functional Programming. ACM, 333–340.

Digital Library

[21]

Pierre Crégut. 2007. Strongly reducing variants of the Krivine abstract machine. Higher-Order and Symbolic Computation 20, 3 (2007), 209–230.

Digital Library

[22]

Olivier Danvy and Ian Zerny. 2013. A synthetic operational account of call-by-need evaluation, See [ Peña and Schrijvers 2013 ], 97–108.

[23]

Erika De Benedetti and Simona Ronchi Della Rocca. 2013. Bounding normalization time through intersection types. In Proceedings of Sixth Workshop on Intersection Types and Related Systems (ITRS) (Electronic Proceedings in Theoretical Computer Science), Luca Paolini (Ed.), Vol. 121. Cornell University Library, 48–57.

[24]

Daniel de Carvalho. 2007. Sémantiques de la logique linéaire et temps de calcul. Ph.D. Dissertation. Universit é Aix-Marseille II.

[25]

Daniel de Carvalho. 2009. Execution Time of lambda-Terms via Denotational Semantics and Intersection Types. CoRR abs/0905.4251 (2009), 1–36.

[26]

Thomas Ehrhard and Laurent Regnier. 2006. Böhm Trees, Krivine’s Machine and the Taylor Expansion of Lambda-Terms. In Logical Approaches to Computational Barriers, Second Conference on Computability in Europe (CiE’06), Swansea, UK, June 30-July 5, 2006. (LNCS), Arnold Beckmann, Ulrich Berger, Benedikt Löwe, and John V. Tucker (Eds.), Vol. 3988. Springer Verlag, 186–197.

[27]

Philippa Gardner. 1994. Discovering Needed Reductions Using Type Theory. In International Conference on Theoretical Aspects of Computer Software (TACS’94) (LNCS), Masami Hagiya and John C. Mitchell (Eds.), Vol. 789. Springer Verlag, 555–574.

[28]

Benjamin Grégoire and Xavier Leroy. 2002. A compiled implementation of strong reduction. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming (ICFP ’02), Pittsburgh, Pennsylvania, USA, October 4-6, 2002., Mitchell Wand and Simon L. Peyton Jones (Eds.). ACM, 235–246.

Digital Library

[29]

Peter Henderson and James H. Morris. 1976. A Lazy Evaluator. In Conference Record of the Third ACM Symposium on Principles of Programming Languages (POPL’76), Atlanta, Georgia, USA, January 1976, Susan L. Graham, Robert M. Graham, Michael A. Harrison, William I. Grosky, and Jeffrey D. Ullman (Eds.). ACM Press, 95–103.

Digital Library

[30]

Simon L. Peyton Jones. 1987. The Implementation of Functional Programming Languages. Prentice-Hall.

[31]

Delia Kesner. 2009. A Theory of Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science 5, 3 (2009), 1–29. http://arxiv.org/abs/0905.2539

[32]

Delia Kesner. 2016. Reasoning About Call-by-need by Means of Types. In Foundations of Software Science and Computation Structures - 19th International Conference (FOSSACS’16), Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016. (LNCS), Bart Jacobs and Christof Löding (Eds.), Vol. 9634. Springer Verlag, 424–441.

[33]

Delia Kesner and Daniel Ventura. 2014. Quantitative Types for the Linear Substitution Calculus. In Theoretical Computer Science - 8th IFIP TC 1/WG 2.2 International Conference (TCS’14), Rome, Italy, September 1-3, 2014. (LNCS), Josep Díaz, Ivan Lanese, and Davide Sangiorgi (Eds.), Vol. 8705. Springer Verlag, 296–310.

[34]

Delia Kesner and Daniel Ventura. 2015. A resource aware computational interpretation for Herberlin’s syntax. In Theoretical Aspects of Computing (ICTAC) (LNCS), Martin Leucker, Camilo Rueda, and Frank D. Valencia (Eds.), Vol. 9399. Springer Verlag, 1–16.

[35]

Assaf J. Kfoury. 2000. A linearization of the Lambda-calculus and consequences. J. Log. Comput. 10, 3 (2000), 411–436.

[36]

Assaf J. Kfoury and Joe Wells. 2004. Principality and type inference for intersection types using expansion variables. Theoretical Computer Science 311, 1-3 (2004), 1–70.

Digital Library

[37]

Jean-Louis Krivine. 1993. Lambda-calculus, types and models. Ellis Horwood.

[38]

John Lamping. 1990. An algorithm for optimal lambda calculus reduction. In Procedings of POPL. ACM, San Francisco, California, 16–30.

Digital Library

[39]

John Launchbury. 1993. A Natural Semantics for Lazy Evaluation. In Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, Charleston, South Carolina, USA, January 1993, Mary S. Van Deusen and Bernard Lang (Eds.). ACM Press, 144–154.

Digital Library

[40]

Jean-Jacques Lévy. 1980. Optimal Reductions in the lambda-calculus. In To Haskell Brooks Curry: Essays in Combinatory Logic, Lambda Calculus and formalism, Roger Hindley and Jonathan P. Seldin (Eds.). Academic Press, 159–191.

[41]

John Maraist, Martin Odersky, and Philip Wadler. 1998. The Call-by-Need Lambda Calculus. Journal of Functional Programming 8, 3 (1998), 275–317.

Digital Library

[42]

Robin Milner. 2007. Local Bigraphs and Confluence: Two Conjectures: (Extended Abstract). Electronic Notes in Theoretical Computer Science 175, 3 (2007), 65–73.

Digital Library

[43]

Ricardo Peña and Tom Schrijvers (Eds.). 2013. 15th International Symposium on Principles and Practice of Declarative Programming (PPDP ’13), Madrid, Spain, September 16-18, 2013. ACM.

Digital Library

[44]

William Tait. 1967. Intensional interpretation of functionals of finite type I. Journal of Symbolic Logic 32, 2 (1967), 198–212.

[45]

The Coq Development Team. 2017. The Coq Proof Assistant (v8.6). (2017). https://github.com/coq/coq .

[46]

Steffen van Bakel. 1992. Complete Restrictions of the Intersection Type Discipline. Theoretical Computer Science 102, 1 (1992), 135–163.

Digital Library

[47]

Christopher P. Wadsworth. 1971. Semantics and Pragmatics of the Lambda Calculus. Ph.D. Dissertation. Oxford University.

Cited By

Accattoli BStorm THirschfeld R(2023)Sharing a Perspective on the 𝜆-CalculusProceedings of the 2023 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3622758.3622884(179-190)Online publication date: 18-Oct-2023
https://dl.acm.org/doi/10.1145/3622758.3622884
Biernacka MCharatonik WDrab T(2022)A simple and efficient implementation of strong call by need by an abstract machineProceedings of the ACM on Programming Languages10.1145/35498226:ICFP(109-136)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3549822
Alves SVentura D(2022)Quantitative Weak LinearisationTheoretical Aspects of Computing – ICTAC 202210.1007/978-3-031-17715-6_7(78-95)Online publication date: 3-Oct-2022
https://doi.org/10.1007/978-3-031-17715-6_7
Show More Cited By

Index Terms

Foundations of strong call by need
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Foundations of Paraconsistent Resolution

An extended first-order predicate sequent calculus PLK with two kinds of negation is introduced as a basis of a new resolution calculus PRC (paraconsistent resolution calculus) for handling the property of paraconsistency. Herbrand theorem, completeness ...
Foundations of Paraconsistent Resolution

An extended first-order predicate sequent calculus PLK with two kinds of negation is introduced as a basis of a new resolution calculus PRC (paraconsistent resolution calculus) for handling the property of paraconsistency. Herbrand theorem, completeness ...
Classical call-by-need and duality
TLCA'11: Proceedings of the 10th international conference on Typed lambda calculi and applications

We study call-by-need from the point of view of the duality between call-by-name and call-by-value. We develop sequent-calculus style versions of call-by-need both in the minimal and classical case. As a result, we obtain a natural extension of call-by-...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 1, Issue ICFP

September 2017

1173 pages

EISSN:2475-1421

DOI:10.1145/3136534

Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than the author(s) must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 August 2017

Published in PACMPL Volume 1, Issue ICFP

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

10
Total Citations
View Citations
555
Total Downloads

Downloads (Last 12 months)61
Downloads (Last 6 weeks)12

Reflects downloads up to 16 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Accattoli BStorm THirschfeld R(2023)Sharing a Perspective on the 𝜆-CalculusProceedings of the 2023 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software10.1145/3622758.3622884(179-190)Online publication date: 18-Oct-2023
https://dl.acm.org/doi/10.1145/3622758.3622884
Biernacka MCharatonik WDrab T(2022)A simple and efficient implementation of strong call by need by an abstract machineProceedings of the ACM on Programming Languages10.1145/35498226:ICFP(109-136)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3549822
Alves SVentura D(2022)Quantitative Weak LinearisationTheoretical Aspects of Computing – ICTAC 202210.1007/978-3-031-17715-6_7(78-95)Online publication date: 3-Oct-2022
https://doi.org/10.1007/978-3-031-17715-6_7
Biernacka MCharatonik WDrab T(2021)A Derived Reasonable Abstract Machine for Strong Call by ValueProceedings of the 23rd International Symposium on Principles and Practice of Declarative Programming10.1145/3479394.3479401(1-14)Online publication date: 6-Sep-2021
https://dl.acm.org/doi/10.1145/3479394.3479401
Accattoli BCondoluci ACoen CGorla D(2021)Strong call-by-value is reasonable, implosivelyProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470630(1-14)Online publication date: 29-Jun-2021
https://dl.acm.org/doi/10.1109/LICS52264.2021.9470630
Kesner DPeyrot LVentura D(2021)The Spirit of Node ReplicationFoundations of Software Science and Computation Structures10.1007/978-3-030-71995-1_18(344-364)Online publication date: 23-Mar-2021
https://doi.org/10.1007/978-3-030-71995-1_18
Biernacka MBiernacki DCharatonik WDrab T(2020)An Abstract Machine for Strong Call by ValueProgramming Languages and Systems10.1007/978-3-030-64437-6_8(147-166)Online publication date: 24-Nov-2020
https://doi.org/10.1007/978-3-030-64437-6_8
Accattoli BGuerrieri GLeberle M(2019)Types by NeedProgramming Languages and Systems10.1007/978-3-030-17184-1_15(410-439)Online publication date: 6-Apr-2019
https://doi.org/10.1007/978-3-030-17184-1_15
Barenbaum PBonelli EMohamed KSabel DThiemann P(2018)Pattern Matching and Fixed PointsProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236972(1-12)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236972
Accattoli BBarras BVanhoof WPientka B(2017)Environments and the complexity of abstract machinesProceedings of the 19th International Symposium on Principles and Practice of Declarative Programming10.1145/3131851.3131855(4-16)Online publication date: 9-Oct-2017
https://dl.acm.org/doi/10.1145/3131851.3131855

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents