一句话：提出寻址机及其基于最左归约的操作语义，并将地址集构造成组合代数，从而为完整无类型 λ-演算提供模型。
本文指出，图灵机与寄存器机虽长期作为计算抽象模型，但其与 λ-演算的等价更多依赖 Church-Turing 论题，而非对 λ-项的实际编码，因为这些机器并不适合直接建模函数式替换计算。作者提出一类“寻址机”（addressing machine），其操作仅涉及内存地址：将地址载入寄存器、通过地址把一台机器应用于另一台、以及调用另一台机器的地址。论文为寻址机给出基于最左归约的操作语义，并研究其行为。其地址集合可自然构成一个组合代数；为获得完整无类型 λ-演算的模型，作者进一步引入一条与组合逻辑中 ω-规则及 ζ_β 规则相似的规则。
Turing machines and register machines have been used for decades in theoretical computer science as abstract models of computation. Also the $\lambda$-calculus has played a central role in this domain as it allows to focus on the notion of functional computation, based on the substitution mechanism, while abstracting away from implementation details. The present article starts from the observation that the equivalence between these formalisms is based on the Church-Turing Thesis rather than an actual encoding of $\lambda$-terms into Turing (or register) machines. The reason is that these machines are not well-suited for modelling $\lambda$-calculus programs. We study a class of abstract machines that we call "addressing machine" since they are only able to manipulate memory addresses of other machines. The operations performed by these machines are very elementary: load an address in a register, apply a machine to another one via their addresses, and call the address of another machine. We endow addressing machines with an operational semantics based on leftmost reduction and study their behaviour. The set of addresses of these machines can be easily turned into a combinatory algebra. In order to obtain a model of the full untyped $\lambda$-calculus, we need to introduce a rule that bares similarities with the $\omega$-rule and the rule $\zeta_\beta$ from combinatory logic.
@article{paperbot1680,
title = {Addressing Machines as models of lambda-calculus},
author = {Giuseppe Della Penna and Benedetto Intrigila and Giulio Manzonetto},
journal = {Logical Methods in Computer Science},
volume = {Volume 18, Issue 3},
year = {2022},
doi = {10.46298/lmcs-18(3:10)2022}
}