New notions of reduction and non-semantic proofs of β-strong normalization in typed λ-calculi
1994-014-stron...pdf (14.62Mb) Main Report
Kfoury, A. J.
Wells, J. B.
MetadataShow full item record
CitationKfoury, A.J.; Wells, J.B.. "New Notions of Reduction and Non-Semantic Proofs of Beta-Strong Normalization in Typed Lambda-Calculi”, Technical Report BUCS-1994-014, Computer Science Department, Boston University, December 19, 1994. [Available from: http://hdl.handle.net/2144/1484]
Two new notions of reduction for terms of the λ-calculus are introduced and the question of whether a λ-term is beta-strongly normalizing is reduced to the question of whether a λ-term is merely normalizing under one of the new notions of reduction. This leads to a new way to prove beta-strong normalization for typed λ-calculi. Instead of the usual semantic proof style based on Girard's "candidats de réductibilité'', termination can be proved using a decreasing metric over a well-founded ordering in a style more common in the field of term rewriting. This new proof method is applied to the simply-typed λ-calculus and the system of intersection types.