Title: New Notions of Reduction and Non-Semantic Proofs of Beta-Strong
Normalization in Typed Lambda-Calculi
Author: A. J. Kfoury and J. B. Wells
Date: December 19, 1994
Abstract:
Two new notions of reduction for terms of the lambda-calculus are
introduced and the question of whether a lambda-term is beta-strongly
normalizing is reduced to the question of whether a lambda-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 lambda-calculi.
Instead of the usual semantic proof style based on Girard's ``candidats de
r\'eductibilit\'e'', 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
lambda-calculus and the system of intersection types.