research-article

Improvements in a functional core language with call-by-need operational semantics

Authors:

Manfred Schmidt-Schauß,

David SabelAuthors Info & Claims

PPDP '15: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming

Pages 220 - 231

https://doi.org/10.1145/2790449.2790512

Published: 14 July 2015 Publication History

Abstract

An improvement is a correct program transformation that optimizes the program, where the criterion is that the number of computation steps until a value is obtained is not increased in any context. This paper investigates improvements an untyped call-by-need lambdacalculus with letrec, case, constructors and seq. Besides showing that several local optimizations are improvements, the main result of the paper is a proof that common subexpression elimination is correct and an improvement, which proves a conjecture and thus closes a gap in the improvement theory of Moran and Sands. We also prove that several different length measures used for improvement in the call-by-need calculus of Moran and Sands and our calculus are equivalent.

References

[1]

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

Digital Library

[2]

R. Bird. Thinking functionally with Haskell. Cambridge University Press, 2014.

[3]

J. Gustavsson and D. Sands. Possibilities and limitations of call-by-need space improvement. In ICFP '01, pages 265--276, 2001.

Digital Library

[4]

J. Hackett and G. Hutton. Worker/wrapper/makes it/faster. In ICFP '14, pages 95--107, 2014.

Digital Library

[5]

J. Hughes. Why functional programming matters. Comput. J., 32(2): 98--107, 1989.

Digital Library

[6]

P. Johann and J. Voigtländer. The impact of seq on free theorems-based program transformations. Fund. Inform., 69(1-2):63--102, 2006.

Digital Library

[7]

A. Kutzner and M. Schmidt-Schauß. A nondeterministic call-by-need lambda calculus. In ICFP '98, pages 324--335, 1998.

Digital Library

[8]

S. Marlow, editor. Haskell 2010 -- Language Report. 2010.

[9]

A. K. D. Moran and D. Sands. Improvement in a lazy context: An operational theory for call-by-need. In POPL '99, pages 43--56, 1999.

Digital Library

[10]

S. Peyton Jones and S. Marlow. Secrets of the Glasgow Haskell Compiler inliner. J. Funct. Programming, 12(4+5):393--434, 2002.

Digital Library

[11]

D. Sabel and M. Schmidt-Schauß. A call-by-need lambda-calculus with locally bottom-avoiding choice: Context lemma and correctness of transformations. Math. Structures Comput. Sci., 18(03):501--553, 2008.

Digital Library

[12]

D. Sabel and M. Schmidt-Schauß. A contextual semantics for Concurrent Haskell with futures. In PPDP '11, pages 101--112, 2011.

Digital Library

[13]

D. Sands. Improvement theory and its applications. In Higher order operational techniques in semantics, pages 275--306. Cambridge university press, 1998.

Digital Library

[14]

M. Schmidt-Schauß and D. Sabel. On generic context lemmas for higher-order calculi with sharing. Theoret. Comput. Sci., 411(11-13): 1521--1541, 2010.

Digital Library

[15]

M. Schmidt-Schauß and D. Sabel. Contextual equivalences in call-by-need and call-by-name polymorphically typed calculi (preliminary report). In WPTE '14, volume 40 of OASICS, pages 63--74, 2014.

[16]

M. Schmidt-Schauß and D. Sabel. Improvements in a functional core language with call-by-need operational semantics. Frank report 55, Institut für Informatik, Goethe-Univ. Frankfurt, 2015.

[17]

M. Schmidt-Schauß, M. Schütz, and D. Sabel. Safety of Nöcker's strictness analysis. J. Funct. Programming, 18(04):503--551, 2008.

Digital Library

[18]

M. Schmidt-Schauß, E. Machkasova, and D. Sabel. Extending Abramsky's lazy lambda calculus: (non)-conservativity of embeddings. In RTA '13, volume 21 of LIPIcs, pages 239--254, 2013.

[19]

M. Schmidt-Schauß, D. Sabel, and E. Machkasova. Simulation in the call-by-need lambda-calculus with letrec, case, constructors, and seq. Log. Methods Comput. Sci., 11(1), 2015.

[20]

N. Sculthorpe, A. Farmer, and A. Gill. The HERMIT in the tree: Mechanizing program transformations in the GHC core language. In IFL '12, volume 8241 of LNCS, pages 86--103, 2013.

[21]

P. Sestoft. Deriving a lazy abstract machine. J. Funct. Programming, 7(3):231--264, 1997.

Digital Library

Cited By

Ceresa MJaskelioff M(2022)Effectful improvement theoryScience of Computer Programming10.1016/j.scico.2022.102792217:COnline publication date: 1-May-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102792
Hackett JHutton G(2019)Call-by-need is clairvoyant call-by-valueProceedings of the ACM on Programming Languages10.1145/33417183:ICFP(1-23)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341718
Handley MHutton G(2019)Improving HaskellTrends in Functional Programming10.1007/978-3-030-18506-0_6(114-135)Online publication date: 24-Apr-2019
https://doi.org/10.1007/978-3-030-18506-0_6
Show More Cited By

Index Terms

Improvements in a functional core language with call-by-need operational semantics
1. Theory of computation
  1. Semantics and reasoning
    1. Program semantics
      1. Operational semantics

Recommendations

Sharing-aware improvements in a call-by-need functional core language
IFL '15: Proceedings of the 27th Symposium on the Implementation and Application of Functional Programming Languages

Based on recent work on program improvements in call-by-need lambda calculi, this paper investigates improvements in a call-by-need polymorphically typed lambda-calculus with letrec, case, constructors, and seq. The goal is to contribute to the ...
Semantics of a Relational $λ$ -Calculus
Theoretical Aspects of Computing – ICTAC 2020
Abstract
We extend the $λ$ -calculus with constructs suitable for relational and functional–logic programming: non-deterministic choice, fresh variable introduction, and unification of expressions. In order to be able to unify $λ$ -expressions and still obtain a ...
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 ACM Other conferences

PPDP '15: Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming

July 2015

263 pages

ISBN:9781450335164

DOI:10.1145/2790449

Conference Chair:
Moreno Falaschi
University of Siena, Italy
,
Program Chair:
Elvira Albert
Complutense University of Madrid, Spain

Copyright © 2015 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]

In-Cooperation

SIGPLAN: ACM Special Interest Group on Programming Languages

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 July 2015

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Conference

PPDP '15

PPDP '15: 17th International Symposium on Principles and Practice of Declarative Programming

July 14 - 16, 2015

Siena, Italy

Acceptance Rates

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

21
Total Citations
View Citations
78
Total Downloads

Downloads (Last 12 months)2
Downloads (Last 6 weeks)0

Reflects downloads up to 20 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Ceresa MJaskelioff M(2022)Effectful improvement theoryScience of Computer Programming10.1016/j.scico.2022.102792217:COnline publication date: 1-May-2022
https://dl.acm.org/doi/10.1016/j.scico.2022.102792
Hackett JHutton G(2019)Call-by-need is clairvoyant call-by-valueProceedings of the ACM on Programming Languages10.1145/33417183:ICFP(1-23)Online publication date: 26-Jul-2019
https://dl.acm.org/doi/10.1145/3341718
Handley MHutton G(2019)Improving HaskellTrends in Functional Programming10.1007/978-3-030-18506-0_6(114-135)Online publication date: 24-Apr-2019
https://doi.org/10.1007/978-3-030-18506-0_6
Schmidt-Schauß MSabel DDallmeyer NSabel DThiemann P(2018)Sequential and Parallel Improvements in a Concurrent Functional Programming LanguageProceedings of the 20th International Symposium on Principles and Practice of Declarative Programming10.1145/3236950.3236952(1-13)Online publication date: 3-Sep-2018
https://dl.acm.org/doi/10.1145/3236950.3236952
Elliott C(2018)The simple essence of automatic differentiationProceedings of the ACM on Programming Languages10.1145/32367652:ICFP(1-29)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236765
Cong YAsai K(2018)Handling delimited continuations with dependent typesProceedings of the ACM on Programming Languages10.1145/32367642:ICFP(1-31)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236764
Hackett JHutton G(2018)Parametric polymorphism and operational improvementProceedings of the ACM on Programming Languages10.1145/32367632:ICFP(1-24)Online publication date: 30-Jul-2018
https://dl.acm.org/doi/10.1145/3236763
Lee CViola E(2018)The Coin Problem for Product TestsACM Transactions on Computation Theory10.1145/320178710:3(1-10)Online publication date: 8-Jun-2018
https://dl.acm.org/doi/10.1145/3201787
Pilipczuk MWahlström M(2018)Directed Multicut is W[1]-hard, Even for Four Terminal PairsACM Transactions on Computation Theory10.1145/320177510:3(1-18)Online publication date: 23-May-2018
https://dl.acm.org/doi/10.1145/3201775
Minahan DVolkovich I(2018)Complete Derandomization of Identity Testing and Reconstruction of Read-Once FormulasACM Transactions on Computation Theory10.1145/319683610:3(1-11)Online publication date: 23-May-2018
https://dl.acm.org/doi/10.1145/3196836
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Table of Contents