一句话：证明改进的全规约 Krivine 抽象机 KN 以锁步方式模拟纯 λ 演算的标准正常序规约。
论文研究全规约 Krivine 抽象机 KN 的规约策略正确性。作者在 Biernacka–Danvy 环境机框架下，让改进的 KN 作用于可含开放项的闭包，并构造对应的闭包演算结构操作语义，其规约关系本身即为一种策略。论文在该演算中证明此策略与纯 λ 演算的标准正常序（最左规约到范式）逐步模拟，再经替换函数把闭包映射回纯项，从而推出 KN 也逐步模拟正常序。该结果强于 KN 的完备性，因为纯 λ 演算存在完备但非标准策略。证明依赖索引对齐、参数即层次与平衡推导三条性质，使结构归纳直接，避免动态 α 转换和变量遍历。
Abstract We exploit the idea of proving properties of an abstract machine by using a corresponding semantic artefact better suited to their proof. The abstract machine is an improved version of Pierre Crégut’s full-reducing Krivine machine KN. The original version works with closed terms of the pure lambda calculus with de Bruijn indices. The improved version reduces in similar fashion but works on closures where terms may be open. The corresponding semantic artefact is a structural operational semantics of a calculus of closures whose reduction relation is purposely a reduction strategy. As shown in previous work, improved KN and the structural operational semantics ‘correspond’, i.e. both artefacts realise the same reduction strategy. In this paper, we prove in the calculus of closures that the reduction strategy simulates in lockstep (at every reduction step) the complete and standard normal-order strategy (i.e. leftmost reduction to normal form) of the pure lambda calculus. The simulation is witnessed by a substitution function from closures of the closure calculus to pure terms of the pure lambda calculus. Thus, KN also simulates normal-order in lockstep by the correspondence. This result is stronger than the known proof that KN is complete, for in the pure lambda calculus there are complete but non-standard strategies. The lockstep simulation proof consists of straightforward structural inductions, thanks to three properties of the closure calculus we call ‘index alignment’, ‘parameters-as-levels’ and ‘balanced derivations’. The first two come from KN. Thanks to these properties, a proof in a calculus of closures involving de Bruijn indices and de Bruijn levels is unproblematic. There is no lexical adjustment at binding lookup, on-the-fly alpha-conversion or recursive traversals of the term to deal with bound and free variables as in other calculi. This paper contributes to the framework for environment machines of Biernacka and Danvy a full-reducing open-terms closure calculus, its corresponding abstract machine, and a lockstep simulation proof via a substitution function.
@article{paperbot727,
title = {The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: A proof via corresponding calculus},
author = {ÁLVARO GARCÍA-PÉREZ and PABLO NOGUEIRA},
journal = {Journal of Functional Programming},
volume = {29},
year = {2019},
doi = {10.1017/s0956796819000017}
}