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

TL;DR

This paper introduces a reversible abstract machine for Plotkin's call-by-value calculus, achieving minimal space overhead in Landauer's embedding, which enhances the understanding of reversible computation models.

Contribution

It presents a novel reversible machine with a compact Landauer's embedding for CbV, reducing space overhead compared to previous models.

Findings

The machine requires only constant space overhead per step.

It provides a reversible implementation of Plotkin's call-by-value calculus.

The approach improves the efficiency of reversible computation models.

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.