New notions of reduction and non-semantic proofs of strong β-normalization in typed λ-calculi

Two notions of reduction for terms of the λ-calculus are introduced and the question of whether a λ-term is β-strongly normalizing is reduced to the question of whether a λ-term is merely normalizing under one of the notions of reduction. This gives a method to prove strong β-normalization for typed λ-calculi. Instead of the usual semantic proof style based on Tait´s realizability or Girard´s “candidats de reductibilite”, termination can be proved using a decreasing metric over a well-founded ordering. This proof method is applied to the simply-typed λ-calculus and the system of intersection types, giving the first non-semantic proof for a polymorphic extension of the λ-calculus