Saved in:
Bibliographic Details
Main Authors: Pizzo, Nicolò, Coen, Claudio Sacerdoti
Format: Preprint
Published: 2026
Subjects:
Online Access:https://arxiv.org/abs/2605.09179
Tags: Add Tag
No Tags, Be the first to tag this record!
Table of Contents:
  • 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.