一句话：给出了带 ρ 和 θ 规则的 λμ-演算归约序列长度的上界，表明新增项与规则不增加计算复杂度。
自 Curry-Howard 同构可扩展到经典逻辑以来，λμ-演算成为经典逻辑证明编码的重要候选。本文在 Xi 关于 λ-演算归约序列长度上界的结果基础上，研究加入 ρ-规则和 θ-规则的 λμρθ-演算，并给出其归约序列长度的上界。分析表明，尽管 μ-规则使 μ-抽象能够消耗任意多个参数，新增的项和规则并不会提高该演算的计算复杂度。工作为经典 λ-演算的归约复杂性提供了理论界。
Since it was realized that the Curry-Howard isomorphism can be extended to the case of classical logic as well, several calculi have appeared as candidates for the encodings of proofs in classical logic. One of the most extensively studied among them is the $\lambda\mu$-calculus of Parigot. In this paper, based on the result of Xi presented for the $\lambda$-calculus Xi, we give an upper bound for the lengths of the reduction sequences in the $\lambda\mu$-calculus extended with the $\rho$- and $\theta$-rules. Surprisingly, our results show that the new terms and the new rules do not add to the computational complexity of the calculus despite the fact that $\mu$-abstraction is able to consume an unbounded number of arguments by virtue of the $\mu$-rule.
@article{paperbot398,
title = {An estimation for the lengths of reduction sequences of the $\lambda\mu\rho\theta$-calculus},
author = {Péter Battyányi and Karim Nour},
journal = {Logical Methods in Computer Science},
volume = {Volume 14, Issue 2},
year = {2018},
doi = {10.23638/lmcs-14(2:17)2018}
}