Confluence proofs of lambda-mu-calculi by Z theorem
Confluence proofs of lambda-mu-calculi by Z theorem
复制标题
Z 定理的 lambda-mu 演算的汇合证明
DOI：
10.1007/s11225-020-09931-0
复制
发表时间：
2021
期刊：
影响因子：
0.7
通讯作者：
K. Fujita
中科院分区：
文献类型：
--
作者：
Y. Honda;K. Nakawaza;K. Fujita
本文应用Dehornoy et al.的Z定理及其变形，称为合成Z定理，证明了Parigot演算在化简规则下的收敛性。首先证明了Baba et al.'本文给出了一种简化规则，即在重命名规则下，-演算的按名调用和按值调用变体的改进的完全展开式满足Z性质。利用Z定理给出了它们的新的合流性证明。其次，证明了复合Z定理可以用于证明具有简化规则、重命名规则和-规则的按名调用演算和按值调用演算的合流性，而对于这些变体，通过一次定义映射很难应用普通的并行约简技术或原始Z定理.
This paper applies Dehornoy et al.’s Z theorem and its variant, called the compositional Z theorem, to prove confluence of Parigot’s-calculi extended by the simplification rules. First, it is proved that Baba et al.’s modified complete developments for the call-by-name and the call-by-value variants of the-calculus with the renaming rule, which is one of the simplification rules, satisfy the Z property. It gives new confluence proofs for them by the Z theorem. Secondly, it is shown that the compositional Z theorem can be applied to prove confluence of the call-by-name and the call-by-value-calculi with both simplification rules, the renaming and the-rules, whereas it is hard to apply the ordinary parallel reduction technique or the original Z theorem by one-pass definition of mappings for these variants.