Short proofs of normalization for the simply- typed λ-calculus, permutative conversions and Gödel's T
Short proofs of normalization for the simply- typed λ-calculus, permutative conversions and Gödel's T
复制标题
简单类型 λ 演算、置换转换和哥德尔 T 归一化的简短证明
DOI：
10.1007/s00153-002-0156-9
复制
发表时间：
2003
影响因子：
0.3
通讯作者：
R. Matthes
中科院分区：
文献类型：
--
作者：
Felix Joachimski;R. Matthes
摘要。摘要研究了项集、强正则化项子集和范式的归纳刻画，给出了简单型λ微积分的弱正则化和强正则化，以及具有置换转换的和类型的扩展。由柏拉图提倡的自然演绎中受广义消去规则启发的新系统的类似处理，显示了该方法的灵活性，该方法不使用强可计算性/候选风格（如Tait和Girard）。还证明了用η规则对置换转换系统的扩展仍然是强正规化的，同样地，对广义应用系统的扩展也是用“直接简化”规则。通过引入无限分支归纳规则，该方法甚至扩展到Gödel的T。
Abstract. Inductive characterizations of the sets of terms, the subset of strongly normalizing terms and normal forms are studied in order to reprove weak and strong normalization for the simply-typed λ-calculus and for an extension by sum types with permutative conversions. The analogous treatment of a new system with generalized applications inspired by generalized elimination rules in natural deduction, advocated by von Plato, shows the flexibility of the approach which does not use the strong computability/candidate style à la Tait and Girard. It is also shown that the extension of the system with permutative conversions by η-rules is still strongly normalizing, and likewise for an extension of the system of generalized applications by a rule of ``immediate simplification''. By introducing an infinitely branching inductive rule the method even extends to Gödel's T.