research-article

Crumbling Abstract Machines

Authors:

Beniamino Accattoli,

Andrea Condoluci,

Giulio Guerrieri,

Claudio Sacerdoti CoenAuthors Info & Claims

PPDP '19: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming

Article No.: 4, Pages 1 - 15

https://doi.org/10.1145/3354166.3354169

Published: 07 October 2019 Publication History

Abstract

Extending the λ-calculus with a construct for sharing, such as let expressions, enables a special representation of terms: iterated applications are decomposed by introducing sharing points in between any two of them, reducing to the case where applications have only values as immediate subterms.

This work studies how such a crumbled representation of terms impacts on the design and the efficiency of abstract machines for call-by-value evaluation. About the design, it removes the need for data structures encoding the evaluation context, such as the applicative stack and the dump, that get encoded in the environment. About efficiency, we show that there is no slowdown, clarifying in particular a point raised by Kennedy, about the potential inefficiency of such a representation.

Moreover, we prove that everything smoothly scales up to the delicate case of open terms, needed to implement proof assistants. Along the way, we also point out that continuation-passing style transformations--that may be alternatives to our representation--do not scale up to the open case.

References

[1]

Beniamino Accattoli. 2012. An Abstract Factorization Theorem for Explicit Substitutions. In 23rd International Conference on Rewriting Techniques and Applications, RTA 2012 (LIPIcs), Vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 6--21. https://doi.org/10.4230/LIPIcs.RTA.2012.6

[2]

Beniamino Accattoli. 2016. The Useful MAM, a Reasonable Implementation of the Strong λ-Calculus. In Logic, Language, Information, and Computation - 23rd International Workshop, WoLLIC 2016 (Lecture Notes in Computer Science), Vol. 9803. Springer, 1--21. https://doi.org/10.1007/978-3-662-52921-8_1

[3]

Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. 2014. Distilling abstract machines. In 19th ACM SIGPLAN International Conference on Functional Programming, ICFP 2014. ACM, 363--376. https://doi.org/10.1145/2628136.2628154

Digital Library

[4]

Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. 2015. A Strong Distillery. In Programming Languages and Systems - 13th Asian Symposium, APLAS 2015 (Lecture Notes in Computer Science), Vol. 9458. Springer, 231--250. https://doi.org/10.1007/978-3-319-26529-2_13

[5]

Beniamino Accattoli and Bruno Barras. 2017. Environments and the Complexity of Abstract Machines. In 19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017. ACM, 4--16. https://doi.org/10.1145/3131851.3131855

[6]

Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, and Claudio Sacerdoti Coen. 2019. Crumbling Abstract Machines (Extended Version). CoRR abs/1907.06057 (2019).

[7]

Beniamino Accattoli and Ugo Dal Lago. 2016. (Leftmost-Outermost) Beta Reduction is Invariant, Indeed. Logical Methods in Computer Science 12, 1 (2016). https://doi.org/10.2168/LMCS-12(1:4)2016

[8]

Beniamino Accattoli and Giulio Guerrieri. 2016. Open Call-by-Value. In Programming Languages and Systems - 14th Asian Symposium, APLAS 2016 (Lecture Notes in Computer Science), Vol. 10017. Springer, 206--226. https://doi.org/10.1007/978-3-319-47958-3_12

[9]

Beniamino Accattoli and Giulio Guerrieri. 2017. Implementing Open Call-by-Value. In Fundamentals of Software Engineering - 7th International Conference, FSEN 2017 (Lecture Notes in Computer Science), Vol. 10522. Springer, 1--19. https://doi.org/10.1007/978-3-319-68972-2_1

[10]

Beniamino Accattoli and Giulio Guerrieri. 2018. Types of Fireballs. In Programming Languages and Systems - 16th Asian Symposium, APLAS 2018 (Lecture Notes in Computer Science), Vol. 11275. Springer, 45--66. https://doi.org/10.1007/978-3-030-02768-1_3

[11]

Beniamino Accattoli and Claudio Sacerdoti Coen. 2015. On the Relative Usefulness of Fireballs. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015. IEEE Computer Society, 141--155. https://doi.org/10.1109/LICS.2015.23

Digital Library

[12]

Beniamino Accattoli and Claudio Sacerdoti Coen. 2017. On the value of variables. Information and Computation 255 (2017), 224--242. https://doi.org/10.1016/j.ic.2017.01.003

[13]

Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Odersky, and Philip Wadler. 1995. The Call-by-Need Lambda Calculus. In 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'95. ACM Press, 233--246. https://doi.org/10.1145/199448.199507

[14]

Pierre Crégut. 1990. An Abstract Machine for Lambda-Terms Normalization. In LISP and Functional Programming. 333--340. https://doi.org/10.1145/91556.91681

[15]

Olivier Danvy. 1994. Back to Direct Style. Science of Computer Programming 22, 3 (1994), 183--195. https://doi.org/10.1016/0167-6423(94)00003-4

Digital Library

[16]

Olivier Danvy. 2003. A New One-Pass Transformation into Monadic Normal Form. In Compiler Construction, 12th International Conference, CC 2003 (Lecture Notes in Computer Science), Vol. 2622. Springer, 77--89. https://doi.org/10.1007/3-540-36579-6_6

[17]

Olivier Danvy and Andrzej Filinski. 1992. Representing Control: A Study of the CPS Transformation. Mathematical Structures in Computer Science 2, 4 (1992), 361--391. https://doi.org/10.1017/S0960129500001535

[18]

Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The essence of compiling with continuations (with retrospective). In 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, A Selection, PLDI 1993. ACM, 502--514. https://doi.org/10.1145/989393.989443

[19]

Álvaro García-Pérez, Pablo Nogueira, and Juan José Moreno-Navarro. 2013. Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order. In 15th International Symposium on Principles and Practice of Declarative Programming, PPDP'13. ACM, 85--96. https://doi.org/10.1145/2505879.2505887

Digital Library

[20]

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. ACM, 235--246. https://doi.org/10.1145/581478.581501

Digital Library

[21]

Giulio Guerrieri. 2019. Towards a Semantic Measure of the Execution Time in Call-by-Value lambda-Calculus. In Proceedings Twelfth Workshop on Developments in Computational Models and Ninth Workshop on Intersection Types and Related Systems, DCM/ITRS 2018. (EPTCS), Vol. 293. 57--72. https://doi.org/10.4204/EPTCS.293.5

[22]

Giulio Guerrieri, Luca Paolini, and Simona Ronchi Della Rocca. 2017. Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus. Logical Methods in Computer Science 13, 4 (2017). https://doi.org/10.23638/LMCS-13(4:29)2017

[23]

John Hatcliff and Olivier Danvy. 1994. A Generic Account of Continuation-Passing Styles. In 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1994. ACM Press, 458--471. https://doi.org/10.1145/174675.178053

Digital Library

[24]

Andrew Kennedy. 2007. Compiling with continuations, continued. In Proceedings of the 12th ACM SIGPLAN International Conference on Functional Programming, ICFP 2007. ACM, 177--190. https://doi.org/10.1145/1291151.1291179

Digital Library

[25]

Arne Kutzner and Manfred Schmidt-Schauß. 1998. A Non-Deterministic Call-by-Need Lambda Calculus. In Third ACM SIGPLAN International Conference on Functional Programming, ICFP 1998. ACM, 324--335. https://doi.org/10.1145/289423.289462

Digital Library

[26]

Søren B. Lassen. 2005. Eager Normal Form Bisimulation. In 20th IEEE Symposium on Logic in Computer Scienc, LICS 2005. IEEE Computer Society, 345--354. https://doi.org/10.1109/LICS.2005.15

[27]

John Launchbury. 1993. A Natural Semantics for Lazy Evaluation. In Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1993. ACM Press, 144--154. https://doi.org/10.1145/158511.158618

Digital Library

[28]

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

[29]

Eugenio Moggi. 1991. Notions of Computation and Monads. Information and Computation 93, 1 (1991), 55--92. https://doi.org/10.1016/0890-5401(91)90052-4

Digital Library

[30]

Luca Paolini and Simona Ronchi Della Rocca. 1999. Call-by-value Solvability. ITA 33, 6 (1999), 507--534. https://doi.org/10.1051/ita:1999130

[31]

Gordon D. Plotkin. 1975. Call-by-Name, Call-by-Value and the lambda-Calculus. Theoretical Computer Science 1, 2 (1975), 125--159. https://doi.org/10.1016/0304-3975(75)90017-1

[32]

Simona Ronchi Della Rocca and Luca Paolini. 2004. The Parametric λ-Calculus - A Metamodel for Computation. Springer. https://doi.org/10.1007/978-3-662-10394-4

[33]

Amr Sabry and Matthias Felleisen. 1993. Reasoning about Programs in Continuation-Passing Style. Lisp and Symbolic Computation 6, 3-4 (1993), 289--360.

Digital Library

[34]

Peter Sestoft. 1997. Deriving a Lazy Abstract Machine. Journal of Functional Programming 7, 3 (1997), 231--264.

Digital Library

[35]

Christopher P. Wadsworth. 1971. Semantics and pragmatics of the lambda-calculus. PhD Thesis. Oxford. Chapter 4.

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
Accattoli BBarenbaum P(2023)A Diamond Machine for Strong EvaluationProgramming Languages and Systems10.1007/978-981-99-8311-7_4(69-90)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8311-7_4
Accattoli BGuerrieri G(2022)The theory of call-by-value solvabilityProceedings of the ACM on Programming Languages10.1145/35476526:ICFP(855-885)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547652
Show More Cited By

Crumbling Abstract Machines
1. Mathematics of computing
  1. Continuous mathematics
    1. Calculus
  2. Mathematical analysis
    1. Calculus
2. Theory of computation
  1. Semantics and reasoning
    1. Program semantics

Recommendations

The Linear Logical Abstract Machine

We derive an abstract machine from the Curry-Howard correspondence with a sequent calculus presentation of Intuitionistic Propositional Linear Logic. The states of the register based abstract machine comprise a low-level code block, a register bank and ...
Distilling abstract machines
ICFP '14: Proceedings of the 19th ACM SIGPLAN international conference on Functional programming

It is well-known that many environment-based abstract machines can be seen as strategies in lambda calculi with explicit substitutions (ES). Recently, graphical syntaxes and linear logic led to the linear substitution calculus (LSC), a new approach to ...
Nominal Techniques in Isabelle/HOL

This paper describes a formalisation of the lambda-calculus in a HOL-based theorem prover using nominal techniques. Central to the formalisation is an inductive set that is bijective with the alpha-equated lambda-terms. Unlike de-Bruijn indices, however,...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Other conferences

PPDP '19: Proceedings of the 21st International Symposium on Principles and Practice of Declarative Programming

October 2019

280 pages

ISBN:9781450372497

DOI:10.1145/3354166

Program Chair:
Ekaterina Komendantskaya

Copyright © 2019 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].

In-Cooperation

Sony: Sony Corporation

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 07 October 2019

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article
Research
Refereed limited

Conference

PPDP '19

PPDP '19: Principles and Practice of Programming Languages 2019

October 7 - 9, 2019

Porto, Portugal

Acceptance Rates

PPDP '19 Paper Acceptance Rate 19 of 45 submissions, 42%;

Overall Acceptance Rate 230 of 486 submissions, 47%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

8
Total Citations
View Citations
92
Total Downloads

Downloads (Last 12 months)7
Downloads (Last 6 weeks)1

Reflects downloads up to 18 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
Accattoli BBarenbaum P(2023)A Diamond Machine for Strong EvaluationProgramming Languages and Systems10.1007/978-981-99-8311-7_4(69-90)Online publication date: 26-Nov-2023
https://dl.acm.org/doi/10.1007/978-981-99-8311-7_4
Accattoli BGuerrieri G(2022)The theory of call-by-value solvabilityProceedings of the ACM on Programming Languages10.1145/35476526:ICFP(855-885)Online publication date: 31-Aug-2022
https://dl.acm.org/doi/10.1145/3547652
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
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 BDal Lago UVanoni G(2021)The (In)Efficiency of interactionProceedings of the ACM on Programming Languages10.1145/34343325:POPL(1-33)Online publication date: 4-Jan-2021
https://dl.acm.org/doi/10.1145/3434332
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
Accattoli BDal Lago UVanoni GGabbrielli MAbel ACheney J(2020)The Machinery of InteractionProceedings of the 22nd International Symposium on Principles and Practice of Declarative Programming10.1145/3414080.3414108(1-15)Online publication date: 8-Sep-2020
https://dl.acm.org/doi/10.1145/3414080.3414108

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