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

Article

Free access

A non-deterministic call-by-need lambda calculus

Authors:

Manfred Schmidt-SchaußAuthors Info & Claims

ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming

Pages 324 - 335

https://doi.org/10.1145/289423.289462

Published: 29 September 1998 Publication History

Abstract

In this paper we present a non-deterministic call-by-need (untyped) lambda calculus λ_nd with a constant choice and a let-syntax that models sharing. Our main result is that λ_nd has the nice operational properties of the standard lambda calculus: confluence on sets of expressions, and normal order reduction is sufficient to reach head normal form. Using a strong contextual equivalence we show correctness of several program transformations. In particular of lambda-lifting using deterministic maximal free expressions. These results show that λ_nd is a new and also natural combination of non-determinism and lambda-calculus, which has a lot of opportunities for parallel evaluation.An intended application of λ_nd is as a foundation for compiling lazy functional programming languages with I/O based on direct calls. The set of correct program transformations can be rigorously distinguished from non-correct ones. All program transformations are permitted with the slight exception that for transformations like common subexpression elimination and lambda-lifting with maximal free expressions the involved subexpressions have to be deterministic ones.

References

[1]

Samson Abramsky. The lazy lambda calculus. In D. Turner, editor, Research Topics in Functional Programming, pages 65-116. Addison- Wesley, 1990.

Digital Library

[2]

Egidio Astesiano and Gerardo Costa. Sharing in nondeterminism. In Proc. 6th ICALP 79, pages 1-15, 1979.

Digital Library

[3]

M. Abadi, L. Cardelli, P.-L. Curien, and J.-J Ldvy. Explicit substitutions. J. functional programming, 4(1 ):375-416, 1991.

[4]

Peter Achten. Interactive functional programs: models, methods and implementation. PhD thesis, Computer Science Department, University Nijmegen, 1996.

[5]

Z.M. Ariola and M Felleisen. The call-by-need lambda calculus. J. functional programming, 7(3):265-301, 1997.

Digital Library

[6]

Z.M. Ariola, M. Felleisen, J. Maraist, M. Odersky, and P. Wadler. A call-by-need lambda calculus. In Principles o} programming languages, pages 233-246, San Francisco, California, 1995. ACM Press.

[7]

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

[8]

G. Boudol. Lambda-calculi for (strict) parallel functions. Information and Computation, 108:51-127, 1994.

Digital Library

[9]

U. De'Liguoro and A. Piperno. Nondeterministic extensions of untyped )vcalculus. Information and Coinputation, 122:149-177, 1995.

Digital Library

[10]

J. Hughes and A. Moran. A semantics for locally bottom-avoiding choice. In Proc. Glasgow functional programming workshop 1992, Workshops in Computing. Springer-Verlag, 1992.

Digital Library

[11]

N.W.O. Hutchison, U. Neuhaus, M. Schmidt- Schaufi, and C.V Hall. Natural Expert: A commercial functional programming environment. J. of Functional Programming, 7(2):163-182, 1997.

Digital Library

[12]

J. Hughes and J. O'Donnell. Expressing and reasoning about non-deterministic functional programs. In Glasgow workshop on functional programming 1989, Workshops in Computing, pages 308-328. Springer-Verlag, 1989.

Digital Library

[13]

J. Hughes and J. O'Donnell. Nondeterministic functional programming with sets. In IV Higher Order Workshop, Workshops in Computing, pages 11-31. $pringer-Verlag, 1990.

[14]

D. Howe. Equality in lazy computation systems. In dth IEEE Syrup. on Logic in Computer Sole'ace, pages 198-203, 1989.

Digital Library

[15]

G.P. Huet. Confluent reductions: Abstract properties and applications to term rewriting systems. J. of the A CM, 27:797-821, 1980.

Digital Library

[16]

J Launchbury. A natural semantics for lazy evaluation. In Proc. 20th Principles of Programming Languages, 1993.

Digital Library

[17]

L. Mandel. Constrained Lambda Calculus. Verlag Shaker, Aachen, Germany, 1995.

[18]

John Maraist, Martin Odersky, and Philip Wadler. The call-by-need lambda calculus. J. of Functional programming, 1998. to appear.

Digital Library

[19]

M.H.A. Newman. On theories with a combinatorial definition of "equivalence". Annals of Mathematics, 2:223-243, 1942.

[20]

E. Nrcker, J. E. Smetsers, M. van Eekelen, and M. J. Plasmeijer. Concurrent Clean. In Proc of Parallel Architecture and Languages Europe (PARLE'91), number 505 in LNCS, pages 202- 219. Springer Verlag, 1991.

[21]

C.-H. L. Ong. Non-determinism in a functional setting. In Proc. 8th IEEE Symposium on Logic in Computer Science (LICS '93), pages 275- 286. iEEE Computer Society Press, 1993.

[22]

Ross Paterson. A tiny functional language with logical features. In M.Coppo et.al., editor, Declarative Programming, Sasbachwalden, pages 66-79, 1991.

[23]

J. Peterson ted.}, K. Hammond ted.}, L. Augustsson, B. Boutel, W. Burton, J. Fasel, A. D. Gordon, J. Hughes, P. Hudak, Th. Johnsson, M. Jones, E. Meijer, S. Peyton Jones, A. Reid, and P. Wadier. Report on the programming language Haskell: A non-strict, purely functional language, Version 1.4, 1997.

[24]

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

Digital Library

[25]

Simon L. Peyton Jones and David R. Lester. b~plementing Functional Languages: a Tutorial. Prentice-Hall International, London, 199I.

Digital Library

[26]

D. Sangiorgi. The lazy lambda calculus in a concurrency scenario. Information and Computation, 111:120-153, 1994.

Digital Library

[27]

H. Sondergard and P. Sestoft. Non-determinism in functional languages. The Computer Journal, 35(5):514-523, 1992.

Digital Library

[28]

N. Yoshida. Optimal reductions in weak-A- calculus with shared environments. In Proc. functional programming languages and comp'uter architecture, pages 243-252. ACM press, 1993.

Cited By

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
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
Accattoli BCondoluci AGuerrieri GCoen CKomendantskaya E(2019)Crumbling Abstract MachinesProceedings of the 21st International Symposium on Principles and Practice of Declarative Programming10.1145/3354166.3354169(1-15)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1145/3354166.3354169
Show More Cited By

Index Terms

A non-deterministic call-by-need lambda calculus

Recommendations

A call-by-need lambda calculus
POPL '95: Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages

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 ...
A non-deterministic call-by-need lambda calculus

In this paper we present a non-deterministic call-by-need (untyped) lambda calculus λ_nd with a constant choice and a let-syntax that models sharing. Our main result is that λ_nd has the nice operational properties of the standard lambda ...
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 ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ICFP '98: Proceedings of the third ACM SIGPLAN international conference on Functional programming

September 1998

351 pages

ISBN:1581130244

DOI:10.1145/289423

Chairmen:
Matthias Felleisen
Rice Univ., Houston, TX
,
Paul Hudak
Yale Univ., New Haven, CT
,
Christian Queinnec
Univ. Paris 6; and INRIA

ACM SIGPLAN Notices Volume 34, Issue 1
Jan. 1999
357 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/291251
Chairmen:
Matthias Felleisen
Rice Univ.
,
Paul Hudak
Yale Univ.
,
Editor:
A. Michael Berman
Issue’s Table of Contents

Copyright © 1998 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

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 29 September 1998

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Qualifiers

Article

Conference

ICFP98

Sponsor:

SIGPLAN

ICFP98: 1998 International Conference on Functional Programming

September 26 - 29, 1998

Maryland, Baltimore, USA

Acceptance Rates

ICFP '98 Paper Acceptance Rate 30 of 77 submissions, 39%;

Overall Acceptance Rate 333 of 1,064 submissions, 31%

Upcoming Conference

ICFP '25

Sponsor:
sigplan

ACM SIGPLAN International Conference on Functional Programming

October 12 - 18, 2025

Singapore , Singapore

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

22
Total Citations
View Citations
600
Total Downloads

Downloads (Last 12 months)99
Downloads (Last 6 weeks)19

Reflects downloads up to 15 Jan 2025

Other Metrics

View Author Metrics

Citations

Cited By

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
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
Accattoli BCondoluci AGuerrieri GCoen CKomendantskaya E(2019)Crumbling Abstract MachinesProceedings of the 21st International Symposium on Principles and Practice of Declarative Programming10.1145/3354166.3354169(1-15)Online publication date: 7-Oct-2019
https://dl.acm.org/doi/10.1145/3354166.3354169
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
Nishida YIgarashi ASabel DThiemann P(2018)Nondeterministic Manifest ContractsProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236964(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236964
Schmidt-Schauß MSabel DLämmel R(2015)Sharing-aware improvements in a call-by-need functional core languageProceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages10.1145/2897336.2897343(1-12)Online publication date: 14-Sep-2015
https://dl.acm.org/doi/10.1145/2897336.2897343
Schmidt-Schauß MSabel DFalaschi MAlbert E(2015)Improvements in a functional core language with call-by-need operational semanticsProceedings of the 17th International Symposium on Principles and Practice of Declarative Programming10.1145/2790449.2790512(220-231)Online publication date: 14-Jul-2015
https://dl.acm.org/doi/10.1145/2790449.2790512
Schmidt-Schauíß MSabel DNiehren JSchwinghammer J(2015)Observational program calculi and the correctness of translationsTheoretical Computer Science10.1016/j.tcs.2015.02.027577:C(98-124)Online publication date: 27-Apr-2015
https://dl.acm.org/doi/10.1016/j.tcs.2015.02.027
LÓPEZ-FRAGUAS FMARTIN-MARTIN ERODRÍGUEZ-HORTALÁ JSÁNCHEZ-HERNÁNDEZ J(2012)Rewriting and narrowing for constructor systems with call-time choice semanticsTheory and Practice of Logic Programming10.1017/S147106841200037314:2(165-213)Online publication date: 30-Oct-2012
https://doi.org/10.1017/S1471068412000373
Rau CSabel DSchmidt-Schauß M(2012)Correctness of program transformations as a termination problemProceedings of the 6th international joint conference on Automated Reasoning10.1007/978-3-642-31365-3_36(462-476)Online publication date: 26-Jun-2012
https://dl.acm.org/doi/10.1007/978-3-642-31365-3_36
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