More Web Proxy on the site http://driver.im/

Article

Free access

A call-by-need lambda calculus

Authors:

Zena M. Ariola,

Martin Odersky,

Matthias Felleisen,

Philip WadlerAuthors Info & Claims

POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

Pages 233 - 246

https://doi.org/10.1145/199448.199507

Published: 25 January 1995 Publication History

Abstract

The mismatch between the operational semantics of the lambda calculus and the actual behavior of implementations is a major obstacle for compiler writers. They cannot explain the behavior of their evaluator in terms of source level syntax, and they cannot easily compare distinct implementations of different lazy strategies. In this paper we derive an equational characterization of call-by-need and prove it correct with respect to the original lambda calculus. The theory is a strictly smaller theory than the lambda calculus. Immediate applications of the theory concern the correctness proofs of a number of implementation strategies, e.g., the call-by-need continuation passing transformation and the realization of sharing via assignments.

References

[1]

M. Abadi, L. Cardelli, P.-L. Curien, and :}.-J. L@vy. Explicit substitutions. Journal of Functional Programming, 4(1), 1991.

[2]

S. Abramsky. The lazy lambda calculus. In D. Turner, editor, Declarative Programming. Addison-Wesley, 1990.

[3]

Z. M. Ariola and Arvind. Properties of a firstorder functional language with sharing. Theoretical Computer Science, September 1995.

Digital Library

[4]

Z. M. Ariola and M. Felleisen. The call-by-need lambda calculus. Technical Report CIS-TR-94- 23, Department of computer science, University of Oregon, October 1994.

[5]

Z. M. Ariola and J. W. KIop. Cyclic lambda graph rewriting. In Proc. of #he Eighth IEEE Symposium on Logic in Computer Science, Paris, 1994.

[6]

Z. M. Ariola and J. W. Klop. Equational term graph rewriting. Acta Informahca, 1994.

[7]

Arvind, V. Kathail, and K. Pingali. Sharing of computation in functional language implementations. In Proc. International Workshop on High- Level Computer Architecture, 1984.

[8]

H. P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1984.

[9]

E. Crank. Parameter-passing and the lambda calculus. Master's thesis, Rice University, 1990.

[10]

E. Crank and M. Felleisen. Parameter-passing and the lambda calculus. In Proc. A CM Conference on Principles of Programming Languages, 1990.

Digital Library

[11]

M. Felleisen and D. P. Friedman. Control operators, the SECD-machine, and the lambda-calculus. in 3rd Working Conference on the Formal Description of Programming Concepts, Ebberup, Denmark, August 1986.

[12]

M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 102, 1992.

Digital Library

[13]

J. Field. On laziness and optimality in lambda interpreters: Tools for specification and analysis. In Proc. ACM Conference on Pmnciples of Programming Languages, San Francisco, 1990.

Digital Library

[14]

D. P. Friedman and D. S. Wise. Cons should not evaluate its arguments, in Proc. Internatzonal Conference on Automata, Languages and Programming, 1976.

[15]

G. Gonthier, M. Abadi, and J.-J L#vy. The geometry of optimal lambda reduction. In Proc. A CM Conference on Principles of Programming Languages, 1992.

Digital Library

[16]

V. K. Kathail. Optimal Interpreters for Lambdacalculus Based Funtional Languages. PhD thesis, Dept. of Electrical Engineering and Computer Science, MIT, 1990.

[17]

J. Lamping. An algorithm for optimal Iambda calculus reduction. In Proc. A CM Conference on Principles of Programming Languages, San Francisco, January 1990.

Digital Library

[18]

J. Launchbury. A natural semantics for lazy evaluation. In Proc. A CM Conference on Principles of Programming Languages, 1993.

Digital Library

[19]

J. Maraist, M. Odersky, and P. Wadler. The callby-need lambda calculus (unabridged). Technical Report 28/94, Universit#it Karlsruhe, Fakult#t fiir informatik, October 1994.

[20]

L. Maranget. Optimal derivations in weak lambdacalculi and in orthogonal term rewriting systems. In Proc. A CM Conference on Principles of Programming Languages, Orlando, Florida, january 1991.

Digital Library

[21]

I. A. Mason and C. Talcott. Reasoning about programs with effects. In Proc. of Programming Language Implementation and Logic Programming, Springer-Verlag LNCS 456, Berlin, 1990.

Digital Library

[22]

I. A. Mason and C. L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1(2), 1991.

[23]

G. Morrisett, M. Felleisen, and R. Harper. Modeling memory management. Technical report, Departement of computer science, Carnegie Mellon University, forthcoming 1994.

[24]

C. Okasaki, P. Lee, and T. Tarditi. Call-by-need and continuation-passing style. In Lisp and Symbolic Computaiion, 1994.

Digital Library

[25]

S. L. Peyton Jones. A fully-lazy lambda lifter in haskell. Software Practice and Experience, 21, 1991.

Digital Library

[26]

G. D. Plotkin. Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science, I, 1975.

[27]

Purushothaman and J. Seaman. An adequate operational semantics of sharing in lazy evaluation. In Proc. 4ih European Symposium on Programming, Springer Verlag LNCS 582, 1992.

Digital Library

[28]

K. H. Rose. Explicit cyclic substitutions. In 3rd International Workshop on Conditional Term Rewriting Systems, July 1992.

Digital Library

[29]

J. M. Seaman. An Operaiional Semantics of Lazy Evaluation for Analysis. PhD thesis, The Pennsylvania State University, 1993.

Digital Library

[30]

C. Wadsworth. Semaniics And Pragmatics Of The Lambda-Calculus. PhD thesis, University of Oxford, September 1971.

[31]

N. Yoshida. Optimal reduction in weak-A-calculus with shared environments. In Proc. A CM Conference on Functional Programming Languages and Computer Architecture, Copenhagen, 1993.

Digital Library

Cited By

Downen P(2024)Call-by-Unboxed-ValueProceedings of the ACM on Programming Languages10.1145/36746548:ICFP(845-879)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674654
Torrens POrchard DVasconcellos C(2024)On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRsProceedings of the ACM on Programming Languages10.1145/36746308:ICFP(147-176)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674630
Xia LIsrael LKramarz MColtharp NClaessen KWeirich SLi Y(2024)Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy ProgramsProceedings of the ACM on Programming Languages10.1145/36746268:ICFP(30-63)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674626
Show More Cited By

Index Terms

A call-by-need lambda calculus

Recommendations

The call-by-need lambda calculus

We present a calculus that captures the operational semantics of call-by-need. The call-by-need lambda calculus is confluent, has a notion of standard reduction, and entails the same observational equivalence relation as the call-by-name calculus. The ...
The call-by-need lambda calculus, revisited
ESOP'12: Proceedings of the 21st European conference on Programming Languages and Systems

The existing call-by-need λ describe lazy evaluation via equational logics. A programmer can use these logics to safely ascertain whether one term is behaviorally equivalent to another or to determine the value of a lazy program. However, neither of the ...
The call-by-need lambda calculus

Plotkin (1975) showed that the lambda calculus is a good model of the evaluation process for call-by-name functional programs. Reducing programs to constants or lambda abstractions according to the leftmost-outermost strategy exactly mirrors execution ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

January 1995

415 pages

ISBN:0897916921

DOI:10.1145/199448

Chairmen:
Ron K. Cytron
Washington Univ., St. Louis, MO
,
Peter Lee
Carnegie Mellon Univ., Pittsburgh, PA

Copyright © 1995 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 ACM 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]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 25 January 1995

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

POPL95

Sponsor:

POPL95: 22nd ACM Symposium on Principles of Programming Languages

January 23 - 25, 1995

California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 824 of 4,130 submissions, 20%

Upcoming Conference

POPL '25

Sponsor:
sigplan

The 52nd Annual ACM SIGPLAN Symposium on Principles of Programming Languages

January 19 - 25, 2025

Denver , CO , USA

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

159
Total Citations
View Citations
1,426
Total Downloads

Downloads (Last 12 months)174
Downloads (Last 6 weeks)29

Reflects downloads up to 10 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Downen P(2024)Call-by-Unboxed-ValueProceedings of the ACM on Programming Languages10.1145/36746548:ICFP(845-879)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674654
Torrens POrchard DVasconcellos C(2024)On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRsProceedings of the ACM on Programming Languages10.1145/36746308:ICFP(147-176)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674630
Xia LIsrael LKramarz MColtharp NClaessen KWeirich SLi Y(2024)Story of Your Lazy Function’s Life: A Bidirectional Demand Semantics for Mechanized Cost Analysis of Lazy ProgramsProceedings of the ACM on Programming Languages10.1145/36746268:ICFP(30-63)Online publication date: 15-Aug-2024
https://dl.acm.org/doi/10.1145/3674626
Arrial VGuerrieri GKesner DSobocinski PLago UEsparza J(2024)Genericity Through StratificationProceedings of the 39th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3661814.3662113(1-15)Online publication date: 8-Jul-2024
https://dl.acm.org/doi/10.1145/3661814.3662113
Sullivan ZDownen PAriola Z(2023)Closure Conversion in Little PiecesProceedings of the 25th International Symposium on Principles and Practice of Declarative Programming10.1145/3610612.3610622(1-13)Online publication date: 22-Oct-2023
https://dl.acm.org/doi/10.1145/3610612.3610622
Augustsson LBreitner JClaessen KJhala RPeyton Jones SShivers OSteele Jr. GSweeney T(2023)The Verse Calculus: A Core Calculus for Deterministic Functional Logic ProgrammingProceedings of the ACM on Programming Languages10.1145/36078457:ICFP(417-447)Online publication date: 31-Aug-2023
https://dl.acm.org/doi/10.1145/3607845
Lévy J(2023)Tracking Redexes in the Lambda CalculusThe French School of Programming10.1007/978-3-031-34518-0_10(241-264)Online publication date: 11-Oct-2023
https://doi.org/10.1007/978-3-031-34518-0_10
Sabel DSchmidt-Schauß MMaio L(2022)Contextual Equivalence in a Probabilistic Call-by-Need Lambda-CalculusProceedings of the 24th International Symposium on Principles and Practice of Declarative Programming10.1145/3551357.3551374(1-15)Online publication date: 20-Sep-2022
https://dl.acm.org/doi/10.1145/3551357.3551374
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
Accattoli B(2022)Exponentials as Substitutions and the Cost of Cut Elimination in Linear LogicProceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science10.1145/3531130.3532445(1-15)Online publication date: 2-Aug-2022
https://dl.acm.org/doi/10.1145/3531130.3532445
Show More Cited By

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 Publication

Media

Figures

Other

Tables

View Table of Contents