Paper Info
Title
Short Proofs Of Normalization For The Simply-Typed Lambda-Calculus, Permutative Conversions And Godel'S 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 lambda-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 a la Tait and Girard. It is also shown that the extension of the system with permutative conversions by eta-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 Godel's T.
Year
DOI
Venue
2003
10.1007/s00153-002-0156-9
ARCHIVE FOR MATHEMATICAL LOGIC
Keywords
DocType
Volume
lambda-calculus, permutative/commuting conversions, sum types, generalized application, Godel's T-q, omega-rule, inductive characterization
Journal
42
Issue
ISSN
Citations 
1
0933-5846
28
PageRank 
References 
Authors
1.45
12
2
Name
Order
Citations
PageRank
Felix Joachimski1614.85
Ralph Matthes220121.67