论文标题
PCF的扩展地址机，并具有明确的替换
Extended Addressing Machines for PCF, with Explicit Substitutions
论文作者
论文摘要
引入了解决机器作为形式主义，以构建纯净，未型Lambda-Calculus的模型。我们通过添加有关自然数的算术操作的说明来扩展其程序的语法，并引入反射原则，允许某些机器访问其自己的地址并执行递归呼叫。我们证明，由此产生的扩展地址机自然会模拟具有明确替换的弱呼叫PCF。最后，我们证明它们也非常适合代表常规的PCF程序（封闭式）计算自然数。
Addressing machines have been introduced as a formalism to construct models of the pure, untyped lambda-calculus. We extend the syntax of their programs by adding instructions for executing arithmetic operations on natural numbers, and introduce a reflection principle allowing certain machines to access their own address and perform recursive calls. We prove that the resulting extended addressing machines naturally model a weak call-by-name PCF with explicit substitutions. Finally, we show that they are also well-suited for representing regular PCF programs (closed terms) computing natural numbers.
