A Reversible Crumbling Abstract Machine for Plotkin's Call-by-Value
For researchers in reversible computing and programming language theory, this provides a compact reversible implementation of a fundamental calculus, though the problem is niche.
This work proposes a Landauer embedding for Plotkin's call-by-value calculus that achieves constant space overhead per reduction step, addressing the challenge of reducing space overhead in reversible computation.
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 $β$-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.