一句话：通过两条交换规则扩展 Plotkin 传值 λ-演算，证明其是保守精细化并建立弱标准化定理。
论文研究 Plotkin 传值 λ-演算的一个扩展：加入两条交换规则（σ-归约），以消除该演算中有害的传值范式，从而获得许多语义性质的优雅刻画。作者证明该扩展演算是 Plotkin 演算的保守精细化，特别地，可解性（solvability）与潜在可求值性（potential valuability）在这两个演算中一致。证明基于一个标准化定理，该定理把 Takahashi 的并行归约方法推广到新的归约规则集合。由于归约之间存在重叠干扰，所得标准化是弱的，即重式（redex）并未被完全序列化。
We study an extension of Plotkin's call-by-value lambda-calculus via two commutation rules (sigma-reductions). These commutation rules are sufficient to remove harmful call-by-value normal forms from the calculus, so that it enjoys elegant characterizations of many semantic properties. We prove that this extended calculus is a conservative refinement of Plotkin's one. In particular, the notions of solvability and potential valuability for this calculus coincide with those for Plotkin's call-by-value lambda-calculus. The proof rests on a standardization theorem proved by generalizing Takahashi's approach of parallel reductions to our set of reduction rules. The standardization is weak (i.e. redexes are not fully sequentialized) because of overlapping interferences between reductions.Comment: 27 pages
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{GuerrieriPR16,
title = {Standardization and Conservativity of a Refined Call-by-Value lambda-Calculus},
author = {Giulio Guerrieri and Luca Paolini and Simona Ronchi Della Rocca},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 4},
year = {2017},
doi = {10.23638/lmcs-13(4:29)2017}
}