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通常通过规约机实现。我们发现,一种尚未受到广泛关注的规约机展现出特别紧凑的兰道尔嵌入特性,其每一步仅需恒定的空间开销。

0
下载
关闭预览

相关内容

【新书】使用Python进行金融建模
专知会员服务
33+阅读 · 2024年9月28日
专知会员服务
92+阅读 · 2021年4月12日
一个牛逼的 Python 调试工具
机器学习算法与Python学习
15+阅读 · 2019年4月30日
换个角度看GAN:另一种损失函数
机器之心
16+阅读 · 2019年1月1日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
VIP会员
最新内容
综述 | 3D场景图:开放挑战与未来方向
专知会员服务
6+阅读 · 6月22日
21世纪的无人机战争
专知会员服务
4+阅读 · 6月22日
《量子技术的军事任务技术适配与利用》
专知会员服务
5+阅读 · 6月22日
美国从乌克兰无人机战争中学习经验
专知会员服务
7+阅读 · 6月21日
ICML 2026 | 面向视觉语言模型的语义鲁棒性认证
专知会员服务
5+阅读 · 6月21日
相关基金
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
1+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2015年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
国家自然科学基金
1+阅读 · 2014年12月31日
国家自然科学基金
0+阅读 · 2014年12月31日
Top
微信扫码咨询专知VIP会员