λ演算标准化定理的构造类型论形式化
Formalization in Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using Multiple Substitution
摘要：
我们提出了一个完整的形式化的标准化定理的Martin-Löf的构造类型论的λ演算使用一阶语法与一种名称的自由和绑定变量和斯托顿的多重替代。我们的形式化是基于Ryo Kashima的证明，其中具有标准序列的beta-约简的概念被归纳关系捕获。证明只使用结构归纳法的语法和定义的关系，这是可能的，由于我们采用的特定公式的替代。整个开发过程使用Agda系统进行了机器检查。
英文摘要：
We present a full formalization in Martin-Löf's Constructive Type Theory of the Standardization Theorem for the Lambda Calculus using first-order syntax with one sort of names for both free and bound variables and Stoughton's multiple substitution. Our formalization is based on a proof by Ryo Kashima, in which a notion of beta-reducibility with a standard sequence is captured by an inductive relation. The proof uses only structural induction over the syntax and the relations defined, which is possible due to the specific formulation of substitution that we employ. The whole development has been machine-checked using the system Agda.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
