arxiv: 2605.09179 · v1 · submitted 2026-05-09 · 💻 cs.LO

Recognition: no theorem link

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

Claudio Sacerdoti Coen, Nicol\`o Pizzo

Pith reviewed 2026-05-12 02:29 UTC · model grok-4.3

classification 💻 cs.LO

keywords Landauer's embeddingreversible computationcall-by-value lambda calculusabstract machinecrumbling machinebeta reduction

0 comments

The pith

The crumbling abstract machine for Plotkin's call-by-value calculus supports a reversible embedding with only constant space added per reduction step.

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

The paper shows that one particular abstract machine for implementing Plotkin's call-by-value lambda calculus can be augmented with a Landauer's embedding that stores only a constant amount of extra data at each beta-step to enable full reversal. This matters because most reversible embeddings for functional languages incur growing space costs that make them impractical for long computations, while a constant overhead keeps the space cost proportional to the number of steps. A sympathetic reader would see this as a way to turn beta-steps into a usable cost model even when the computation must run both forward and backward.

Core claim

The crumbling abstract machine, which has received little attention, admits a Landauer's embedding for Plotkin's call-by-value calculus that requires only constant space overhead for each step, while correctly implementing the reduction and preserving the ability to reconstruct prior states.

What carries the argument

The crumbling abstract machine, which decomposes terms so that each reduction step logs a fixed-size record sufficient for reversal.

If this is right

Beta-steps remain a faithful cost model once the computation is made reversible.
Reversible call-by-value programs can be obtained without space overhead that grows with computation length.
The embedding gives a concrete way to study space usage in reversible functional computation.

Where Pith is reading between the lines

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

The same machine structure might yield compact embeddings for related strategies such as call-by-need.
Constant overhead opens the possibility of embedding this reversibility into resource-bounded models of computation.
Extending the approach to typed calculi or adding features like control operators could be tested by measuring the space record size on sample terms.

Load-bearing premise

The crumbling abstract machine correctly implements Plotkin's call-by-value reduction while allowing prior states to be recovered using only a fixed amount of additional space per step.

What would settle it

A concrete call-by-value reduction sequence in which either the machine produces an incorrect result or the extra data needed for reversal grows beyond a constant size at some step.

Figures

Figures reproduced from arXiv: 2605.09179 by Claudio Sacerdoti Coen, Nicol\`o Pizzo.

**Figure 1.** Figure 1: Plotkin’s Closed CbV calculus Contributions. The contributions of this work consist in presenting an economic Landauer’s embedding for Plotkin’s closed CbV by means of a Landauer’s embedding for a new reduction machine for the finest crumbling, that we call Reversible Crumbling Abstract Machine (RCAM). In addition to showing the reversibility of the machine, we establish the usual properties of crumbling … view at source ↗

**Figure 2.** Figure 2: Finest crumbled calculus 2.2 The finest crumbled calculus The idea behind crumbling consists in avoiding the nesting of applications, so that we can write terms such as (tu)s and t(us) as (xs) [x←tu] and (tx) [x←us] by using explicit substitutions: this is the most common way for representing the crumbling, and represents the most idiomatic way for representing environment entries. Many forms of crumbling … view at source ↗

**Figure 3.** Figure 3: Translation from λP rot-terms to crumbled forms and back 2.3 The finest crumbling translation and its inverse Let Λ and Λ denote respectively the set of all λP lot-terms and the set of all finest crumbled forms. We define the crumbling translation · : Λ → Λ in order to translate a term from the λP lot calculus to its crumbled representation. Together with this translation function we define the read-back f… view at source ↗

**Figure 4.** Figure 4: Measures for terms, bites and environments; bound and free variables, domains Example [∗←z1z2] [z1←λx. [∗←xz3] [z3←xx]] [z2←λy. [∗←y]] →m1 [∗←z2z4] [z4←z2z2] [z1←λx. [∗←xz3] [z3←xx]] [z2←λy. [∗←y]] →m2 [∗←z2z4] [z4←λy. [∗←y]] [z1←λx. [∗←xz3] [z3←xx]] [z2←λy. [∗←y]] →m2 [∗←λy. [∗←y]] [z4←λy. [∗←y]] [z1←λx. [∗←xz3] [z3←xx]] [z2←λy. [∗←y]] [PITH_FULL_IMAGE:figures/full_fig_p007_4.png] view at source ↗

**Figure 5.** Figure 5: Example of evaluation of the crumbling of the term (λx.x(xx))λy.y 1. Freshness: t is well-named. 2. Closure: t is closed. 3. Bodies: each body in t is the translation of a term. 4. Size: the size |t| is linear with respect to the size of the initial term t. 5. Contextual decoding: if t = E1 [z←xy] E2 then (E1 [z←⟨·⟩])↓ is a right vcontext. 2.4 Evaluating crumbles The reduction rules for the finest crumble… view at source ↗

**Figure 6.** Figure 6: Reversible Crumbling Abstract Machine The transitions. It is easy to see that the forward transitions ⇝m1 , ⇝m2 are exactly the →m1 , →m2 transitions of the finest crumbling calculus once read-back is applied and that the ⇝sea is the identity up to read-back. In subsection 3.2 we will deeply discuss the reversibility of each transition. Definition 6 (Reachable State). A state is reachable if it is obtained… view at source ↗

**Figure 7.** Figure 7: An example of output A An implementation in OCaml of the RCAM We provide at https://github.com/sacerdot/RCAM a reference implementation in OCaml of the RCAM, meant to guarantee the soundness of the assumptions that underly the complexity analyses. The implementation also allows the reader to run the machine on examples of her choice, to better understand how the machine computes. The implementation takes a… view at source ↗

read the original abstract

Landauer's embeddings enable the reversibility of computations for non-reversible programming languages, augmenting each intermediate state with enough data to reconstruct the previous state. An interesting research question is therefore to try to reduce the space overhead required. In this work we propose a Landauer's embedding for Plotkin's call-by-value calculus (CbV). In order to control the computational complexity of CbV and turn the number of $\beta$-steps into a cost model, CbV is typically implemented via reduction machines. We show that one machine, that has not received much attention, exhibits a particularly compact Landauer's embedding, requiring only constant space overhead for each step.

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.

Desk Editor's Note private letter to a colleague

The crumbling abstract machine gives CbV a Landauer's embedding with only constant extra space per beta step.

read the letter

The paper's main point is that one under-used crumbling abstract machine for Plotkin's call-by-value lambda calculus supports a reversible embedding that adds only constant space per reduction step. That is the concrete claim the authors are making, and it lines up with the title and abstract. They start from the usual motivation: Landauer's embeddings add history to make irreversible steps reversible, but most embeddings cost too much space, so they look for a machine that keeps the added data small while still giving a usable cost model for beta reduction. The crumbling machine turns out to be the one that works cleanly for this purpose. That specific pairing looks new; prior reversible lambda work has used other machines or accepted higher overhead. The construction itself is the contribution, and it is presented directly without extra claims about performance or applications. The paper does a reasonable job of situating the machine in the existing literature on CbV abstract machines and reversible computation. It keeps the focus on the space bound, which is the part that matters for the cost model. If the transitions are defined so that every forward step records exactly the information needed to undo it, and nothing more, then the constant overhead follows. The stress-test found no obvious mismatch between the machine and CbV reduction or hidden growth in the history, which is good. The main soft spot is that the abstract is very short on the actual machine rules and the proof that the embedding preserves the reduction relation. The full paper must supply those definitions and show that the stored data really stays bounded by a constant independent of term size or reduction length. Without that, the central claim is still plausible but not yet verified from the given text. Readers already working on reversible functional languages or cost models for lambda calculi will find this useful. It is a narrow, technical result rather than a broad framework, so it is best for people who already know abstract machines and Landauer's embeddings. The work is coherent on its own terms and shows clear engagement with the relevant definitions, so it deserves a serious referee who can check the machine correctness and the space analysis. I would send it to peer review.

Referee Report

0 major / 3 minor

Summary. The paper introduces a Landauer's embedding for Plotkin's call-by-value lambda calculus realized via the crumbling abstract machine. It claims that this machine admits a reversible embedding in which each beta-step requires only constant additional space to record history, while correctly implementing CbV reduction and allowing prior states to be reconstructed.

Significance. If the central construction and its space bound hold, the result is significant for reversible computing: it isolates a CbV machine whose history overhead is asymptotically better than typical stack-based or environment-based machines, directly supporting the use of beta-steps as a cost model in a reversible setting. The work also supplies a concrete, implementable bridge between abstract machines and Landauer's principle.

minor comments (3)

The abstract and introduction would benefit from an explicit statement of the machine's transition rules (perhaps in §3) and a one-paragraph proof sketch of the constant-space claim before the detailed development.
Notation for the history component of the embedding should be introduced once and used uniformly; currently the distinction between the forward machine state and the reversible pair is occasionally ambiguous in the early sections.
A small table comparing the space overhead of the crumbling machine with at least one other standard CbV machine (e.g., the CEK machine) would make the compactness claim easier to appreciate.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary, the recognition of the significance of a constant-space Landauer's embedding for CbV, and the recommendation of minor revision. We are pleased that the central construction is viewed as a useful bridge between abstract machines and reversible computing.

Circularity Check

0 steps flagged

No circularity: derivation is a direct technical construction

full rationale

The paper defines the crumbling abstract machine for Plotkin's CbV, augments it with a Landauer's embedding, and proves correctness plus constant space overhead per step from the machine transitions themselves. No equations reduce to their own inputs by construction, no parameters are fitted then renamed as predictions, and no load-bearing claims rest on self-citations whose content is unverified or circular. The central result is an explicit reversible machine whose space bound follows from the embedding definition and transition rules, making the derivation self-contained against external benchmarks of CbV machines and reversibility.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The claim rests on the standard definition of Plotkin's call-by-value reduction and the general properties of Landauer's embeddings; no new free parameters or invented entities are introduced in the abstract.

axioms (2)

domain assumption Plotkin's call-by-value beta-reduction rules define the computation steps whose reversibility is sought.
Invoked implicitly when the abstract refers to turning the number of beta-steps into a cost model.
standard math Landauer's embedding augments states with sufficient history to allow reversal.
Stated directly in the opening sentence as the general technique being specialized.

pith-pipeline@v0.9.0 · 5405 in / 1163 out tokens · 31146 ms · 2026-05-12T02:29:19.858889+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

38 extracted references · 38 canonical work pages

[1]

https://ocaml.org/manual/5.4/debugger.html, accessed on 27.02.2026

ocamldebug. https://ocaml.org/manual/5.4/debugger.html, accessed on 27.02.2026

work page 2026
[2]

Logical Methods in Computer ScienceV olume 19, Issue 4(Dec 2023)

Accattoli, B.: Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. Logical Methods in Computer ScienceV olume 19, Issue 4(Dec 2023). https://doi.org/10.46298/lmcs-19(4:23)2023

work page doi:10.46298/lmcs-19(4:23)2023 2023
[3]

In: Proceedings of the 19th International Symposium on Principles and Prac- tice of Declarative Programming

Accattoli, B., Barras, B.: Environments and the complexity of abstract machines. In: Proceedings of the 19th International Symposium on Principles and Prac- tice of Declarative Programming. pp. 4–16. PPDP ’17, Association for Comput- ing Machinery, New York, NY, USA (Oct 2017). https://doi.org/10.1145/3131851. 3131855

work page doi:10.1145/3131851 2017
[4]

https://doi.org/10.48550/arXiv.2506.14131

Accattoli, B., Coen, C.S., Wu, J.H.: Positive Sharing and Abstract Machines (Sep 2025). https://doi.org/10.48550/arXiv.2506.14131

work page doi:10.48550/arxiv.2506.14131 2025
[5]

https://doi.org/10.48550/arXiv.1907.06057

Accattoli, B., Condoluci, A., Guerrieri, G., Coen, C.S.: Crumbling Abstract Ma- chines (Jul 2019). https://doi.org/10.48550/arXiv.1907.06057

work page doi:10.48550/arxiv.1907.06057 2019
[6]

In: Proceed- ingsofthe22ndInternationalSymposiumon PrinciplesandPracticeofDeclarative Programming

Accattoli, B., Dal Lago, U., Vanoni, G.: The Machinery of Interaction. In: Proceed- ingsofthe22ndInternationalSymposiumon PrinciplesandPracticeofDeclarative Programming. pp. 1–15. PPDP ’20, Association for Computing Machinery, New York, NY, USA (Sep 2020). https://doi.org/10.1145/3414080.3414108

work page doi:10.1145/3414080.3414108 2020
[7]

In: Igarashi, A

Accattoli, B., Guerrieri, G.: Open Call-by-Value. In: Igarashi, A. (ed.) Program- ming Languages and Systems. pp. 206–226. Springer International Publishing, Cham (2016). https://doi.org/10.1007/978-3-319-47958-3_12

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

In: Dastani, M., Sirjani, M

Accattoli, B., Guerrieri, G.: Implementing Open Call-by-Value. In: Dastani, M., Sirjani, M. (eds.) Fundamentals of Software Engineering. pp. 1–19. Springer Inter- national Publishing, Cham (2017). https://doi.org/10.1007/978-3-319-68972-2_1

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

In: Ábrahám, E., Dubslaff, C., Tarifa, S.L.T

Accattoli, B., Guerrieri, G., Leberle, M.: Strong Call-by-Value and Multi Types. In: Ábrahám, E., Dubslaff, C., Tarifa, S.L.T. (eds.) Theoretical Aspects of Computing – ICTAC 2023. pp. 196–215. Springer Nature Switzerland, Cham (2023). https: //doi.org/10.1007/978-3-031-47963-2_13

work page doi:10.1007/978-3-031-47963-2_13 2023
[10]

In: Kohlenbach, U., Barceló, P., de Queiroz, R

Accattoli, B., Sacerdoti Coen, C.: On the Value of Variables. In: Kohlenbach, U., Barceló, P., de Queiroz, R. (eds.) Logic, Language, Information, and Com- putation. pp. 36–50. Springer, Berlin, Heidelberg (2014). https://doi.org/10.1007/ 978-3-662-44145-9_3

work page 2014
[11]

In: Gardner, P., Yoshida, N

Danos, V., Krivine, J.: Reversible Communicating Systems. In: Gardner, P., Yoshida, N. (eds.) CONCUR 2004 - Concurrency Theory. pp. 292–307. Springer, Berlin, Heidelberg (2004). https://doi.org/10.1007/978-3-540-28644-8_19

work page doi:10.1007/978-3-540-28644-8_19 2004
[12]

SIGPLAN Not.39(4), 502–514 (Apr 2004)

Flanagan, C., Sabry, A., Duba, B.F., Felleisen, M.: The essence of compiling with continuations. SIGPLAN Not.39(4), 502–514 (Apr 2004). https://doi.org/ 10.1145/989393.989443

work page doi:10.1145/989393.989443 2004
[13]

InterJournal Complex Systems46(1996)

Huelsbergen, L.: A logically reversible evaluator for the call-by-name lambda cal- culus. InterJournal Complex Systems46(1996)

work page 1996
[14]

Journal of Functional Programming7(5), 549–554 (Sep 1997)

Huet, G.: The Zipper. Journal of Functional Programming7(5), 549–554 (Sep 1997). https://doi.org/10.1017/S0956796897002864

work page doi:10.1017/s0956796897002864 1997
[15]

In: Koopman, P., Clack, C

Kluge, W.: A Reversible SE(M)CD Machine. In: Koopman, P., Clack, C. (eds.) Implementation of Functional Languages. pp. 95–113. Springer, Berlin, Heidelberg (2000). https://doi.org/10.1007/10722298_6

work page doi:10.1007/10722298_6 2000
[16]

(1961) Irreversibility and heat generation in the computing process.IBM Journal of Research and Development5(3) 183–191https://doi

Landauer, R.: Irreversibility and Heat Generation in the Computing Process. IBM Journal of Research and Development5(3), 183–191 (Jul 1961). https://doi.org/ 10.1147/rd.53.0183 18 Nicolò Pizzo and Claudio Sacerdoti Coen

work page doi:10.1147/rd.53.0183 1961
[17]

In: Goubault-Larrecq, J., König, B

Lanese, I., Phillips, I., Ulidowski, I.: An Axiomatic Approach to Reversible Com- putation. In: Goubault-Larrecq, J., König, B. (eds.) Foundations of Software Sci- ence and Computation Structures . pp. 442–461. Springer International Publishing, Cham (2020). https://doi.org/10.1007/978-3-030-45231-5_23

work page doi:10.1007/978-3-030-45231-5_23 2020
[18]

In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages

Mackie, I.: The geometry of interaction machine. In: Proceedings of the 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 198–208 (1995)

work page 1995
[19]

In: Klin, B., Pimentel, E

Miller, D., Wu, J.H.: A Positive Perspective on Term Representation. In: Klin, B., Pimentel, E. (eds.) 31st EACSL Annual Conference on Computer Science Logic ( CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs ), vol. 252, pp. 3:1–3:21. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, Dagstuhl, Germany (2023). https://doi.org/10.4230/L...

work page doi:10.4230/lipics.csl.2023.3 2023
[20]

Theoretical Com- puter Science1(2), 125–159 (Dec 1975)

Plotkin, G.D.: Call-by-name, call-by-value and theλ-calculus. Theoretical Com- puter Science1(2), 125–159 (Dec 1975). https://doi.org/10.1016/0304-3975(75) 90017-1

work page doi:10.1016/0304-3975(75 1975
[21]

read-backs to

Yokoyama, T., Axelsen, H.B., Glück, R.: Towards a Reversible Functional Lan- guage.In:DeVos,A.,Wille,R.(eds.)ReversibleComputation.pp.14–29.Springer, Berlin, Heidelberg (2012). https://doi.org/10.1007/978-3-642-29517-1_2 A Reversible Crumbling Abstract Machine for Plotkin’s Call-by-Value 19 Fig. 7.An example of output A An implementation in OCaml of the R...

work page doi:10.1007/978-3-642-29517-1_2 2012
[22]

all the variables indom(E ′′)are pairwise distinct: this holds because all variables put in the domain by crumbling are globally fresh 2.dom(E)∩bv(E) =∅: this also holds for the same reason

work page
[23]

–Case wherez∈dom([x←b]E): it holds because[x←b]Eis well-named by i.h

ifE ′′ =E 1 [z←b ′′]E 2 thenz̸∈fv(b ′′)∪fv(E 2): we proceed by cases on where zcan occur inE ′′ –Case wherez=∗andE 1 =ϵ: trivial since∗can only occur in the domain –Casewherez∈dom([y←b ′]E ′):itholdsbecause[y←b ′]E ′ iswell-named by i.h. –Case wherez∈dom([x←b]E): it holds because[x←b]Eis well-named by i.h. and because when computinguthe variables put in t...

work page
[24]

Freshness:t is well-named

work page
[25]

Bodies: each body intis the translation of a term

work page
[26]

Size: the size|t|is linear with respect to the size of the initial termt

work page
[27]

Contextual decoding: ift =E 1 [z←xy]E 2 then(E 1 [z←⟨·⟩]) ↓ is a right v- context. Proof

work page
[28]

See Lemma 22.⊓ ⊔ Definition 7 (σ-operator).The functionσ (·) turns a v-environment into the parallel substitution obtained by firing all explicit substitutions at once. It is defined by structural recursion as follows: σϵ =x7→x σ[x←v]E ′v = ( x7→v ↓ σE′v y7→y σ E′v Lemma 23 (Read-back to value).For anyEv that is both a crumble and a v-environment,E v ↓ is...

work page
[29]

Freshness:Eis well-named

work page
[30]

Bodies: each body occurring inEis a subterm (up to renaming and substi- tution of variable to variable) of the initial crumble

work page
[31]

Contextual decoding: ifE=E 1 [z←xy]E 2 then(E 1 [z←⟨·⟩]) ↓ is a right v- context. Proof

work page
[32]

See Lemma 26⊓ ⊔ B.3 Proofs for subsection 2.2 Lemma 35 (Initialization).For every closed termt,t ↓ =t. Proof.Inductively on the shape of t: –t:=xis not possible sincetis closed by hypothesis –t:=λx.y, then(λx.y) ↓ = [∗←λx.[∗←y]] ↓ =λx.y 34 Nicolò Pizzo and Claudio Sacerdoti Coen –t:=λx.u, then(λx.u) ↓ = [∗←λx.u ]↓ =λx.u ↓; by i.h.u ↓ =u, soλx.u ↓ = λx.u –...

work page
[33]

Initialization: See Lemma 35

work page
[34]

Principal Projection: See Lemma 36

work page
[35]

Determinism: See Lemma 37

work page
[36]

Halt: See Lemma 38.⊓ ⊔ 36 Nicolò Pizzo and Claudio Sacerdoti Coen C Proofs for section 3 C.1 Proofs for subsection 3.1 Lemma 6 (Invariants for the RCAM).LetSbe a reachable by forward-only transitions state of the RCAM:

work page
[37]

Freshness:Sis well-named

work page
[38]

Proof.Freshness and closure are inherited by the environments that compose the state

Rightmost:S= (E, E v,H)for some environmentE, v-environmentE v and history stackH. Proof.Freshness and closure are inherited by the environments that compose the state. For the rightmost invariant, we only move the pointer to the next entry of the environment with the⇝sea transition, i.e. we only move the pointer when the entry already contains a value.⊓ ...

work page