# 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