一句话：以算术方法证明 λ-Sym-Prop 强归一化，并用 zoom-in redex 序列给出其与 λ̄μμ̃* 的翻译。
本文研究经典命题逻辑自然演绎风格下 λ-Sym-Prop 演算的强归一化，以及它与 Curien 和 Herbelin 的 λ̄μμ̃ 演算的蕴含部分扩展否定后所得 λ̄μμ̃* 演算之间的联系。作者首先给出 λ-Sym-Prop 强归一化的算术证明，再构造两种演算之间的翻译。证明方法改编自 David 和 Nour 的强归一化技术，核心创新是引入 redex 的 zoom-in 序列概念，该概念可引导至主定理的直接证明。结果从证明论角度统一了两类经典 λ 演算的强归一化论证，并为公式即类型解释提供归约性质支持。
In this paper we give an arithmetical proof of the strong normalization of lambda-Sym-Prop of Berardi and Barbanera [1], which can be considered as a formulae-as-types translation of classical propositional logic in natural deduction style. Then we give a translation between the lambda-Sym-Prop-calculus and the lambda-bar-mu-mu-tilde-star-calculus, which is the implicational part of the lambda-bar-mu-mu-tilde-calculus invented by Curien and Herbelin [3] extended with negation. In this paper we adapt the method of David and Nour [4] for proving strong normalization. The novelty in our proof is the notion of zoom-in sequences of redexes, which leads us directly to the proof of the main theorem.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{BattyanyiN17,
title = {Strong normalization of lambda-Sym-Prop- and lambda-bar-mu-mu-tilde-star- calculi},
author = {Peter Battyanyi and Karim Nour},
journal = {Logical Methods in Computer Science},
volume = {Volume 13, Issue 3},
year = {2017},
doi = {10.23638/lmcs-13(3:34)2017}
}