Strong normalization of λμμ-calculus with explicit substitutions
Strong normalization of λμμ-calculus with explicit substitutions
复制标题
具有显式替换的 λμμ 演算的强归一化
DOI：
--
复制
发表时间：
2004
期刊：
影响因子：
--
通讯作者：
Emmanuel Polonovski
中科院分区：
文献类型：
--
作者：
Emmanuel Polonovski
由Curien和Herbelin [7]定义的λμμ-演算是λμ-演算的一个变体，它表现出诸如项/上下文和按名称/按值调用的对称性。由于它是一个对称的，因此是一个非确定性的演算，通常的规范化证明技术需要进行一些调整才能在这种设置下工作。在这里，我们证明了带有显式替换的简单类型λμμ-演算的强正规化（SN）。为此，我们首先证明了简单类型λμμ-演算的SN（通过Barbanera和Berardi [2]的归约技术的变体），然后我们通过PSN（强规范化保持）形式化SN的证明技术，并且我们通过Bonelli [5]形式化的永久性技术证明了PSN。
The λμμ-calculus, defined by Curien and Herbelin [7], is a variant of the λμ-calculus that exhibits symmetries such as term/context and call-by-name/call-by-value. Since it is a symmetric, and hence a non-deterministic calculus, usual proof techniques of normalization needs some adjustments to be made to work in this setting. Here we prove the strong normalization (SN) of simply typed λμμ-calculus with explicit substitutions. For that purpose, we first prove SN of simply typed λμμ-calculus (by a variant of the reducibility technique from Barbanera and Berardi [2]), then we formalize a proof technique of SN via PSN (preservation of strong normalization), and we prove PSN by the perpetuality technique, as formalized by Bonelli [5].