Short Proofs of Normalization

for the simply-typed λ-calculus, permutative conversions and Gödel’s T

Felix Joachimski^{1}, Ralph Matthes^{2} April 18, 2002

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 simplytyped λ-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 η-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.

Introduction

Normalization proofs for the simply-typed λ-calculus enjoy continuous interest [Gog95, vRS95, vRSSX99] in the literature although the main results of weak and strong normalization have been established quite early by Turing (around 1941, published in [Gan80]) and Sanchis [San67].

This article employs a proof method that allows to show strong normalization for all typed terms without recourse to inclusive predicates such as strong computability [Tai67] or validity [Pra71] that are not formalizable in primitive recursive arithmetic. A simple induction on types verifies that (strong) normalizability is closed under application while closure under substitution has to be shown simultaneously.

Separating concerns. With the prospect of computer-checkable formalization and of proof-theoretic analyses of normalization proofs for more complicated calculi we identify independent steps in the proof. This is done by introducing strictly positive inductive definitions of the underlying concepts, thus abandoning geometric notions (such as positions in terms, reduction trees and reduction sequences) that would lead to ponderous arguments in the desired extensions.

Strong normalizability. Intuitively, a term r is strongly normalizing iff there are no infinite reduction sequences starting with r. However, the data type of reduction sequences is notoriously problematic for computer-assisted proof development. Following [Alt93] and the tradition in proof theory, we define strong normalizability of a term r (with respect to a binary relation →) inductively by

{∀r′.r → r′ ⇒ r′ ⇓ \atop r ⇓}

Thus, when checking strong normalizability of a term r it is sufficient to consider every one-step reduct of r instead of all possible (potentially infinite) reduction sequences.

Still, reduct analysis becomes increasingly annoying in normalization proofs for more and more complex systems. Therefore, we characterize strong normalizability via an inductive definition of a set SN given by syntax-directed Horn clauses, reducing the task of checking all one-step reducts to analysing no more than one standard reduct and some subterms. The proof of equivalence with the earlier definition is in fact the only place where reduct analysis has to be carried out.

1Mathematisches Institut der Ludwig-Maximilians-Universität München, felix@joachimski.de

2Institut für Informatik der Ludwig-Maximilians-Universität München, matthes@informatik.uni-muenchen.de

For pure untyped λ-calculus such an inductive characterization has first been presented by van Raamsdonk/Severi [vRS95]. Among other goals, this article aims at extending the underlying notion to extensions of the base calculus by recursion, case operators and generalized eliminations (see below).^{3}

Weak normalizability. A term r is weakly normalizing iff there is a finite reduction sequence starting with r and ending with a term which allows no further reduction. We give an inductive definition more suitable for a satisfying formalization. When checking weak normalization of a term r according to this definition one has to check some reduct of r. Unfortunately this reduct is not determined by r. Therefore, we also characterize weak normalizability via a syntax-directed inductive definition, thus embodying a reduction strategy that easily allows to read off which reduct to check.^{4} Establishing the characterization this time amounts to proving standardization.

Building on these preliminary considerations the normalization proofs in sections 4–7 exclusively argue on the syntax-directed inductive definitions.

Notation for multiple eliminations. In the inductive characterization of strongly normalizing terms we recognize the standard redex of a term by displaying it in head form. This requires the introduction of a metasyntactic abbreviation: A list of terms r_{1}, …, r_{n} is written r⃗ and can be used to denote iterated eliminations like in xr⃗ and (λxs)rr⃗ (which stand for xr_{1} … r_{n} and (λxs)rr_{1} … r_{n}). Notice that those lists may actually be empty, leading to xr⃗ ≡ x (where ≡ is syntactic equality).

It is crucial that we can carry this style of writing down multiple eliminations to more complex term systems as long as they enjoy an introduction/elimination dichotomy under the natural deduction (Curry-Howard) interpretation. This holds for ordinary term application, recursion on natural numbers (corresponding to N-elimination in natural deduction, i.e., induction on N) and case analysis (+-elimination), generalized applications à la von Plato as well as for many other systems not studied in this paper.^{5} Thus we arrive at a more general notion of elimination rR of the term r that may stand for the application of r to R (→-elimination with R a term), recursion rR with R ≡ (s, t) (s the initial term, t the step term, usually written Rec s t r), case analysis rR with R ≡ (x.s, y.t) (commonly denoted by case r of inj_{0}x ⇒ s, of inj_{1}y ⇒ t) and generalized application rR with R ≡ (s, x.t) (for r ≡ y written as t_{x}{r, s} in [Sch99]).

The vector notation turns out to replace concepts like branches and endsegments [Pra71] which have been important elements of normalization arguments in systems with permutative conversions.

Simply-typed λ-calculus. The basic system is dealt with in the first four sections: In section 1 untyped λ-calculus, function types, reduction and weak and strong normalizability are defined. In section 2 weak normalization is shown by a method relying on a proof by induction on normal forms. As we define weak normalizability from the set of normal forms this method is free from any notational overhead, i. e., any defined concept entering the proof is already needed for stating the result, viz. weak normalization. Section 3 contains the characterizations of weakly and strongly normalizing terms (also for the extension by the η-rule), section 4 the proof of strong normalization.

Permutative conversions. They—also called commuting conversions—recover the subformula property^{6} for terms in normal form in a system with sum types and a case-construct. Difficulties arise with so-called critical eliminations r(x.s, y.t) : τ of a term r of type ρ + σ where τ need neither be a subtype of ρ nor of σ. This has led to the invention of endsegments and validity predicates (see [Pra71] for a graphical and [vdP96] for a term-based definition) or improper reductions [Lei75].

3Based on a draft version of the present article, an extension to a logical framework using dependent types has been carried out by Goguen [Gog99] whose typed operational semantics [Gog95] has been found independently of [vRS95]. Interestingly, the initial motivation for the work reported here was a kind of reverse engineering of Goguen’s thesis [Gog94] for systems without dependent types.

4[vR96] stated and proved this characterization correct for pure untyped λ-calculus.

5[Mat98] employs this approach in an analysis of extensions of Girard’s system F by various forms of monotone inductive types. More recently, [Joa01] even gives a precise definition and analysis of the general notion of introduction/elimination systems which incorporate the underlying concept.

6“The type of any subterm of r : ρ is subtype of either the type of a free variable or of ρ.” See, e.g., [Hin97] for a good exposition.

In section 5 we use the vector notation together with an only marginal modification of the basic normalization argument and come up with a short and easily formalizable proof which even covers the η-reduction rules.

Generalized applications. They allow a further simplification of the grammar of normal forms for the λ-calculus by means of a generalized application rule that corresponds to the left introduction rule in sequent calculus. As in the case of sum types we have to add permutative conversions—now for function types—in order to retain the subformula property for normal terms. The methods of section 5 easily carry over to this system as shown in section 6, hence yielding strong normalization which appears to be a new result.

Gödel’s T. Although the normalization proofs in the previous sections of this paper do make use of inductive definitions they could be formalized within primitive recursive arithmetic, since all inductive clauses have finitely many premises only (see [Tro73]). For reasons of proof-theoretical strength we cannot hope to extend the simple normalization proof to Gödel’s T without major modifications since it is well-known that termination of T implies consistency of Peano arithmetic [Göd58] and that this fact is provable in primitive recursive arithmetic.

It will turn out that the inductive characterization SN of the strongly normalizing terms can be extended to T while the embedding of the set of all terms requires the introduction of an infinitely branching clause in an inductive definition of a subset Ω ⊂ SN to cover recursion. A vaguely similar program has first been carried out for a combinatory version in [San67].^{7} In section 7 we cover the full reduction relation of the λ-calculus with primitive recursion in finite types, profiting from our vector-based term display.

Acknowledgments. We would like to thank our mentor Helmut Schwichtenberg for numerous encouraging meetings and stimulating advice. Wilfried Buchholz provided invaluable insight into inductive definitions. Jan von Plato brought to our attention the problem of strong normalization for natural deduction with general eliminations, the solution of which now forms the core of section 6. For repeated discussions and helpful remarks we are grateful to Henk Barendregt, Ulrich Berger, René David, Healfdene Goguen, J. Roger Hindley, Tobias Nipkow^{8} and Anne Troelstra.

1 λ-calculus

1.1. Terms. (Raw) terms r, s, t ∈ Λ are generated from variables x, y, z (of an infinite supply) by the grammar

Λ ∋ r, s ::= x | rs | λxr.

x is bound in λxr. Notationally, we let application associate to the left, writing rs⃗ for rs_{1} … s_{n} ≡ (… (rs_{1}) … s_{n}) with a possibly empty vector s⃗. As remarked in the introduction the use of lists to denote multiple eliminations is a metasyntactic device. Pointwise application of a function f or a predicate P to a list of terms r⃗ will be denoted by f(r⃗) and P (r⃗), respectively; the comma serves to denote concatenation and elongation: r, r⃗, s⃗, s ≡ r, r_{1}, …, r_{n}, s_{1}, … s_{m}, s.

We use the point notation λx.r to omit the parentheses in λx(r), where the range of the point extends as far as syntactically possible. The simultaneous substitution of terms s⃗ for x⃗ in r is defined as usual and written either rx⃗[s⃗] or r[x⃗ := s⃗]. Terms which differ only in names of bound variables are identified, i.e., α-equal terms are equal.

7Other approaches can be found for instance in [Dil68], [How80] and [Sch93].

8Nipkow verified lemmata 3.3, 3.4 and 4 with the theorem prover Isabelle and gave worthwhile hints for improvement.

1.2. Inductive characterization and normal forms. The set of terms is inductively characterized by the following grammar —

Λ ∋ r, s ::= xr⃗ | λxr | (λxr)ss⃗,

where the last form captures non-normal terms; we will see later that this presentation exhibits the leftmost outermost reducible expression (redex). Excluding this last clause we obtain the grammar of normal forms

NF ∋ r ::= xr⃗ | λxr.

1.3. Types and type assignment. ρ, σ, τ are generated from basic types ι by the grammar

ρ, σ ::= ι | ρ → σ.

Given a unique assignment x : ρ of types to variable symbols such that for each type infinitely many variables exist, we can determine the typable terms and their unique type by the following rules:^{9}

\begin{matrix}r : ρ → σ & s : ρ \\ rs : σ \end{matrix}  \begin{matrix}r : σ & x : ρ \\ λxr : ρ → σ \end{matrix}

We will decorate (sub-)terms with types in superscripts (as in r^{ρ}s) in order to signify that they are typable and get the respective type. Λ^{→} denotes the set of typable terms under a fixed type assignment for the variables.

1.4. Reduction. The reduction relation → := →_{β} is generated from the β-conversion rule (λxr)s → r_{x}[s] by means of the compatible closure, extending conversion inductively by

r → r′ ⟹ λxr → λxr′, rs → r′s, sr → sr′.

→^{+} is the transitive closure of → (defined inductively), →^{∗} is the transitive, reflexive closure. The resulting reduction relation is also compatible in the sense that r → r′ implies s_{x}[r] →^{∗} s_{x}[r′], and s_{x}[r] → s_{x}[r′] if x occurs exactly once in s. It is substitutive insofar as r → r′ implies r_{x}[s] → r′_{x}[s]. That reduction preserves typability and types is a consequence of compatibility together with the fact that type-correct substitution respects types.^{10}

We see how our inductive term characterization finds the leftmost outermost convertible expression^{11} and that NF exactly captures the irreducible terms.

→_{η} is generated from the conversion rule λx.rx → r (if x is not free in r) using the compatible closure. We write →_{βη} for →_{β} ∪ →_{η}.

Notations. We define r ↓ (r is weakly normalizing) inductively by

{r ∈ NF \atop r ↓}  {r → r′ ↓ \atop r ↓}

Thus r ↓ ⇔ ∃s ∈ NF.r →^{∗} s.

r ⇓ (r is strongly normalizing) is defined in the introduction. The set {r | r ⇓} amounts to the well-founded part WF_{→} of the reduction relation.^{12} r ⇓ is equivalent to: There is no infinite reduction sequence starting with r [⇒: Induction on r ⇓. ⇐ is an instance of bar induction]. We write #r for the finite height of the (finitely branching) reduction tree of strongly normalizing terms r, given recursively by #r := sup{#r′ + 1 | r → r′}.

9Although our choice of typing discipline does shorten arguments considerably, it is not vital for the course of proofs, since we are only dealing with simple types here.

10We will not further comment on typability and type issues for the rest of this paper in order to keep the presentation short.

11See [Bar84] for a discussion of the mentioned concepts and various reduction strategies.

12Let ≻ be a binary relation on the fixed set M.

Prog_{≻}(X) :⇔ ∀x ∈ M.(∀y ≺ x.y ∈ X) ⇒ x ∈ X,  (X is ≻-progressive)

WF_{≻}  := ⋂{X ⊆ M | Prog_{≻}(X)}.

• The definition of the well-founded part WF_{≻} yields the schema Prog_{≻}(X) ⟹ WF_{≻} ⊆ X of accessible

part induction. (footnote continued on page 5)

2 Weak normalization proof

2.1. The proof. In this section we assume that all mentioned terms are typable.

Lemma. r, s^{ρ} ∈ NF ⟹ (i) rs ↓, (ii) r_{x}[s] ↓.

Proof by simultaneous induction on ρ, side induction on r ∈ NF.

yr⃗. Assume yr⃗ ∈ NF has been obtained from r⃗ ∈ NF. (i). yr⃗s ∈ NF follows immediately. (ii). Side induction hypothesis (ii) shows r⃗_{x}[s] ↓; let t⃗ be the respective normal forms. If x ≢ y then (yr⃗)_{x}[s] = yr⃗_{x}[s] ↓. Otherwise

(yr⃗)_{x}[s] ≡ (xr⃗)_{x}[s] = sr⃗_{x}[s] →^{∗} st⃗.

Thus for sr⃗_{x}[s] ↓ it suffices to show st⃗ ↓. For this we use an additional induction on the length of t⃗. If this vector is empty st⃗ ≡ s ∈ NF by assumption. Otherwise t⃗ ≡ t⃗′, t and by induction hypothesis we have st⃗′ ↓ with normal form s′. Since st⃗′ is applied to t we know that the type of t is a subtype of the type ρ of s. Hence the main induction hypothesis (i) yields s′t ↓, with normal form s′′. Putting the reductions together we get (with the help of compatibility)

st⃗ ≡ st⃗′t →^{∗} s′t →^{∗} s′′ ∈ NF.

λyr. (i). λyr ∈ NF is derived from r ∈ NF. Hence the side induction hypothesis (ii) for r proves r_{y}[s] ↓. Consequently (λyr)s → r_{y}[s] also normalizes. (ii). Without loss of generality y ≢ x and y not free in s^{13}, so (λyr)_{x}[s] = λyr_{x}[s]. By side induction hypothesis (ii) r_{x}[s] ↓, thus λyr_{x}[s] ↓. Qed

Theorem. r^{ρ} ↓.

Proof by induction on r. x ∈ NF by definition. rs ↓ by the lemma (part (i)), using the induction hypothesis for r and s. λxr ↓, since by induction hypothesis r ↓. Qed

2.2. Extracted program. By formalizing this constructive normalization proof in the style of [Ber93] we obtain

• the algorithmic content nf : Λ^{→} → NF of the theorem (defined by recursion on the term

structure):

nf(x)  := x
nf(λxr) := λx nf(r)
nf(rs) := app(nf(r), nf(s))

• the algorithms app : NF × NF → NF, subst_{x} : NF × NF → NF (with auxiliary function app_{s} : NF^{∗} → NF for s ∈ NF where NF^{∗} denotes the set of finite lists over NF and ε is the empty list), extracted from the proofs of part (i) and (ii) of the lemma (defined by recursion corresponding to the induction principles used):

• WF_{≻} is ≻-progressive itself.

• Definition by recursion on WF_{≻} is admissible, since WF_{≻} is an example of a deterministic inductive defini-

tion.

• If ≻ ⊆ ≻′ then Prog_{≻}(X) implies Prog_{≻′}(X), hence WF_{≻′} ⊆ WF_{≻}, i.e., λ≻.WF_{≻} is antitone with respect

to ⊆.

• WF_{≻} = WF_{≻^{+}} where ≻^{+} is the transitive closure of ≻. [For the interesting part WF_{≻} ⊆ WF_{≻^{+}} one has to

show that WF_{≻^{+}} is ≻-progressive. ⊇ uses antitonicity.] This means that “course-of-generation-induction”

is a derived induction principle, the use of which will be announced as induction on WF_{≻^{+}}.

13thanks to the identification of α-equal terms

app(yr⃗, s)  := yr⃗s
app(λyr, s)  := subst_{y}(r, s)
subst_{x}(yr⃗, s) := if x ≡ y then app_{s}(subst_{x}(r⃗, s)) else y subst_{x}(r⃗, s)
app_{s}(ε) := s
app_{s}(t⃗, t) := app(app_{s}(t⃗), t)
subst_{x}(λyr, s) := λy subst_{x}(r, s)

2.3. A reformulation. First notice that

(∗) r ∈ NF ⟹ rx ↓

[Case λxr:^{14} (λxr)x → r ∈ NF. Case yr⃗: yr⃗x ∈ NF if r⃗ ∈ NF]. This fact can be used to merge the two assertions of the lemma into one that speaks about substitution only, allowing a shorter proof that does no more involve an induction on the length of the application in the case of (ii) yr⃗. We are grateful to René David for hinting at this trick which he found and showed to us for the strong normalization case (see section 4) after our presentation of a very early version of the present paper.^{15}

Lemma. r, s^{ρ} ∈ NF ⟹ r_{x}[s] ↓.

Proof by induction on ρ, side induction on r ∈ NF.

Case yr⃗. The proof is trivial if r⃗ is empty or x ≢ y. Otherwise yr⃗ = (xt^{ρ_{0}})^{ρ_{1}}t⃗ with ρ = ρ_{0} → ρ_{1}.

• By the side induction hypothesis t_{x}[s] ↓, t⃗_{x}[s] ↓ with normal forms t′, t⃗′. Hence z_{1}t⃗′ ∈ NF for a new variable z_{1} of type ρ_{1}.

• (∗) shows sz_{0} ↓ for any new variable z_{0} of type ρ_{0}, let s′ be a^{16} normal form. By

substitutivity

st′ = (sz_{0})_{z_{0}}[t′] →^{∗} s′_{z_{0}}[t′].

By induction hypothesis at ρ_{0} (which is a subtype of ρ) we get s′_{z_{0}}[t′] ↓ with normal form — say — s_{0}.

Together this allows to apply the induction hypothesis for ρ_{1} to obtain (z_{1}t⃗′)_{z_{1}}[s_{0}] ↓ and this provides a normal form of the term in question:

(xtt⃗)_{x}[s] = st_{x}[s]t⃗_{x}[s] →^{∗} st′t⃗′ →^{∗} s_{0}t⃗′ ↓ .

Case λyr. (λyr)_{x}[s] = λyr_{x}[s], so the side induction hypothesis proves the claim. Qed

Corollary. r, s ∈ NF ⟹ rs ↓.

Proof. Use the lemma for xs and r with new x. Qed The extracted algorithms subst_{x} and app differ from the previously found programs and use the constructive content app^{x} : NF → NF of the proof of (∗).

14This is a rather subtle application of bound variable renaming. It is, of course, possible to make it explicit.

15In [Dav01], this idea is made fruitful for the uniform proof of several known and also new characterizations of terms typable in systems of intersection types by normalization properties.

16Confluence ensures that normal forms are unique but this is not required throughout the paper.

app^{x}(λxr)  := r^{17}
app^{x}(yr⃗)  := yr⃗x
subst_{x}(λyr, s) := λy subst_{x}(r, s)
subst_{x}(y, s)  := if x ≡ y then s else y
subst_{x}(ytt⃗, s) := if x ≡ y
then subst_{z_{1}}(z_{1}subst_{x}(t⃗, s), subst_{z_{0}}(app^{z_{0}}(s), subst_{x}(t, s)))
(z_{0} not free in s, z_{1} not free in t⃗, s)
else y subst_{x}(t, s)subst_{x}(t⃗, s)
app(r, s)  := subst_{x}(xs, r),  (x not free in s)

3 The sets WN and SN

In the proof of Lemma 2.1 we used three closure properties of the set {r | r ↓}.

r⃗ ↓ ⟹ xr⃗ ↓,
r ↓ ⟹ λxr ↓,
r_{x}[s]s⃗ ↓ ⟹ (λxr)ss⃗ ↓ .

We now use these clauses to generate the sets WN and SN inductively which will turn out to capture the concepts weakly and strongly normalizing exactly, even in the context of untyped λ-calculus. The characterization of WN and SN with respect to the intuitive notions of weak and strong normalizability can be found in [vRS95].^{18}

3.1. Definition. The sets SN ⊂ WN ⊂ Λ are defined inductively by the following rules.

r⃗ ∈ WN ; (Var) ; xr⃗ ∈ WN  r ∈ WN ; (λ) ; λxr ∈ WN  r_{x}[s]s⃗ ∈ WN ; (β) ; (λxr)ss⃗ ∈ WN

r⃗ ∈ SN ; (Var) ; xr⃗ ∈ SN  r ∈ SN ; (λ) ; λxr ∈ SN  \begin{aligned}r_{x}[s]s⃗ ∈ SN & s ∈ SN \\ & (β) \\ (λxr)ss⃗ ∈ SN \end{aligned}

Remark. The derived term of each rule has a different form — in fact, there is a one-to-one correspondence between the rules and the grammar rules in 1.2 — and therefore the sets WN and SN are generated freely, rendering recursion admissible. Furthermore both sets contain NF by definition.

Using the abbreviation ℧ := (λx.xx)(λx.xx) ∈ Λ \ WN we see that (λyz)℧ ∈ WN \ SN.

3.2. Weak normalization for WN. r ∈ WN implies r ↓, since the defining rules are closure properties of {r | r ↓}. But the converse direction also holds,^{19} so we have r ∈ WN ⟺ r ↓. The normal form ↓(r) of a term r ∈ WN can be defined by recursion as follows.^{20}

17If we used explicit renaming of bound variables this clause would read app^{x}(λyr) := r_{y}[x].

18See the introduction for the reasons why we do not simply refer to those results and the equivalence of the intuitive definitions with r ↓ and r ⇓.

19This means that the reduction strategy that underlies the definition of WN actually is the standard reduction strategy guaranteed to exist by the standardization theorem (see, e.g., [Dav95] for a short exposition).

↓: WN ⟶ NF,
↓(xr⃗) := x ↓(r⃗),
↓(λxr) := λx ↓(r),
↓((λxr)ss⃗) := ↓(r_{x}[s]s⃗).

3.3. Lemma. (Soundness). SN ⊆ WF_{→}.

Proof by induction on SN, i.e., by showing that the set of strongly normalizing terms is closed under the rules defining SN.

(Var). Assume r⃗ ⇓. Since each reduction on xr⃗ has to take place in one of the r⃗, we also get xr⃗ ⇓.

(λ). Each reduction on λxr actually occurs in r, so the hypothesis r ⇓ yields λxr ⇓.

(β). We show (λxr)ss⃗ ⇓ by main induction on s ⇓ and side induction on r_{x}[s]s⃗ ⇓.^{21} We have to prove t ⇓ for any immediate reduct t. The following reductions are possible.

(λxr)ss⃗ → (λxr′)ss⃗. Then r_{x}[s]s⃗ → r′_{x}[s]s⃗ by substitutivity, hence by side induction hypothesis (λxr′)ss⃗ ⇓.

(λxr)ss⃗ → (λxr)s′s⃗. Then r_{x}[s]s⃗ →^{∗} r_{x}[s′]s⃗ by compatibility, hence also r_{x}[s′]s⃗ ⇓. The main induction hypothesis yields (λxr)s′s⃗ ⇓.

(λxr)ss⃗ → (λxr)ss⃗′. Then r_{x}[s]s⃗ → r_{x}[s]s⃗′, hence by side induction hypothesis (λxr)ss⃗′ ⇓. (λxr)ss⃗ → r_{x}[s]s⃗ ⇓ by assumption. Qed

Along the lines of the proof one can verify the following inductive bounds on the height #r of the reduction tree for terms r ∈ SN:

#xr⃗ ≤ ∑#r⃗, #λxr ≤ #r^{22} and #(λxr)ss⃗ ≤ 1 + #r_{x}[s]s⃗ + #s.

3.4. Completeness. For the purpose of the normalization proof it is not necessary to know that SN captures all strongly normalizing terms. Nevertheless the result is interesting in its own right.

Lemma. WF_{→} ⊆ SN.

The proof uses nested inductions on WF_{→} and the term structure. In fact, the lemma is an instance of the following proposition, the generality of which will pay off in section 5.

Proposition. Let → be a binary relation on the set WF_{▷} with

∀r ∀r′ ∀r′′.r ▷ r′ → r′′ ⇒ ∃r′′′.r → r′′′ ▷ r′′ (commutation).

Then WF_{→} ⊆ WF_{▷∪→}.

20Goguen’s typed operational semantics [Gog95], which inspired our work, can be understood as a combination of SN, NF and the normal form function ↓ into one inductive definition.

21This argument is crucial to the proof of strong normalization and to our knowledge it is an unavoidable part of any strong normalization proof amenable to a faithful formalization. Most often, however, it is hidden in an argument via infinite reduction sequences. In order to clarify the intricate structure of the argument we spell out the nesting of inductions precisely. Main induction on s ⇓ amounts to showing →-progressivity of the set

M := {s | ∀r, s⃗.r_{x}[s]s⃗ ⇓ ⇒ (λxr)ss⃗ ⇓}.

So assume that any one-step-reduct of s is in M. For s ∈ M we do side induction on r_{x}[s]s⃗ ⇓, i.e., we show →-progressivity of the set

N := {t′ | t′ ⇓ ∧ ∀r, s⃗.t′ = r_{x}[s]s⃗ ⇒ (λxr)ss⃗ ⇓}.

So assume t′ is a term and each immediate reduct is in N. We have to show t′ ∈ N. t′ ⇓ follows from the definition of ⇓, since N ⊆ WF_{→}. If t′ has the form r_{x}[s]s⃗ we have to show (λxr)ss⃗ ⇓, so we prove t ⇓ for every one-step reduct t. Henceforward, each clause of the proof in the main text can be recast using the pending assumptions.

22Clearly, the first two inequalities even hold with =.

Proof by (accessible part) induction on →. With ≻:= ▷ ∪ → our goal is Prog_{→}(WF_{≻}), which reads ∀r.(∀s←r.s ∈ WF_{≻}) ⇒ r ∈ WF_{≻}. Using induction on ▷ we need to prove

Prog_{▷}(λr.(\underbrace{∀s←r.s ∈ WF_{≻}}_{≡:Δ(r)}) ⇒ r ∈ WF_{≻}) ≡ ∀r.(∀t ◁ r.Δ(t) ⇒ t ∈ WF_{≻}) ∧ Δ(r) ⇒ r ∈ WF_{≻}.

So assume r with

(1) ∀t ◁ r.Δ(t) ⇒ t ∈ WF_{≻} and

(2) Δ(r) ≡ ∀s←r.s ∈ WF_{≻}.

We need to show r ∈ WF_{≻}. Since the well-founded part WF_{≻} is ≻-progressive it suffices to show ∀s ≺ r.s ∈ WF_{≻}. So let r ≻ s.

Case r → s. Then s ∈ WF_{≻} holds by (2).

Case r ▷ s. Using (1) it suffices to know Δ(s), i.e., ∀t←s.t ∈ WF_{≻}. So assume r ▷ s → t. Then by commutation there exists an r′ with r → r′ ▷ t, so by (2) also r′ ∈ WF_{≻}, hence t ∈ WF_{≻} as r′ ≻ t. Qed

To get the lemma, we first apply the proposition to → and a restricted subterm relation ▷ given by the clauses

xr⃗ ▷ r_{k}, λxr ▷ r, and (λxr)ss⃗ ▷ s.

Clearly, WF_{▷} = Λ. Commutation is shown by simple case analysis.

λxr ▷ r → r′ ⟹ λxr → λxr′ ▷ r′,
xr⃗ ▷ r_{k} → r′_{k} ⟹ xr⃗ → xr⃗′ ▷ r′_{k},
(λxr)ss⃗ ▷ s → s′ ⟹ (λxr)ss⃗ → (λxr)s′s⃗ ▷ s′.

The proposition yields WF_{→} ⊆ WF_{▷∪→}. The latter is a subset of SN by antitonicity of λ≻.WF_{≻}, since SN is generated as WF_{⊐} with ⊐ extending ▷ by head-conversion

(λxr)ss⃗ ⊐ r_{x}[s]s⃗.

3.5. On η. The set SN also captures exactly the notion of strongly normalizing for →_{βη}. For WF_{→_{βη}} ⊆ SN we apply antitonicity of λ≻.WF_{≻}. For the converse inclusion, the proof of Lemma 3.3 remains largely unaltered due to the fact that η-reductions on the left side of an application (as in (λx.rx)s →_{η} rs) are also β-reductions and thus need not be considered. Furthermore η-reductions on the right side of an application (i.e., rλx.sx →_{η} rs) are always covered by the induction hypothesis. So we only have to deal with the new case of a head-η-reduction λx.sx → s in part (λ) of the proof when showing that λx.sx ⇓ follows from sx ⇓, but clearly s ⇓, since the set {r | r ⇓} = WF_{→_{βη}} of strongly normalizing terms is closed under subterms.

It has been shown elsewhere [AJ01] that strong normalization (and confluence) of combined βreduction and η-expansion follows from the same property of β-reduction alone. As a consequence SN also exactly characterizes the set of strongly normalizing terms with respect to →_{βη↑} (defined loc. cit.).

3.6. The SN-method [Mat98]. Having the characterization of strongly normalizing terms via SN at hand, one can rearrange traditional strong normalization proofs, e.g., by the method of logical predicates, such that they do not refer to reduction. Using suitable extensions of the vector notation, SN can also be defined for system F and extensions such as by monotone inductive types. The saturated sets variant [Tai75] of Girard’s normalization proof may be adapted, with the notion of saturatedness naturally arising from the definition of SN. This is also true for systems with permutative conversions as shown, e. g., in [Mat00].

4 Strong normalization proof

In this section we lift the proof of Lemma 2.1 to strong normalization, using the SN-method explained above. We assume throughout that all displayed terms are typable.

Lemma. r ∈ SN, s^{ρ} ∈ SN ⟹ (i) rs ∈ SN, (ii) r_{x}[s] ∈ SN.

Proof by simultaneous induction on ρ and side induction on the generation of r ∈ SN. In essence the proof is parallel to that of Lemma 2.1 but the use of SN shortens arguments considerably.

(Var). r ≡ yr⃗ ∈ SN is generated from r⃗ ∈ SN. (i). r⃗ ∈ SN together with s ∈ SN shows yr⃗s ∈ SN, using (Var). (ii). Side induction hypothesis (ii) yields r_{k}[x := s] ∈ SN for each r_{k} in r⃗. Now if y ≢ x we get yr⃗_{x}[s] ∈ SN at once. Otherwise we need sr⃗_{x}[s] ∈ SN, but this follows by multiple applications of the main induction hypothesis for (i), since each of the arguments in the nested application has a subtype of ρ.^{23}

(λ). λyr ∈ SN is generated from r ∈ SN. (i). For (λyr)s ∈ SN it suffices to show r_{y}[s] ∈ SN. But this is exactly the side induction hypothesis for (ii). (ii). Side induction hypothesis (ii) yields r_{x}[s] ∈ SN and consequently λyr_{x}[s] ∈ SN.

(β). (λyr)tt⃗ ∈ SN is obtained from r_{y}[t]t⃗ ∈ SN and t ∈ SN. Therefore both side induction hypotheses apply and yield (i) r_{y}[t]t⃗s ∈ SN and (ii) (r_{y}[t]t⃗)_{x}[s], t_{x}[s] ∈ SN, respectively. From these we obtain the assertions (λyr)tt⃗s ∈ SN (i) and ((λyr)tt⃗)_{x}[s] ∈ SN (ii) by definition of SN. Qed

Remark. A proof of the statement of the lemma with SN replaced by WN is only marginally simpler.

Theorem. All terms are strongly normalizable.

Proof. Show r ∈ SN by induction on the structure of r, using the lemma. Lemma 3.3 proves strong normalizability of r. Qed

Again (compare with 2.3), we can merge parts (i) and (ii) of the lemma into closure under substitution using the

Proposition. r ∈ SN ⟹ rx ∈ SN.^{24}

Proof by induction on SN. Qed

Lemma. r, s^{ρ} ∈ SN ⟹ r_{x}[s] ∈ SN.

Proof by induction on ρ, side induction on r ∈ SN. We only mention the variable case with a non-trivial elimination (xt^{ρ_{0}})^{ρ_{1}}t⃗ on the same variable x that is substituted by s. Then ρ = ρ_{0} → ρ_{1}.

• By the side induction hypothesis we have t_{x}[s], t⃗_{x}[s] ∈ SN. Consequently also zt⃗_{x}[s] ∈ SN for a fresh variable z : ρ_{1}.

• By the proposition we have sy^{ρ_{0}} ∈ SN for a new y, hence by induction hypothesis for ρ_{0} also st_{x}[s] ∈ SN.

• The induction hypothesis for ρ_{1} shows (xtt⃗)_{x}[s] = (zt⃗_{x}[s])_{z}[st_{x}[s]] ∈ SN. Qed

As a corollary we get closure of SN under application, again.

23More precisely, this argument involves an additional induction on the length of the list r⃗, analogous to the proof of Lemma 2.1.

24Induction on rx ∈ SN would show the converse direction.

5 Extension to permutative conversions

We proceed to a typed calculus with sums and permutative conversions similar to those being studied in [Pra71], [Lei75] or [GLT89]. In contrast to their expositions we do not consider product types or other first-order extensions, although the proof method copes with them, too.

5.1. (Raw) terms. Let always i ∈ {0, 1}.

r, s, t ::= x | λyr | rs | inj_{i}r | s(x_{0}.t_{0}, x_{1}.t_{1}).

The variables y, x_{0}, x_{1} get bound in r, t_{0}, t_{1}, respectively.

5.2. Types and type assignment. The type grammar is extended to sums ρ + σ. In order to get unique types for typable terms we add a type subscript to the injection (writing inj_{i,ρ}) that will, however, be omitted.

{r : ρ_{i} \atop inj_{i,ρ_{1−i}}r : ρ_{0} + ρ_{1}}  \begin{matrix}r : ρ_{0} + ρ_{1} & s_{0} : σ & s_{1} : σ \\ r(x_{0}^{ρ_{0}}.s_{0}, x_{1}^{ρ_{1}}.s_{1}) : σ \end{matrix}

(The type superscripts of variables in the second rule indicate the type assignments for those variables. In fact, the assignments are premises of the rule.) Note that typing rules out pathological terms like (λxr)(x.s, y.t) or (inj_{i}r)s.

In the rest of this section we require all mentioned terms to be typable.

5.3. Inductive characterization. We use capital letters R, S, T for eliminations^{25}, which are either terms or sum-eliminations (x_{0}.s_{0}, x_{1}.s_{1}):

R ::= r | (x_{0}.s_{0}, x_{1}.s_{1}).

The terms r, s_{0} and s_{1} are named elimination terms in this definition. Eliminations of the form (x_{0}.s_{0}, x_{1}.s_{1}) are called critical. We write (x_{0}.s_{0}, x_{1}.s_{1})_{x}[t] for the capture-free substitution (x_{0}.s_{0}[x := t], x_{1}.s_{1}[x := t]).

Using a square bracket notation […] for optional syntax elements, we can inductively characterize the set of typed terms by

Λ^{→+} ∋ r, s ::= xr⃗ [R] | λxr | inj_{i}r |
xr⃗(x_{0}.s_{0}, x_{1}.s_{1})SS⃗ | (λxr)sS⃗ | (inj_{i})(x_{0}.s_{0}, x_{1}.s_{1})R⃗.

5.4. Normal forms. The last three clauses in the inductive term characterization are not considered normal. This is intuitive for the β-redices (λxr)sS⃗ and (inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗. The term xr⃗(x_{0}.s_{0}, x_{1}.s_{1})SS⃗ need not fulfil the subformula property in general.

NF ∋ r ::= xr⃗ [(x_{0}.s_{0}, x_{1}.s_{1})] | λxr | inj_{i}r.

Notice how the inductive term characterization uniquely determines the canonical redex of nonnormal terms.

5.5. Reduction. These redices are removed by means of β-conversion

(λxr)s →_{β_{→}} r_{x}[s], (inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1}) →_{β_{+}} s_{i}[x_{i} := r],

and permutative conversions

r(x_{0}.s_{0}, x_{1}.s_{1})S →_{π} r(x_{0}.s_{0}S, x_{1}.s_{1}S).^{26}

25Note the ambiguity: R as well as rR are called eliminations (cf. the introduction).

The compatible closure → of these conversions is given by

r → r′ ⟹ sr → sr′, rS → r′S, λxr → λxr′, inj_{i}r → inj_{i}r′,
s(x.r, y.t) → s(x.r′, y.t), s(y.t, x.r) → s(y.t, x.r′).

5.6. Definition. The set SN is generated inductively by the following rules where (x.r, y.t) ∈ SN is an abbreviation for r, t ∈ SN.

r⃗ [,R] ∈ SN ; (Var) ; xr⃗ [R] ∈ SN  r ∈ SN ; (λ) ; λxr ∈ SN

xr⃗(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗ ∈ SN ; (Var_{π})^{27} ; xr⃗(x_{0}.s_{0}, x_{1}.s_{1})SS⃗ ∈ SN  r ∈ SN ; (inj) ; inj_{i}r ∈ SN

r_{x}[s]S⃗ ∈ SN  s ∈ SN (β_{→})
(λxr)sS⃗ ∈ SN
s_{i}[x_{i} := r]S⃗ ∈ SN  s_{1−i}S⃗ ∈ SN  r ∈ SN (β_{+})
(inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗ ∈ SN

Remark. xR⃗ is necessarily generated from an xr⃗ [R] where a potentially critical elimination R occurs outermost, if at all. Furthermore xr⃗ [R] can be obtained from xR⃗ by permutative conversions.

It is also worth mentioning that the definition of SN incorporates permutations for variable eliminations only. The following lemma shows that this is sufficient to capture all strongly normalizing terms.

Lemma. SN = WF_{→}.

Proof. “⊆” (soundness): We again have to show that WF_{→} = {r | r ⇓} has the closure properties which define SN. For (Var) and (λ) the proof remains unchanged, (inj_{i}) is as trivial as (λ). The proof for (β_{→}) is verbosely the same as that in section 3, replacing s⃗ by S⃗. Notice that now permutative conversions may affect the length of the list S⃗.

(Var_{π}). Show xr⃗(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗ ⇓ ⟹ xr⃗(x_{0}.s_{0}, x_{1}.s_{1})SS⃗ ⇓ by induction on xr⃗(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗ ∈ WF_{→^{+}}. We have to show t ⇓ for every reduct t of xr⃗(x_{0}.s_{0}, x_{1}.s_{1})SS⃗. The only interesting case arises with S⃗ ≡ T T⃗ and a permutation of S ≡ (y_{0}.t_{0}, y_{1}.t_{1}) with T leading to

t = xr⃗(x_{0}.s_{0}, x_{1}.s_{1})(y_{0}.t_{0}T, y_{1}.t_{1}T)T⃗.

t ⇓ follows by induction hypothesis as

xr⃗(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗ ≡ xr⃗(x_{0}.s_{0}(y_{0}.t_{0}, y_{1}.t_{1}), x_{1}.s_{1}(y_{0}.t_{0}, y_{1}.t_{1}))T T⃗

reduces with three permutative reduction steps (hence once →^{+}) to

xr⃗(x_{0}.s_{0}(y_{0}.t_{0}T, y_{1}.t_{1}T), x_{1}.s_{1}(y_{0}.t_{0}T, y_{1}.t_{1}T))T⃗.

26Strictly speaking, we require x_{0}, x_{1} not to be free in S. Otherwise the rule would not comply with α-equality.

27This clause is subject to the same proviso as the rule of permutative conversion.

(β_{+}). Show that s_{i}[x_{i} := r]S⃗ ⇓, s_{1−i}S⃗ ⇓ and r ⇓ imply (inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗ ⇓ by main induction on r ⇓, side induction on s_{i}[x_{i} := r]S⃗ ⇓, side side induction on s_{1−i}S⃗ ⇓ and a third side induction on the length of S⃗. We have to show t ⇓ for every reduct t of (inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗. The most interesting case is when S⃗ ≡ T T⃗ and (x_{0}.s_{0}, x_{1}.s_{1}) is permuted with T, i.e., t = (inj_{i}r)(x_{0}.s_{0}T, x_{1}.s_{1}T)T⃗. This is an application of the third side induction hypothesis

since (s_{i}T)[x_{i} := r]T⃗ = s_{i}[x_{i} := r]S⃗ ⇓, s_{1−i}T T⃗ ⇓ and r ⇓.^{28}

“⊇” (completeness): Use nested course-of-generation inductions on r ⇓ and r. Actually, we may also apply the general proposition of 3.4. To this end define ▷ as follows.

λxr ▷ r,  inj_{i}r ▷ r,
xr⃗ [R] ▷ r_{k},  xr⃗ (x_{0}.s_{0}, x_{1}.s_{1}) ▷ s_{i},
(λxr)sS⃗ ▷ s,  (inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗ ▷ s_{1−i}S⃗ and r.

Clearly WF_{▷} = Λ^{→+}, since the size of the terms decreases in each clause. Commutation of ▷ with →^{+} is shown by simple case analysis where the crucial case necessitates →^{+} instead of →: (inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗ ▷ s_{1−i}S⃗ →^{+} t implies

(inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗ →^{∗} (inj_{i}r)(x_{0}.s_{0}S⃗, x_{1}.s_{1}S⃗) →^{+} \{ \begin{matrix}(inj_{0}r)(x_{0}.s_{0}S⃗, x_{1}.t) \\ (inj_{1}r)(x_{0}.t, x_{1}.s_{1}S⃗) \end{matrix} \} ▷ t.

Proposition 3.4 yields WF_{→^{+}} ⊆ WF_{▷∪→^{+}}. Using properties of WF we get

WF_{→} = WF_{→^{+}} ⊆ WF_{▷∪→^{+}} ⊆ WF_{▷∪→} ⊆ SN.

Qed

Lemma. r(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗ ∈ SN ⟹ r(x_{0}.s_{0}, x_{1}.s_{1})SS⃗ ∈ SN.

Proof by course-of-generation-induction on r(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗ ∈ SN. Distinguish cases according to the shape of r. Most cases are a trivial application of the induction hypothesis. Interesting are

Case xr⃗(y_{0}.t_{0}, y_{1}.t_{1}). Assume xr⃗(y_{0}.t_{0}, y_{1}.t_{1})(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗ ∈ SN. This has been concluded by repeated application of (Var_{π}) from

xr⃗(y_{0}.t_{0}(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗, y_{1}.t_{1}(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗) ∈ SN,

i.e., we have got r⃗ ∈ SN and both t_{i}(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗ ∈ SN before. By induction hypothesis we get t_{i}(x_{0}.s_{0}, x_{1}.s_{1})SS⃗ ∈ SN. Hence

xr⃗(y_{0}.t_{0}(x_{0}.s_{0}, x_{1}.s_{1})SS⃗, y_{1}.t_{1}(x_{0}.s_{0}, x_{1}.s_{1})SS⃗) ∈ SN.

Using the rule (Var_{π}) repeatedly we obtain

xr⃗(y_{0}.t_{0}, y_{1}.t_{1})(x_{0}.s_{0}, x_{1}.s_{1})SS⃗ ∈ SN.

Case inj_{i}r. Assume (inj_{i}r)(x_{0}.s_{0}S, x_{1}.s_{1}S)S⃗ ∈ SN. This has been derived from (s_{i}S)[x_{i} := r]S⃗ = s_{i}[x_{i} := r]SS⃗ ∈ SN and r, s_{1−i}SS⃗ ∈ SN. Hence (inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})SS⃗ ∈ SN. Qed 5.7. Lemma. For all types ρ, for all r ∈ SN,

28This case requires s_{1−i}S⃗ ⇓ as second premise, justifying the somewhat peculiar fact that (β_{+}) goes back to s_{1−i}S⃗ instead of the subterm s_{1−i} of (inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗. In an untyped calculus the term (inj_{0}x)(x_{0}.y, x_{1}.λz.zz)(λz.zz)

would be a counter-example to SN ⊆ WF_{→} with the wrong formulation: The permutative reduct has ℧ as a subterm.

(i) if s^{ρ} ∈ SN then rs ∈ SN, (ii) if r : ρ ≡ ρ_{0} + ρ_{1} and s_{0}, s_{1} ∈ SN then r(x_{0}.s_{0}, x_{1}.s_{1}) ∈ SN, (iii) if s^{ρ} ∈ SN then r_{x}[s] ∈ SN. Proof. By simultaneous induction on ρ, side induction on r ∈ SN. Distinguish cases according

to r ∈���r_{0}, r_{1})R⃗. Case xS⃗. We need xS⃗(rs⃗ ; 0, rs⃗ ; 1)R⃗s⃗ ∈ SN, which amounts to rs⃗ ; 0, R⃗s⃗ ∈ SN and rs⃗ ; 1 ∈ SN. The latter follows from the main induction hypothesis for rn⃗ ; 1 = r′_{1}. The other terms are in SN since rs⃗ ; 0R⃗s⃗ ∈ SN by the main induction hypothesis (applied to r′_{0}R⃗′) and SN is closed under the subterm relation. Case (R_{S}). Suppose rn⃗ = (Sr′)(s′, t′)R⃗′ ∈ SN comes from t′r′(r′(s′, t′))R⃗′ ∈ SN. Now if r = (Sr′′)(s, t)R⃗ then the claim follows easily from the induction hypothesis. Otherwise r = x_{k}(s, t)R⃗, n_{k} is the successor of — say — m and we need to show s_{k}(ss⃗, ts⃗)R⃗s⃗ ∈ SN. Similar to the case (R_{0}) we show the more general statement ∀ŝ�.|ŝ| = Sm ⟹ ŝ(ss⃗, ts⃗)R⃗s⃗ ∈ SN by side induction on ŝ ∈ SN. Since |ŝ| = Sm, the variable cases and 0 can be excluded. All reduction cases are easily handled by the side induction hypothesis. So we are left with the case (S) where ŝ = Sŝ′ and |ŝ′| = m. It suffices to show ts⃗ŝ′(ŝ′(ss⃗, ts⃗))R⃗s⃗ ∈ SN. This term can be expressed as r_{x⃗,x}^{∗}[s⃗, ŝ′] with r^{∗} = tx(x(s, t))R⃗ and a new variable x. More- over,  r_{x⃗,x}^{∗}[n⃗, m] = t′r′(r′(s′, t′))R⃗′, so we can use the main induction hypothesis for that term to prove the claim. The cases (λ) and (β) are simple applications of the induction hypothesis.  Qed Corollary. r ⇓. References [AJ01]  Klaus Aehlig and Felix Joachimski. Operational aspects of normalization by evaluation. Sub- mitted, 2001. [Alt93]  Thorsten Altenkirch. A formalization of the strong normalization proof for system F in LEGO. In Bezem and Groote [BG93], pages 13–28. [Bar84]  Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North–Holland, Ams- terdam, second revised edition, 1984. [Ber93]  Ulrich Berger. Program extraction from normalization proofs. In Bezem and Groote [BG93], pages 91–106. [BG93]  Marc Bezem and Jan F. Groote, editors. Typed Lambda Calculi and Applications, volume 664 of Lecture Notes in Computer Science. Springer Verlag, 1993. [Dav95] René David. Une preuve simple de résultats classiques en λ calcul. C.R. Acad. Sci. Paris, t. 320, Série I:1401–1406, 1995. [Dav01] René David. Normalization without reducibility. Annals of Pure and Applied Logic, 107(1– 3):121–130, 2001. [dG99]  Philippe de Groote. On the strong normalisation of natural deduction with permutation- conversions. In Paliath Narendran and Michaël Rusinowitch, editors, Rewriting Techniques and Applications, 10th International Conference, RTA-99, Trento, Italy, July 2-4, 1999, Pro- ceedings, volume 1631 of Lecture Notes in Computer Science, pages 45–59. Springer Verlag, 1999.

[Dil68]  Justus Diller. Zur Berechenbarkeit primitiv-rekursiver Funktionale endlicher Typen. In Kurt Schütte, editor, Contributions to Mathematical Logic, pages 109–120. North–Holland, Ams- terdam, 1968. [Gan80] Robin O. Gandy. An early proof of normalization. In J.P. Seldin and J.R. Hindley, editors, To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, pages 453–455. Academic Press, 1980. [GLT89] Jean-Yves Girard, Yves Lafont, and Paul Taylor. Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989. [Göd58] Kurt Gödel. Über eine bisher noch nicht benützte Erweiterung des finiten Standpunkts. Dialectica, 12:280–287, 1958. [Gog94] Healfdene Goguen. A Typed Operational Semantics for Type Theory. PhD thesis, University of Edinburgh, August 1994. Available as LFCS Report ECS-LFCS-94-304. [Gog95] Healfdene Goguen. Typed operational semantics. In Mariangiola Dezani-Ciancaglini and Gordon Plotkin, editors, Typed Lambda Calculi and Applications, volume 902 of Lecture Notes in Computer Science, pages 186–200. Springer Verlag, 1995. [Gog99] Healfdene Goguen. Soundness of the logical framework for its typed operational semantics. In Jean-Yves Girard, editor, Typed Lambda Calculi and Applications, 4th International Confer- ence, TLCA’99, L’Aquila, Italy, April 7-9, 1999, Proceedings, volume 1581 of Lecture Notes in Computer Science, pages 177–197. Springer Verlag, 1999. [Hin97]  J. Roger Hindley. Basic Simple Type Theory, volume 42 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1997. [How80] W.A. Howard. Ordinal analysis of terms of finite type. The Journal of Symbolic Logic, 45(3):493–504, 1980. [Joa01]  Felix Joachimski. Reduction Properties of ΠIE-Systems. PhD thesis, LMU München, 2001. [Lei75]  Daniel Leivant. Strong normalization for arithmetic (variations on a theme of Prawitz). In J. Diller and G.H. Müller, editors, Proof Theory Symposion Kiel 1974, volume 500 of Lecture Notes in Mathematics, pages 182–197. Springer Verlag, 1975. [Mat98] Ralph Matthes. Extensions of System F by Iteration and Primitive Recursion on Monotone Inductive Types. Dissertation (PhD thesis), Universität München, 1998. SN . Wealways first prove (i) and (ii) in parallel and later infer (iii), possibly with the help

of (ii). xr⃗ [R]. Let S ∈ SN. If [R] is void then xr⃗S ∈ SN simply follows from r⃗, S ∈ SN. Otherwise we may assume that R is a critical elimination of the form (x_{0}.s_{0}, x_{1}.s_{1}). For xr⃗(x_{0}.s_{0}, x_{1}.s_{1})S ∈ SN we need xr⃗(x_{0}.s_{0}S, x_{1}.s_{1}S) ∈ SN and this requires s_{0}S, s_{1}S ∈ SN. But the latter follows from the side induction hypothesis for s_{0} and s_{1} which in case that S is critical applies since they have the same type as xr⃗(x_{0}.s_{0}, x_{1}.s_{1}). In case (i) we do not need this last fact.

Note that in order to use the side induction hypothesis (ii) we always have to check that the

previously generated term in SN has the same (sum) type ρ.

xr⃗(x_{0}.s_{0}, x_{1}.s_{1})T T⃗ ∈ SN has been derived from xr⃗(x_{0}.s_{0}T, x_{1}.s_{1}T)T⃗ ∈ SN. The side induction hypothesis for the latter yields xr⃗(x_{0}.s_{0}T, x_{1}.s_{1}T)T⃗S ∈ SN, so we obtain xr⃗(x_{0}.s_{0}, x_{1}.s_{1})T T⃗S ∈

SN at once.

λxr ∈ SN has been derived from r ∈ SN. Since λxr necessarily has a function type we only have to deal with case (i) and may apply the side induction hypothesis for (iii) in order to conclude

r_{x}[s] ∈ SN. Hence (λxr)s ∈ SN.

(λxr)tT⃗. If S ∈ SN then by the respective side induction hypothesis r_{x}[t]T⃗S ∈ SN, hence (λxr)tT⃗S ∈ SN by (β_{→}).

inj_{i}r ∈ SN is derived from r ∈ SN. Since inj_{i}r has a sum type only case (ii) is possible. The assertion (inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1}) ∈ SN can be obtained from s_{i}[x_{i} := r] ∈ SN using the (β_{+})- rule, and that follows from the main induction hypothesis (iii) since r has a strictly smaller

type than inj_{i}r.

(inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗. Similar to the (β_{→})-case: (inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗ ∈ SN has been inferred from s_{i}[x_{i} := r]S⃗ ∈ SN, s_{1−i}S⃗ ∈ SN and r ∈ SN. Since the first two terms also have type ρ the side induction hypothesis may be applied and yields

s_{i}[x_{i} := r]S⃗S ∈ SN  and  s_{1−i}S⃗S ∈ SN,

so one application of the (β_{+})-rule proves the assertion

(inj_{i}r)(x_{0}.s_{0}, x_{1}.s_{1})S⃗S ∈ SN.

In the proof of (iii) the complicated cases are the variable eliminations (all other cases are covered by the side induction hypothesis).

Case yr⃗ [R]. The side induction hypothesis supplies us with r⃗_{x}[s] ∈ SN and R_{x}[s] ∈ SN.

• If x ≢ y this suffices to conclude (yr⃗ [R])_{x}[s] ∈ SN.

• If x ≡ y and the elimination is empty the claim follows at once from s ∈ SN.

• If not we successively apply s to the substituted eliminations r⃗_{x}[s], using the induction hypothesis for (i) repeatedly at subtypes of ρ, arriving at sr⃗_{x}[s] ∈ SN. If [R] is not void we may assume that R is critical. If, moreover, r⃗ is empty we apply (ii) at type ρ (which already has been proved) in order to conclude that sR_{x}[s] ∈ SN. Otherwise sr⃗_{x}[s] has a subtype of ρ and we apply the induction hypothesis for (ii), obtaining sr⃗_{x}[s]R_{x}[s] ∈ SN. For this to work it is vital that at most the last elimination is critical, because in contrast to →-eliminations the types are not in general lowered by +-eliminations.