关于类型上递归方程的$λ$ -演算强正规化的一个算术证明
An arithmetical proof of the strong normalization for the $λ$-calculus with recursive equations on types
摘要：
我们给出了强规范化的$λ$ -演算（也是$λμ$ -演算）的算术证明，其中类型系统是一个简单的类型与递归方程的类型。使用约简的候选证明是一个简单的扩展，没有方程，但这种证明不能在皮亚诺算术形式化。这种证明所需的系统的强度尚不清楚。我们的证明表明，它不超过皮亚诺算术。
英文摘要：
We give an arithmetical proof of the strong normalization of the $λ$-calculus (and also of the $λμ$-calculus) where the type system is the one of simple types with recursive equations on types. The proof using candidates of reducibility is an easy extension of the one without equations but this proof cannot be formalized in Peano arithmetic. The strength of the system needed for such a proof was not known. Our proof shows that it is not more than Peano arithmetic.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
