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.
翻译:兰道尔嵌入能够为非可逆编程语言实现计算的可逆性,通过为每个中间状态附加足够的数据来重建前一状态。因此,一个有趣的研究问题是如何降低所需的空间开销。本文提出了面向Plotkin按值调用演算(CbV)的兰道尔嵌入。为控制CbV的计算复杂度并将β-规约步数转化为成本模型,CbV通常通过规约机实现。我们发现,一种尚未受到广泛关注的规约机展现出特别紧凑的兰道尔嵌入特性,其每一步仅需恒定的空间开销。