pith. sign in

arxiv: 1907.06057 · v1 · pith:GPTZ4WDAnew · submitted 2019-07-13 · 💻 cs.LO · cs.PL

Crumbling Abstract Machines

Beniamino Accattoli , Andrea Condoluci , Giulio Guerrieri , Claudio Sacerdoti Coen This is my paper

Pith reviewed 2026-05-24 21:57 UTC · model grok-4.3

classification 💻 cs.LO cs.PL
keywords abstract machineslambda calculuscall-by-valuesharingevaluation contextsopen termscontinuation-passing style
0
0 comments X

The pith

A crumbled representation of terms lets call-by-value abstract machines encode evaluation contexts inside the environment rather than in separate stacks and dumps, with no slowdown even for open terms.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper studies a way to represent lambda terms that breaks chains of applications into single steps by inserting sharing points, so every application has only values as immediate arguments. This form moves what used to live in the machine's applicative stack and dump directly into the environment. The resulting machine design is simpler because those context structures disappear. Measurements and proofs show the change preserves the original number of steps. The same representation continues to work when terms contain free variables, which is required for proof-assistant implementations, while continuation-passing style does not.

Core claim

By introducing sharing points between every pair of applications, the crumbled representation reduces every application to the case where the function and argument are both values. The evaluation context that would otherwise be stored in explicit stack and dump structures is instead recorded inside the environment. This change removes those data structures from the machine while preserving the exact number of reduction steps, and the same encoding works without modification on open terms.

What carries the argument

The crumbled representation of terms, which decomposes iterated applications by inserting sharing points so that every application has only values as immediate subterms.

If this is right

  • The abstract machine no longer requires separate data structures for the applicative stack and the dump.
  • The number of reduction steps performed by the machine remains identical to the step count of the original machine.
  • The same machine definition continues to evaluate open terms without additional machinery.
  • Continuation-passing style transformations cannot be used in place of the crumbled representation when terms may be open.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • Evaluators written for proof assistants can adopt the representation to avoid maintaining separate context stacks while still supporting free variables.
  • The encoding of contexts into environments may reduce the constant factors in memory traffic for implementations that already use environments heavily.
  • Similar decompositions could be tried for call-by-name or call-by-need strategies to see whether the same removal of explicit context structures occurs.

Load-bearing premise

Recording the evaluation context inside the environment adds no extra work or changes the observable behavior compared with keeping an explicit stack and dump.

What would settle it

Implement both the crumbled machine and a conventional machine on the same set of closed and open terms, then compare the total number of machine transitions required to reach a value; any consistent excess in the crumbled version would refute the no-slowdown claim.

Figures

Figures reproduced from arXiv: 1907.06057 by Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen, Giulio Guerrieri.

Figure 1
Figure 1. Figure 1: Pif calculus λ if Plot. 3 Crumbled Evaluation, Informally Decomposing applications. The idea is to forbid the nest￾ing of non-value constructs such as applications and if-then-else without losing expressive power. To ease the explanation, we focus on nested applications and forget aboutif-then-else— they do not pose any difficulty. Terms such as (tu)s or t(us) are then represented as(λx.(xs))(tu) and (λx.(… view at source ↗
Figure 2
Figure 2. Figure 2: The conditional fireball calculus λ if fire. Theorem 5.10 (The Crumble GLAM is bilinear up to search and (un)plugging). For any closed term t and any Crumble GLAM execution ρ : t →∗ Cr c, the cost of implementing ρ on a RAM is O((|ρ|p + 1) · |t|) plus the cost of plugging and un￾plugging. OCaml implementation. In Appendix D.4 we introduce the Pointed Crumble GLAM, a refinement of the Crumble GLAM making ex… view at source ↗
Figure 3
Figure 3. Figure 3: Kennedy’s example of evaluation in the monadic calculus where the number of commutation steps is quadratic in the number of βv-steps (→i stands for the composition of i →-steps). The i th βv -step is immediately followed by i commutation steps →let that just append two lists of substitutions moving one substitution at a time. Therefore, to reach a normal form one needs n βv -steps and n(n + 1)/2 let-steps.… view at source ↗
Figure 4
Figure 4. Figure 4: Evaluation: closed (left) vs open (right) [PITH_FULL_IMAGE:figures/full_fig_p037_4.png] view at source ↗
read the original abstract

Extending the lambda-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.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript introduces a crumbled representation of lambda terms extended with sharing (let expressions), which decomposes iterated applications so that they have only values as immediate subterms. It studies the consequences for call-by-value abstract machines, claiming that this representation eliminates the need for explicit data structures encoding the evaluation context (applicative stack and dump) by encoding them instead in the environment, proves there is no slowdown relative to standard machines, and proves that the approach scales smoothly to open terms (in contrast to CPS transformations, which do not).

Significance. If the central claims hold, the work provides a meaningful simplification in abstract machine design while preserving efficiency and extending applicability to open terms, which is relevant for proof assistants. The explicit contrast with CPS and the resolution of the inefficiency concern noted by Kennedy are useful contributions. The scaling result to open terms is a notable strength.

minor comments (2)
  1. The introduction would benefit from a small concrete example illustrating the crumbling transformation on a term with multiple applications.
  2. Notation for the environment encoding of contexts could be made more uniform across definitions and figures for easier cross-reference.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for their positive summary of the manuscript and for recommending acceptance. The report correctly identifies the key contributions regarding the crumbled representation, the elimination of explicit evaluation contexts, the efficiency proof addressing Kennedy's concern, and the scaling to open terms in contrast to CPS.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper introduces a crumbled term representation via let-sharing and derives its consequences for abstract machine design and complexity via direct proofs on the new representation and standard call-by-value semantics. No step reduces a claimed prediction or theorem to a fitted parameter, self-citation chain, or definitional equivalence with its own input. The scaling to open terms and the CPS comparison are established by explicit semantic arguments rather than by renaming or smuggling prior results. The derivation chain is therefore self-contained.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The work relies on standard lambda calculus foundations without introducing new free parameters or invented entities.

axioms (1)
  • domain assumption Standard call-by-value evaluation rules for lambda calculus with let expressions
    The paper builds its machine designs and efficiency claims on conventional CBV semantics.

pith-pipeline@v0.9.0 · 5705 in / 1041 out tokens · 36073 ms · 2026-05-24T21:57:28.379762+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Forward citations

Cited by 1 Pith paper

Reviewed papers in the Pith corpus that reference this work. Sorted by Pith novelty score.

  1. A Reversible Crumbling Abstract Machine for Plotkin's Call-by-Value

    cs.LO 2026-05 unverdicted novelty 6.0

    A crumbling abstract machine yields a reversible Landauer's embedding for call-by-value lambda calculus with constant space overhead per step.

Reference graph

Works this paper leans on

134 extracted references · 134 canonical work pages · cited by 1 Pith paper

  1. [1]

    Beniamino Accattoli. 2012. An Abstract Factorization The- orem for Explicit Substitutions. In 23rd International Confer- ence on Rewriting Techniques and Applications, RTA 2012 (LI PIcs), Vol. 15. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 6–21 . h/t_tps://doi.org/10.4230/LIPIcs.RTA.2012.6

    work page doi:10.4230/lipics.rta.2012.6 2012

  2. [2]

    Beniamino Accattoli. 2016. The Useful MAM, a Reasonable Im- plementation of the Strong λ-Calculus. In Logic, Language, Infor- mation, and Computation - 23rd International Workshop, WoL LIC 2016 (Lecture Notes in Computer Science) , Vol. 9803. Springer, 1–21. h/t_tps://doi.org/10.1007/978-3-662-52921-8_1

    work page doi:10.1007/978-3-662-52921-8_1 2016

  3. [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. h/t_tps://doi.org/10.1145/2628136.2628154

    work page doi:10.1145/2628136.2628154 2014

  4. [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. h/t_tps://doi.org/10.1007/978-3-319-26529-2_13

    work page doi:10.1007/978-3-319-26529-2_13 2015

  5. [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 2 017. ACM, 4–16. h/t_tps://doi.org/10.1145/3131851.3131855

    work page doi:10.1145/3131851.3131855 2017

  6. [6]

    Beniamino Accattoli and Ugo Dal Lago. 2016. (Leftmost-Outerm ost) Beta Reduction is Invariant, Indeed. Logical Methods in Computer Sci- ence 12, 1 (2016). h/t_tps://doi.org/10.2168/LMCS-12(1:4)2016

    work page doi:10.2168/lmcs-12(1:4)2016 2016

  7. [7]

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

    work page doi:10.1007/978-3-319-47958-3_12 2016

  8. [8]

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

    work page doi:10.1007/978-3-319-68972-2_1 2017

  9. [9]

    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. h/t_tps://doi.org/10.1007/978-3-030-02768-1_3

    work page doi:10.1007/978-3-030-02768-1_3 2018

  10. [10]

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

    work page doi:10.1109/lics.2015.23 2015

  11. [11]

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

    work page doi:10.1016/j.ic.2017.01.003 2017

  12. [12]

    Ariola, Matthias Felleisen, John Maraist, Martin Oder- sky, and Philip Wadler

    Zena M. Ariola, Matthias Felleisen, John Maraist, Martin Oder- sky, and Philip Wadler. 1995. The Call-by-Need Lambda Cal- culus. In 22nd ACM SIGPLAN-SIGACT Symposium on Princi- ples of Programming Languages, POPL’95 . ACM Press, 233–246. h/t_tps://doi.org/10.1145/199448.199507

    work page doi:10.1145/199448.199507 1995

  13. [13]

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

    work page doi:10.1145/91556.91681 1990

  14. [14]

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

    work page doi:10.1016/0167-6423(94)00003-4 1994

  15. [15]

    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–

    work page 2003

  16. [16]

    h/t_tps://doi.org/10.1007/3-540-36579-6_6

    work page doi:10.1007/3-540-36579-6_6

  17. [17]

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

    work page doi:10.1017/s0960129500001535 1992

  18. [18]

    Duba, and Matthias Fell eisen

    Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Fell eisen

    work page

  19. [19]

    In 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, A Selection, PLDI 1993

    The essence of compiling with continuations (with retrospec- tive). In 20 Years of the ACM SIGPLAN Conference on Programming Language Design and Implementation 1979-1999, A Selection, PLDI 1993. ACM, 502–514. h/t_tps://doi.org/10.1145/989393.989443

    work page doi:10.1145/989393.989443 1979

  20. [20]

    Álvaro García-Pérez, Pablo Nogueira, and Juan José Moreno- Navarro

    work page

  21. [21]

    In 15th International Sympo- sium on Principles and Practice of Declarative Programming , PPDP’13

    Deriving the full-reducing Krivine machine from the small-step operational semantics of normal order. In 15th International Sympo- sium on Principles and Practice of Declarative Programming , PPDP’13. ACM, 85–96. h/t_tps://doi.org/10.1145/2505879.2505887

    work page doi:10.1145/2505879.2505887

  22. [22]

    Benjamin Grégoire and Xavier Leroy. 2002. A compiled implementa - tion of strong reduction. In Proceedings of the Seventh ACM SIGPLAN International Conference on Functional Programming, ICFP ’02. ACM, 235–246. h/t_tps://doi.org/10.1145/581478.581501

    work page doi:10.1145/581478.581501 2002

  23. [23]

    John Hatcliff and Olivier Danvy. 1994. A Generic Account of Continuation-Passing Styles. In 21st ACM SIGPLAN-SIGACT Sympo- sium on Principles of Programming Languages, POPL 1994 . ACM Press, 458–471. h/t_tps://doi.org/10.1145/174675.178053 Conference’17, July 2017, Washington, DC, USA Acca/t_toli, Condoluci, Guerrieri, and Sacerdoti Coen

    work page doi:10.1145/174675.178053 1994

  24. [24]

    Andrew Kennedy. 2007. Compiling with continuations, contin- ued. In Proceedings of the 12th ACM SIGPLAN International Con- ference on Functional Programming, ICFP 2007 . ACM, 177–190. h/t_tps://doi.org/10.1145/1291151.1291179

    work page doi:10.1145/1291151.1291179 2007

  25. [25]

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

    work page doi:10.1145/289423.289462 1998

  26. [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. h/t_tps://doi.org/10.1109/LICS.2005.15

    work page doi:10.1109/lics.2005.15 2005

  27. [27]

    John Launchbury. 1993. A Natural Semantics for Lazy Evalua tion. In Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Princi- ples of Programming Languages, POPL 1993 . ACM Press, 144–154. h/t_tps://doi.org/10.1145/158511.158618

    work page doi:10.1145/158511.158618 1993

  28. [28]

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

    work page 1998

  29. [29]

    Eugenio Moggi. 1991. Notions of Computation and Mon- ads. Information and Computation 93, 1 (1991), 55–92. h/t_tps://doi.org/10.1016/0890-5401(91)90052-4

    work page doi:10.1016/0890-5401(91)90052-4 1991

  30. [30]

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

    work page doi:10.1051/ita:1999130 1999

  31. [31]

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

    work page doi:10.1016/0304-3975(75)90017-1 1975

  32. [32]

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

    work page doi:10.1007/978-3-662-10394-4 2004

  33. [33]

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

    work page 1993

  34. [34]

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

    work page 1997

  35. [35]

    Wadsworth

    Christopher P. Wadsworth. 1971. Semantics and pragmatics of the lambda-calculus. PhD Thesis. Oxford. Chapter 4. Technical Appendix A Comments on Related Works Here we discuss in detail Kennedy’s potential slowdown and provide a counter-example to the scalability of the CPS transformation to open terms. Kennedy Kennedy [ 21] compares three different calculi...

    work page 1971

  36. [36]

    In his example, the number of commutations is quadratic in the number of β/v.alt-steps, since the i th β/v.alt-step is immediately followed by i commutation steps

    where the number of commutations is not bounded linearly by the number of β/v.alt-steps and blames the inefficiency of his compiler on that. In his example, the number of commutations is quadratic in the number of β/v.alt-steps, since the i th β/v.alt-step is immediately followed by i commutation steps. ANFs are just canonical shapes of monadic terms where ...

    work page 2017

  37. [37]

    (x /v.alt, e)↓ = (x, e)↓(/v.alt, e)↓ for every variable x and crum- bled value /v.alt

    work page

  38. [38]

    (if x then c else d, e)↓ = if (x, e)↓ then (c @ e)↓ else (d @ e)↓ for every variable x and crum- bles c, d. Proof. By induction on e: • Case e = ϵ:

    work page

  39. [39]

    (x /v.alt, ϵ)↓ = (x /v.alt)↓ = x↓ /v.alt↓ = (x, ϵ)↓(/v.alt, ϵ)↓

    work page

  40. [40]

    • Case e = e ′[/y.alt/shortleftarrowb] for some e ′, /y.alt, b:

    (if x then c else d, ϵ)↓ = (if x then c else d)↓ = (if x↓ then c↓ else d↓) = (if ((x, ϵ))↓ then ((c @ ϵ))↓ else ((d @ ϵ))↓). • Case e = e ′[/y.alt/shortleftarrowb] for some e ′, /y.alt, b:

    work page

  41. [41]

    By the definition of (·)↓, (x /v.alt, e ′[/y.alt/shortleftarrowb])↓ = (x /v.alt, e ′)↓{ /y.alt/shortleftarrowb↓} . By i.h. (x /v.alt, e ′)↓{ /y.alt/shortleftarrowb↓} = ((x, e ′)↓(/v.alt, e ′)↓){/y.alt/shortleftarrowb↓} . By the definition of substitution, ((x, e ′)↓(/v.alt, e ′)↓){/y.alt/shortleftarrowb↓} = ((x, e ′)↓{ /y.alt/shortleftarrowb↓})((/v.alt, e ′...

    work page

  42. [42]

    By the definition of (·)↓, (if x then c else d, e ′[/y.alt/shortleftarrowb])↓ = (if x then c else d, e ′)↓{ /y.alt/shortleftarrowb↓} . By i.h. (if x then c else d, e ′)↓{ /y.alt/shortleftarrowb↓} = (if (x, e ′)↓ then (c @ e ′)↓ else (d @ e ′)↓){/y.alt/shortleftarrowb↓} . By the definition of substitution, (if (x, e ′)↓ then (c @ e ′)↓ else (d @ e ′)↓){/y.al...

    work page

  43. [43]

    Plugging: If C # c and C↓ is a λ-context and C ⟨c⟩ is well-named, then C ⟨c⟩↓ = C↓⟨c↓⟩

    work page

  44. [44]

    Composition: If C # C ′ and C ⟨C ′⟩ is well-named, where C↓ and C ′ ↓ are contexts, then C ⟨C ′⟩↓ = C↓⟨C ′ ↓⟩, which is a context. Proof. 1. If C ≔ ⟨·⟩ , then C↓ = ⟨·⟩ and so C ⟨c⟩↓ = c↓ = C↓⟨c↓⟩. Otherwise C ≔ (b, e[x/shortleftarrow⟨·⟩]) with c = (b ′, e ′); since C ⟨c⟩ = (b, e[x/shortleftarrowb ′] e ′)is well-named, then x /nelement dom(e ′); therefore,...

    work page

  45. [45]

    Conference’17, July 2017, Washington, DC, USA Acca/t_toli, Condoluci, Guerrieri, and Sacerdoti Coen If C ≔ ⟨·⟩ , then C↓ = ⟨·⟩ and C ⟨C ′⟩ = C ′, thus C ⟨C ′⟩↓ = C ′ ↓ = C↓⟨C ′ ↓⟩

    The composition of two contexts is a context, thus C↓⟨C ′ ↓⟩ is a context since C↓ and C ′ ↓ are so. Conference’17, July 2017, Washington, DC, USA Acca/t_toli, Condoluci, Guerrieri, and Sacerdoti Coen If C ≔ ⟨·⟩ , then C↓ = ⟨·⟩ and C ⟨C ′⟩ = C ′, thus C ⟨C ′⟩↓ = C ′ ↓ = C↓⟨C ′ ↓⟩. If C ′ ≔ ⟨·⟩ , then C ′ ↓ = ⟨·⟩ and C ⟨C ′⟩ = C, so C ⟨C ′⟩↓ = C↓ = C↓⟨C ′ ...

    work page 2017

  46. [46]

    Freshness: t is well-named

    work page

  47. [47]

    Closure: if t is closed, then fv(t)= ∅

    work page

  48. [48]

    Disjointedness: dom(C) ∩fv(b)= ∅ if t = C ⟨(b, e)⟩

    work page

  49. [49]

    Bodies: every body in t is the translation of a term

    work page

  50. [50]

    Contextual decoding: if t = C ⟨c⟩, then C↓ is a right v-context. Proof

    work page

  51. [52]

    It follows immediately from the freshness condition in the definition of translation

    work page

  52. [53]

    By induction on t and by cases on the rules defining the translation

    work page

  53. [54]

    Cases: • λ-Value, i.e

    By induction on the size of t. Cases: • λ-Value, i.e. t = /v.alt. Then t = (/v.alt, ϵ)and so the only possible crumble context C such that t = C ⟨c⟩ for some crumble c is C = ⟨·⟩ and so C↓ = ⟨·⟩ , which is a right v-context. • λ-Value applied to value, i.e. t = /v.alt/v.alt′. As in the previ- ous case. • Application applied to a value , i.e. t = u/v.altwi...

    work page 2017

  54. [56]

    Bodies: every body occurring in c is a subterm (up to renaming) of the initial crumble

    work page

  55. [57]

    Weak contextual decoding: for every decomposition C ⟨(b, e/v.alt)⟩where b is not a crumbled value, if C ′′ is a prefix of C then C ′′ ↓ is a right v-context. Proof. By induction on the length of the reduction sequence leading to the crumble. The base cases hold by Lemma 4.5 (by noting that for Point 4, Lemma 4.5.5 implies the weaker statement Lemma 5.5.4)....

    work page

  56. [58]

    Hence the claim follows from the i.h

    The substitution transitions subvar, subl , subif do not change the set of variables occurring on the lhs of substitutions outside abstractions because they copy a value that does not contain any. Hence the claim follows from the i.h.. For transition β/v.altthe claim fol- lows from the side condition. For the remaining rules i/f_t, iff, ife, @e the claim f...

    work page

  57. [59]

    Transition β/v.altcopies to the top level and renames the body of an abstraction

    The substitution transitions subvar, subl , subif do not change the domain of the crumble and only copy to the left a value from the environment, and the claim follows from the i.h.. Transition β/v.altcopies to the top level and renames the body of an abstraction. By the properties of α - renaming fv((c @ [x/shortleftarrow/v.alt])α )= fv(c @ [x/shortlefta...

    work page

  58. [60]

    The rule β/v.altcopies and renames the body of an abstraction that was al- ready in the environment, and the claim follows from the i.h

    The rules subvar, subl , subif may copy an abstraction, but the abstraction was already in the environment, and the claim follows from the i.h.. The rule β/v.altcopies and renames the body of an abstraction that was al- ready in the environment, and the claim follows from the i.h. since the translation commutes with the re- naming of free variables (Remar...

    work page 2017

  59. [61]

    Cases of the reduction step C ′⟨(b ′, e ′ /v.alt)⟩ →a C ⟨(b, e/v.alt)⟩: – Case β/v.alt: C ′⟨((λx .c)/v.alt, e/v.alt)⟩ → β/v.alt C ′⟨cα @ ([x α /shortleftarrow/v.alt] e/v.alt)⟩

    Let b ′′ → n C ′⟨(b ′, e ′ /v.alt)⟩ → a C ⟨(b, e/v.alt)⟩(where b is not a practical value). Cases of the reduction step C ′⟨(b ′, e ′ /v.alt)⟩ →a C ⟨(b, e/v.alt)⟩: – Case β/v.alt: C ′⟨((λx .c)/v.alt, e/v.alt)⟩ → β/v.alt C ′⟨cα @ ([x α /shortleftarrow/v.alt] e/v.alt)⟩. Let C ′′be a prefix of C. There are two sub-cases: ∗ C ′′is a prefix of C ′: by i.h. C ′′ ...

    work page 2017

  60. [62]

    Initialization: t ↓ = t for every term t

    work page

  61. [63]

    Principal projection: if c → a d then c↓ → a d↓, for any rule a ∈ { β/v.alt, i/f_t, iff, ife, @e}

    work page

  62. [64]

    Overhead transparency: if c → a d then c↓ = d↓ for any rule a ∈ { subvar, subl , subif }

    work page

  63. [65]

    Determinism: the transition → Cr is deterministic

    work page

  64. [66]

    Halt: if c is Cr-normal then c↓ is Pi f -normal

    work page

  65. [67]

    Therefore, the Crumble GLAM, Pif evaluation → pif, and the read-back (·)↓ form an implementation system

    Overhead termination: → a terminates, for any rule a ∈ { subvar, subl , subif } . Therefore, the Crumble GLAM, Pif evaluation → pif, and the read-back (·)↓ form an implementation system. Proof. 1. See Prop. 4.2

    work page

  66. [68]

    See Lemma D.11, since c is closed by Lemma 5.5.2

    work page

  67. [69]

    □ D.3 Proofs of Subsect

    Immediate consequence of Lemma 5.8 (proved inde- pendently). □ D.3 Proofs of Subsect. 5.3 Proof of (Prop. 5.7). Let t be a term and /v.alta value. Then:

    work page

  68. [70]

    | t | var ≤ 1; and | t | var = 1 if and only if t is a variable

    work page

  69. [71]

    | /v.alt| var ≤ 1; and | /v.alt| var = 1 if and only if /v.altis a variable. Proof. By mutual induction on t and /v.alt: • Variable, i.e. /v.alt= t ≔ x : then /v.alt= x and t = (x, ϵ), hence | /v.alt| var = | t | var = 1. • Boolean or error , i.e. /v.alt= t ∈ { true, false, err} : then /v.alt= /v.altand t = (/v.alt, ϵ), hence | /v.alt| var = | t | var = 0...

    work page 2017

  70. [74]

    Rightmost: e¦ = (e ¦ e/v.alt)for some environment e and some /v.alt-environment e/v.alt. Proof p. 27Theorem D.15 (Implementation). Let e¦ be a reachable pointed environment in the Pointed Crumble GLAM

    work page

  71. [80]

    Therefore, the Pointed Crumble GLAM (with its transition function → pCr), the Crumble GLAM (with→ Cr), and the read- back (·)⇓ form an implementation system

    Overhead termination: → sea terminates. Therefore, the Pointed Crumble GLAM (with its transition function → pCr), the Crumble GLAM (with→ Cr), and the read- back (·)⇓ form an implementation system. Conference’17, July 2017, Washington, DC, USA Acca/t_toli, Condoluci, Guerrieri, and Sacerdoti Coen Complexity We reuse the measures introduced in Sub- sect. 5...

    work page 2017

  72. [82]

    Closure: e¦ is closed

    work page

  73. [83]

    Rightmost: e¦ = (e ¦ e/v.alt)for some environment e and some /v.alt-environment e/v.alt. Proof. By induction on the length of the evaluation se- quence leading to e¦. The base cases hold by the definition of reachability and by the definition of ι(·). As for the inductive cases, we proceed by cases on the transition rules:

    work page

  74. [84]

    The rules in { i/f_t, iff, ife, @e, sea} do not increase the number of explicit substitutions occuring in e¦ out- side of abstractions, hence the claim follows from the i.h

    For β/v.altthe claim follows from the side condition. The rules in { i/f_t, iff, ife, @e, sea} do not increase the number of explicit substitutions occuring in e¦ out- side of abstractions, hence the claim follows from the i.h.. The rules in { subvar , subl , subif } copy a practical value from the environment e/v.alt: note that e/v.alt(x)is ei- ther an ab...

    work page

  75. [85]

    Similar to the discussion in Lemma 5.5

    work page

  76. [86]

    As for the sea rule, by Lemma D.20 it suffices to prove that (b, e/v.alt)is a /v.alt-crumble, knowing that the other transition rules cannot be applied

    The rules in { β/v.alt, i/f_t, iff, ife, @e, subvar , subl , subif } do not change the evaluated part, hence the claim follows from the i.h.. As for the sea rule, by Lemma D.20 it suffices to prove that (b, e/v.alt)is a /v.alt-crumble, knowing that the other transition rules cannot be applied. This follows from the side condition of the sea rule: the crumble...

    work page 2017

  77. [87]

    Initialisation: (ι(c))⇓ = c for every crumble c

    work page

  78. [88]

    Principal projection: if e¦ → a e ′ ¦ then (e¦)⇓ → a (e ′ ¦)⇓ for any rule a /nequal sea

    work page

  79. [89]

    Overhead transparency: if e¦ → sea e ′ ¦ then (e¦)⇓ = (e ′ ¦)⇓

    work page

  80. [90]

    Determinism: the transition function → pCr is deter- ministic

    work page

Showing first 80 references.