按名传递只是带有界限控制的按值传递
摘要：$ Lambda\_\$ $: 一种通过值调用的lambda演算，扩展了shift0和控制分隔符$ \$ $，具有精心设计的规约理论，可以将具有beta和eta缩减的lambda演算通过一个继续传递风格翻译的右逆同构地嵌入到$ Lambda\_\$ $中。虽然lambda演算的按名缩减可以轻松模拟按值版本，但我们表明，添加shift0和$ \$ $是表达能力的黄金平衡，足以模拟beta和eta缩减，并仍然允许一个模拟回卷。作为一个推论，计算$ Lambdamu\_v $、$ lambda\_\$ $、$ Lambda\_\$ $和$ lambda $ 相应地。
作者：Mateusz Pyzik
论文ID：2212.08594
分类：Programming Languages
分类简称：cs.PL
提交时间：2023-06-22