IA038 Types and Proofs
5. The Normalization Theorem
Notation:
• −→ . . . one-step reduction, reducing one redex occurence into a contractum within a term
• −→−→ . . . multi-step reduction, zero to any number of single step reductions
• = means (−→ ∪ −→−1
) (or just equality from the denotational semantics)
1
Jiří Zlatuška


March 14, 2023
Uniqueness of the normal form
Reduction −→ satisfies Church-Rosser property (−→ is CR) iff for any M, M1, M2 such that M −→−→ M1
and M −→−→ M2, there is a term M3 such that M1 −→−→ M3 and M2 −→−→ M3.
Diagramatically, the following diagram comutes:
cc
EE
EE
cc
M M1
M2 M3
CR
2
When Church-Rosser property holds true, we have:
When
M = N,
there exists a term Z such that
M −→−→ Z a N −→−→ Z.
The proof follows from the definition of CR by induction on transitivity definition of =:
When M = N follows from M −→−→ N, we can have N ≡ Z.
When M = N follows from N = L and L = M, then by induction assumption (IA) there are terms
Z1 and Z2 such that N −→−→ Z1, L −→−→ Z1 a L −→−→ Z2, M −→−→ Z2. Church-Rosser property now
yields the existence of Z, such that Z1 −→−→ Z and Z2 −→−→ Z.
Proof schema:
d
dd‚
d
dd‚
d
dd‚
d
dd‚
d
dd‚
d
dd‚
 
  ©
 
  ©
 
  ©
 
  ©
 
  ©
 
  ©
IA IA
CR
= =N L M
Z
Z1 Z2
3
Hence Church-Rosser property guarantees for normal forms:
reachability For N being a normal form of M such that M = N, there is M −→−→ N
(When M = N, there is Z s.t. N −→−→ Z and M −→−→ Z, but N is normal, hence Z ≡ N.)
uniqueness For any term, there axists at most one normal form.
(For two normal forms, N1, N2, there is N1 = N2 based on transtivity of =; from CR there exists
a term Z, for which N1 −→−→ Z and N2 −→−→ Z, normality gives N1 ≡ Z and N2 ≡ Z and
thus N1 ≡ N2.)
Property: Reduction in the λ-calculus is CR.
Proving CR means analyzing redex/contractum behavior and development of redexes dusring subsequent
reductions.
4
Weak Church-Rosser property:
c
E
EE
cc
M M1
M2 M3
WCR
5
Just beware of the fact that the definition of CR cannot be simplified to single/step reductions in the
assumption:
CR generally does not follow from WCR when the existence of normal forms is not guaranteed:
The following is and infinite graph of a reduction which is WCR but not CR:
N

s
N0
  ©
N1
g
g‡rrj
N2
  ©ˆˆˆz
N3£
£
£
£ ¨¨%
N4
  ©
N5 g
g
g
g‡ˆˆˆz
N6
dd‚
N7£
£
£
£ $$$W
N8
  ©
N9 g
g
g
g‡ˆˆˆˆz N10
dd‚
N11£
£
£
£
. . .
  ©
. . . gg‡
. . .
6
The weak normalization theorem
Weakly normalizing reduction: for every term there exists a reduction into normal form
Strongly normalizing reduction: Any reduction sequence terminates (with a normal form).
Reduction in the λ-calculus is weakly normalizing.
Proof by Alan Turing (found by Hindley-Seldin in 1980):
Define redex degree for a redex
(λxT1
.PT2
)QT1
as the number of symbols in the type T1.
Typed terms can be ordered by the highers redex degree contained in them, or by highest different degree
of differing redex in case the highest are equal, or by the length of terms in case all redexes are of the
same degree.
Converting (reducing) a redex with the highest order, no other redexes of that order arise. Hence this
reduction lowers the degree, yielding a finite maximum length of any reduction sequence converting
redexes of the highest degree.
7
Strong normalization proof by Gandy:
Define λI-terms based on λ-terms and interpreted by numerical values and functions.
Typed λI-terms are defined as a subset of λ-terms only allowing to form abstractions when bound variable
occurs in the bodz, i.e.
λx.M is a λI-term for M being a λI-term and x a variable only if x ∈ FV(M).
Provide a fixed interpretation of types by a function J assigning J (T) ≡ N, for any atomic type T.
Use monotonic functions defined as a family H:
For every type T define a structure
(HT , <T )
consisting of a set with an ordering:
HT ⊆ J (T)
<T ⊆ HT × HT
as:
(HT , <T ) ≡ (N, <N ), with T atomic type,
HT1→T2
≡ { f ∈ J (T1 → T2) | ∀a, a ∈ HT : fa ∈ HT2
∧
∧(a <T1
a ⇒ fa <T2
fa ) }
f <T1→T2
g iff ∀a ∈ HT1
: fa <T2
ga.
(The initial ordering <N it the less-than relation over natural numbers.)
8
This defines a hierarchy of sets HT as subsets of T containing just monotonic functions preserving the
ordering when applied to arguments).
Property: When λI-terms only use members of HT , they define monotonic functions of its free variables
with members from HT ¿
Let M be a λI-term of type T. For ϕ an interpretation assigning to free variables of M values from H,
then the value
E[[M]]ϕ
is monotonic and belongs to HT .
Proof by induction on the structure of M:
1. For M ≡ x we assumed E[[x]]ϕ ∈ HT is monotonic.
2. For M ≡ M1M2, from the inductive assumption it follows that
E[[M1]]ϕ ∈ HT1→T
and
E[[M2]]ϕ ∈ HT1
,
both monotonic it their free variables.
From the definition of HT1→T it follows
(E[[M1]]ϕ)(E[[M2]]ϕ) ∈ HT
and this is again monotonic function of the free variables from M1M2.
9
3. For M ≡ λx.M1, if follows from the induction assumption,
E[[M1]]ϕ ∈ HT2
for any ϕ , which assigns a value from HT1 to variable x of type T. This means
∀a ∈ HT1 : ( λλxE[[M1]][x ← x]ϕ)a ∈ HT2
and also (because E[[M1]]ϕ is monotonic function of its free variables and x ∈ FV(M1))
∀a, a ∈ HT1
: ( λλxE[[M1]][x ← x]ϕ)a < ( λλxE[[M1]][x ← x]ϕ)a
and so
E[[λx.M]]ϕ ∈ HT
whioch is again monotonic in its free variables.
10
For definition of term norms, define several base functions over natural numbers:
1. For each atomic type T define the following constants:
0T
of type T,
ST of type T → T a
+T of type T → T → T,
interpreted so that
ϕ(0T
) = 0,
ϕ(ST ) = successor function N → N a
ϕ(+T ) = addition function N → N → N (≡ N × N → N).
Applications of contants +T will be written in infix notation,
M +T N
instead of
+T MN.
2. For any types T1, T2 define terms ST1→T2 , +T1→T2 as
ST1→T2 ≡ λfT1→T2
xT1
.ST2 (fx)
and
+T1→T2
≡ λfT1→T2
gT1→T2
xT1
.(fx) +T2
(gx).
11
3. Let T be an atomic type, T1, T2 general types. Define a family of typed terms L as
(a) LT
≡ 0T
(b) LT →T
≡ λxT
.x
(c) L(T1→T2)→T
≡ λfT1→T2
.LT2→T
.fLT1
(d) LT1→(T2→T3)
≡ λxT1
yT2
.(LT1→T3
x) +T3
(LT2→T3
y)
In particular, we have now the constant 0 ∈ N, ther successor function N → N and the addition function
N × N → N, plus an extension of those in all types together with functions LT1→T
, with T atomic,
allowing to project those into natural numbers.
Each of these functions is monotonic and belonging into H:
For any interpretation ϕ and any type T the following can be easily proved:
1. E[[0T
]]ϕ ∈ HT
,
2. E[[ST ]]ϕ ∈ HT →T
,
3. E[[+T ]]ϕ ∈ HT →T →T
,
4. E[[LT
]]ϕ ∈ HT
.
12
Now define a transformation || || mapping terms of any tzpe into a base type (and thus to natural
numbers).
1. x ≡ x, for x a variable.
2. (MN) ≡ M N .
3. (λxT1
.MT2
) ≡ λx.ST1
(M + LT1→T2
x).
13
In order to define || ||, general λ-terms have to be embedded into λI-terms using
?
transformation: For any term M define λI-term M
?
as:
�
A key property: Let M be a redex and N the corresponding contractum, i.e.
M −→−→ N.
Then it holds true
E[[M ]]ϕ > E[[N ]]ϕ,
for any interpretation ϕ.
For proof, take
M ≡ (λx.P)Q
and
N ≡ P[Q/x].
Then
M ≡ (λx.S(P + Lx))Q
≡ (S(P + Lx))[Q /x]
≡ S(P [Q /x] + LQ )
and
N ≡ (P[Q/x])
≡ P [Q /x].
The result follows from monotonicity of λI-terms.
14
Monoonicity of reductions
Let M, N be terms satisfying
Then it holds true
E[[M ]]ϕ > E[[N ]]ϕ.
15
M → N.
Norms of general terms
Transformation || || can now be defined as:
For any term M of type T1 define ||M|| as
||M|| ≡ E[[LT1→T
(M )]]ϕ,
where T is atomic.
Hence for M, N terms satisfying
M −→ N.
it holds true that
||M|| > ||N||.
(By monotonicity of L and the previous result.)
16
Strong normalization of typed λ-terms:
The typed λ-calculus reduction is strongly normalizing.
No infinite sequence of reductions
M −→ M1 −→ M2 −→ · · · −→ · · ·
may exist for any term M because of the monotonicity property: The value of ||M|| is finite, and decreases
after any reduction
M −→ N
so that
||M|| > ||N||.
There is no decreasing infinite sequence of natural numbers starting with ||M||, so also no infinite sequence
of reductions.
The value of ||M|| is uniquely defined for any interpretation ϕ because of CR.
The upper bound for the length of any sequence of reductions starting with M can be given as ||M||.
17
18
19