对称$λμ$ -演算强正规化结果的算术证明
Arithmetical proofs of strong normalization results for the symmetric $λμ$-calculus
摘要：
对称$λμ$ -演算是Parigot引入的$λμ$ -演算，其中增加了约简规则$\m'$，它是$μ$的对称。我们给出了该演算的一些强规范化结果的算术证明。我们表明（这是一个新的结果），$μμ'$ -减少是强正规化的无类型演算。我们还显示了强规范化的$βμμ'$减少类型演算：这是已知的，但以前的证明使用候选人的reductionary类型的解释被定义为固定点的一些增算子，因此，是高度非算术。
英文摘要：
The symmetric $λμ$-calculus is the $λμ$-calculus introduced by Parigot in which the reduction rule $\m'$, which is the symmetric of $μ$, is added. We give arithmetical proofs of some strong normalization results for this calculus. We show (this is a new result) that the $μμ'$-reduction is strongly normalizing for the un-typed calculus. We also show the strong normalization of the $βμμ'$-reduction for the typed calculus: this was already known but the previous proofs use candidates of reducibility where the interpretation of a type was defined as the fix point of some increasing operator and thus, were highly non arithmetical.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
