Short Proofs of Normalization

for the simply-typed lambda-calculus, permutative conversions and Gödel's T

by Felix Joachimski and Ralph Matthes

appeared in the Archive for Mathematical Logic 42, 59-87 (2003)


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 ā 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 Gödel's T.
Second revision (23 pages, April 2002) available as With respect to the revised version (see below), there is no change in the mathematical content.

Erratum to the published version and hence also to this version and the 1999 version: PDF (2 pages, November 2004). Every statement is correct but two lemmas concerning permutative conversions need a change in the organization of their proofs.

Slides for a talk on the parts without permutative conversions on May 30, 2002 are available here.


Revised version (22 pages, November 1999) available as For comparison we also provide an older version from October 1998 (24 pages).

Those who know the 1998 version might want to read the following:

Short Proofs of Normalization for the simply-typed
lambda-calculus, permutative conversions and Gödel's T

by Ralph Matthes and Felix Joachimski
Version as of Nov 11, 1999

The major changes relative to the 1998 version:

A new section (6) with a new lambda calculus with
generalized application: Strong normalization is our new
result (solving a problem raised by Jan von Plato). Even
Kappa (=immediate simplification) included. Shows our
ability to efficiently handle permutative conversions which
we see as a major achievement of the paper.

Treatment of Eta clearer for -> and new for + (not covered
by de Groote)

Treatment of T much smoother: We only have to prove more
closure properties of SN (via value expansion).

Further Comments: 
The normalization algorithms are not seen as the outcome
of the respective sections but as some summary which comes
for free.

The SN method may be seen as a way of reducing the cut rank
to zero in one pass. Hence, it is not designed with the aim
to conduct fine-grained analysis of reduction lengths.

The issue of formalizability in theorem proving systems on
computers is important, and the proofs are indeed
well-suited for that purpose as shown by Tobias Nipkow for
the Isabelle system.

We also could have included a forward (w.r.t. our original
submission date) reference to Goguen's TLCA 99 paper which
shows how to extend our method to dependent types (i. e., to
Martin-Löf's Logical Framework).

Ralph Matthes
Last modified: Mon Nov 29 19:55:05 CET 2004