Uniform Proofs of Normalisation and
Approximation for Intersection Types
Kentaro Kikuchi
RIEC, Tohoku University
Katahira 2-1-1, Aoba-ku, Sendai 980-8577, Japan
kentaro@nue.riec.tohoku.ac.jp

We present intersection type systems in the style of sequent calculus, modifying the systems that
Valentini introduced to prove normalisation properties without using the reducibility method. Our
systems are more natural than Valentini’s ones and equivalent to the usual natural deduction style
systems. We prove the characterisation theorems of strong and weak normalisation through the proposed systems, and, moreover, the approximation theorem by means of direct inductive arguments.
This provides in a uniform way proofs of the normalisation and approximation theorems via type
systems in sequent calculus style.

1

Introduction

A traditional way of proving strong normalisation for typed λ -terms is the reducibility method [20],
which uses set-theoretic comprehension. Other methods without using reducibility have also been studied in the literature (see, e.g. Section 5 of [19] for a review of those methods). Some of them use an
inductive characterisation of strongly normalising λ -terms given by van Raamsdonk and Severi [18].
In [21], Valentini introduced, instead of using the inductive characterisation, an intersection type system that is closed under the rules of the original system, and proved strong normalisation by a simple
induction on the typing derivation.
In this paper we develop Valentini’s approach further providing an improvement on his system and its
extensions with an axiom for the type constant ω . These systems are in the style of sequent calculus and
equivalent to the original intersection type systems in natural deduction style. Using the new systems, we
prove the characterisation theorems of strong and weak normalisation, which are well-known properties
of intersection type systems [17, 8].
Another important point in our approach is that we design new systems that derive the same sequents
as the original natural deduction style systems do, so that we can prove various other properties than
normalisation by simple inductions on the typing derivation (cf. [15]). In the present paper we illustrate
that by showing the approximation theorem for the type system with ω , which is usually proved using
reducibility predicates over a typing context and a type (see, e.g. [11, 4]).
The difference between the systems in [21] and ours is the following. First, some rules of the systems
in [21] have restrictions on types to be type variables. Also, the rule for abstraction takes a form that
implies the η -rule. On the other hand, our systems do not have the restrictions on types, and our rule
for abstraction is the usual one. In this natural setting, we show that our system is closed under the rules
of the original natural deduction style system. This part of the proof of strong normalisation is much
shorter than that in [21]. Secondly, the system characterising weakly normalising λ -terms in [21] does
not have the type constant ω , and is not related to the original natural deduction style system. In this
paper, we introduce new systems with an axiom for the type constant ω , and prove weak normalisation
Jakob Rehof (Ed.): Intersection Types and Related Systems (ITRS)
EPTCS 177, 2015, pp. 10–23, doi:10.4204/EPTCS.177.2

K. Kikuchi

11

of λ -terms that are typable with ω -free types in the original system. The closure under the rules of the
original system is shown by almost the same argument as that in the case of the system without ω .
In [21], only normalisation properties are discussed, and other properties than normalisation are not
proved using the sequent calculus style systems. Some other papers [18, 16, 9, 1] have studied strong
normalisation for terms typable with intersection types without using reducibility. Each of them uses
an inductive characterisation of strongly normalising terms, but any other properties than normalisation
have not been treated. So the present paper seems to be the first to apply a proof method for normalisation
without reducibility to other properties of intersection type systems.
There is also an attempt in [3] to give uniform proofs of the characterisation theorems of normalisation and the approximation theorem. The method is through strong normalisation for reduction on
typing derivations. However, it uses reducibility predicates to prove the strong normalisation, and the
proof seems more complicated than ours.
The organisation of the paper is as follows. In Section 2 we introduce two kinds of intersection type
systems. In Section 3 we prove the characterisation theorem of strong normalisation through the new
type system. In Section 4 we introduce type systems with ω , and prove the characterisation theorem of
weak normalisation. In Section 5 we prove the approximation theorem using one of the new systems
with ω .

2

Intersection type systems

In this section we introduce two intersection type systems: one is in the ordinary natural deduction style
and the other in sequent calculus style. They prove to be equivalent, and both characterise strongly
normalising λ -terms.
First we introduce some basic notions on the λ -calculus [5]. The set Λ of λ -terms is defined by
the grammar: M ::= x | MM | λ x.M where x ranges over a denumerable set of variables. We use letters
x, y, z, . . . for variables and M, N, P, . . . for λ -terms. The notions of free and bound variables are defined
as usual. The set of free variables occurring in a λ -term M is denoted by FV(M). We identify α convertible λ -terms, and use ≡ to denote syntactic equality modulo α -conversion. [ := ] is used for
usual capture-free substitution.
The β -rule is stated as (λ x.M)N → M[x := N], and β -reduction is the contextual closure of the β rule. We use −→β for one-step reduction, and −→∗β for its reflexive transitive closure. A λ -term M is
said to be strongly (weakly) normalising if all (some, respectively) β -reduction sequences starting from
M terminate. The set of strongly (weakly) normalising λ -terms is denoted by SNβ (WNβ , respectively).
The set of types is defined by the grammar: σ ::= ϕ | σ → σ | σ ∩ σ where ϕ ranges over a denumerable set of type variables. We use letters σ , τ , ρ , . . . for arbitrary types. The type assignment systems λ∩

Γ ,x : σ ⊢ x : σ

(Ax)

Γ ,x : σ ⊢ M : τ
(→ I)
Γ ⊢ λ x.M : σ → τ
where x ∈
/Γ

Γ ⊢ M : σ → τ Γ ⊢ N : σ (→ E)
Γ ⊢ MN : τ

Γ ⊢ M : σ Γ ⊢ M : τ (∩ I)
Γ ⊢ M : σ ∩τ

Γ ⊢ M : σ ∩ τ (∩ E)
Γ ⊢M:σ

Γ ⊢ M : σ ∩ τ (∩ E)
Γ ⊢M:τ

Figure 1: Natural deduction style system λ∩

12

Uniform Proofs of Normalisation and Approximation for Intersection Types

Γ , x : σ ⊢s x : σ

(Ax)

Γ ⊢s M[x := N]N1 . . . Nn : σ Γ ⊢s N : τ
(Beta)s
Γ ⊢s (λ x.M)NN1 . . . Nn : σ

Γ ⊢s N : σ1 Γ , y : σ2 ⊢s yN1 . . . Nn : τ
(L →)
Γ , x : σ1 → σ2 ⊢s xNN1 . . . Nn : τ
where y ∈
/ FV(N1 ) ∪ · · · ∪ FV(Nn ) and y ∈
/Γ
Γ , x : σ1 , x : σ2 ⊢s xN1 . . . Nn : τ
(L ∩)
Γ , x : σ1 ∩ σ2 ⊢s xN1 . . . Nn : τ

Γ , x : σ ⊢s M : τ
(R →)
Γ ⊢s λ x.M : σ → τ
where x ∈
/Γ

Γ ⊢s M : σ Γ ⊢s M : τ
(R ∩)
Γ ⊢s M : σ ∩ τ

Figure 2: Sequent calculus style system λ∩s
and λ∩s are defined by the rules in Figures 1 and 2, respectively. A typing context is defined as a finite set
of pairs {x1 : σ1 , . . . , xn : σn } where the variables are pairwise distinct in the system λ∩ while they may
be the same in the system λ∩s . A variable with different types is intended to have the type of intersection
of all of them. The typing context Γ , x : σ denotes the union Γ ∪ {x : σ }, and x ∈
/ Γ means that x does not
appear in Γ , i.e., for no type σ , x : σ ∈ Γ . Note that x : σ ∈ Γ is possible in the typing context Γ , x : σ .
In particular, the premisses of the rule (L →) may have x : σ1 → σ2 in Γ . In that case, x : σ1 → σ2 is
introduced by the rule (L →) with implicit contraction.
The system in [21] has the restriction in λ∩s that the type σ in the rules (Ax) and (Beta)s and the type
τ in the rules (L →) and (L ∩) must be type variables. Also, the rule (R →) takes the following form:

Γ , x : σ ⊢s Mx : τ
Γ ⊢s M : σ → τ
where x ∈
/ Γ and x ∈
/ FV(M), so that the system includes the η -rule and is not equivalent to the system
λ∩ . (For example, ⊢s λ x.x : (σ → τ ) → ((ρ ∩ σ ) → τ ) is derivable in the system of [21], but ⊢ λ x.x :
(σ → τ ) → ((ρ ∩ σ ) → τ ) is not derivable in λ∩ .)
Example 2.1. Self-application can now be typed naturally in λ∩s , as follows (cf. [21, pp. 478–479]).
x : σ ⊢s x : σ x : σ , y : τ ⊢s y : τ
(L →)
x : σ , x : σ → τ ⊢s xx : τ
(L ∩)
x : σ ∩ (σ → τ ) ⊢s xx : τ
(R →)
⊢s λ x.xx : (σ ∩ (σ → τ )) → τ
The (Beta)s -free part of the system λ∩s types exactly the terms in β -normal form, and any β -redex in
a typed term must be constructed through the rule (Beta)s . So it is immediately seen that the terms that
are not head-normalising (e.g. (λ x.xx)(λ x.xx)) can not be typed in the system λ∩s .
Proposition 2.2. Γ , x : σ1 ∩ σ2 ⊢s M : τ if and only if Γ , x : σ1 , x : σ2 ⊢s M : τ .
Proof. By induction on the derivations.
Henceforth we write Γ∩ for the typing context in which each variable has the type of intersection of
all the types that the variable has in Γ .

K. Kikuchi

3

13

Characterisation of strongly normalising λ -terms

If one tries to prove strong normalisation for terms typed in the system λ∩ directly by induction on
derivations, a difficulty arises in the case of the rule (→ E). One way of overcoming this difficulty is
to use reducibility predicates [20]. Here we use the sequent calculus style system λ∩s instead. For the
system λ∩s , we can prove strong normalisation for typed terms directly by induction on derivations.
Theorem 3.1. If Γ ⊢s M : σ then M ∈ SNβ .
Proof. By induction on the derivation of Γ ⊢s M : τ in λ∩s . The only problematic case is where the last
rule applied is (Beta)s . In that case, by the induction hypothesis, we have M[x := N]N1 . . . Nn ∈ SNβ and
N ∈ SNβ . From the former we have M, N1 , . . . , Nn ∈ SNβ . Then any infinite reduction sequence starting
from (λ x.M)NN1 . . . Nn must have the form
(λ x.M)NN1 . . . Nn −→β∗
−→β
−→β

(λ x.M ′ )N ′ N1′ . . . Nn′
M ′ [x := N ′ ]N1′ . . . Nn′
...

where M−→β∗ M ′ , N−→β∗ N ′ and Ni −→∗β Ni′ for i ∈ {1, . . . , n}. But then there is an infinite reduction
sequence
M[x := N]N1 . . . Nn −→β∗ M ′ [x := N ′ ]N1′ . . . Nn′
−→β . . .
contradicting the hypothesis. Hence (λ x.M)NN1 . . . Nn ∈ SNβ .
To complete a proof of strong normalisation for terms typed in the system λ∩ , what remains to be
shown is that if M is typable in λ∩ then it is typable in λ∩s . This is proved using several lemmas below.
First we show that λ∩s is closed under the weakening rule.
Lemma 3.2. If Γ ⊢s M : τ then Γ , x : σ ⊢s M : τ .
Proof. By induction on the derivation of Γ ⊢s M : τ .
The next two lemmas are the essential difference from the proof of [21]. These are used in the proof
of Lemma 3.5 below. The simply typed counterpart of Lemma 3.3 is found in the second proof of strong
normalisation for the simply typed λ -calculus in [12].
Lemma 3.3. If Γ ⊢s M : σ → τ and x ∈
/ Γ then Γ , x : σ ⊢s Mx : τ .
Proof. By induction on the derivation of Γ ⊢s M : σ → τ . Here we show a few cases.
•

•

(Ax)
Γ , y : σ → τ ⊢s y : σ → τ
In this case we take two axioms Γ , x : σ ⊢s x : σ and Γ , x : σ , z : τ ⊢s z : τ , and obtain Γ , x : σ , y :
σ → τ ⊢s yx : τ by an instance of the (L →) rule.

Γ ⊢s M[y := N]N1 . . . Nn : σ → τ Γ ⊢s N : ρ
(Beta)s
Γ ⊢s (λ y.M)NN1 . . . Nn : σ → τ
By the induction hypothesis, we have Γ , x : σ ⊢s M[y := N]N1 . . . Nn x : τ , and by Lemma 3.2, we
have Γ , x : σ ⊢s N : ρ . From these, we obtain Γ , x : σ ⊢s (λ y.M)NN1 . . . Nn x : τ by an instance of
the (Beta)s rule.

Uniform Proofs of Normalisation and Approximation for Intersection Types

14

•

Γ , y : σ ⊢s M : τ
(R →)
Γ ⊢s λ y.M : σ → τ
where y ∈
/ Γ . From Γ , y : σ ⊢s M : τ , we have Γ , x : σ ⊢s M[y := x] : τ . From this and the axiom
Γ , x : σ ⊢s x : σ , we obtain Γ , x : σ ⊢s (λ y.M)x : τ by an instance of the (Beta)s rule.

Lemma 3.4. If Γ ⊢s M : σ ∩ τ then Γ ⊢s M : σ and Γ ⊢s M : τ .
Proof. By induction on the derivation of Γ ⊢s M : σ ∩ τ .
Now we are in a position to prove the following important lemma.
Lemma 3.5. λ∩s is closed under substitution, i.e., if Γ , x : σ1 , . . . , x : σm ⊢s P : τ where x ∈
/ Γ , m ≥ 0 and
σi 6= σ j for i 6= j, and, for any i ∈ {1, . . . , m}, Γ ⊢s N : σi , then Γ ⊢s P[x := N] : τ .
Proof. The proof is by main induction on the number of ‘→’ and ‘∩’ occurring in σ1 , . . . , σm and subinduction on the length of the derivation of Γ , x : σ1 , . . . , x : σm ⊢s P : τ . We proceed by case analysis
according to the last rule used in the derivation of Γ , x : σ1 , . . . , x : σm ⊢s P : τ . Here we consider a few
cases.
• Suppose the last rule in the derivation is

Γ , x : σ ⊢s M[y := Q]N1 . . . Nn : τ Γ , x : σ ⊢s Q : ρ
(Beta)s
Γ , x : σ ⊢s (λ y.M)QN1 . . . Nn : τ
where x : σ = x : σ1 , . . . , x : σm . By the subinduction hypothesis, we obtain both

Γ ⊢s M[y := Q][x := N]N1 [x := N] . . . Nn [x := N] : τ
and

Γ ⊢s Q[x := N] : ρ

Since y is a bound variable, we can assume that it does not occur in N. Hence the first judgement
is
Γ ⊢s M[x := N][y := Q[x := N]]N1 [x := N] . . . Nn [x := N] : τ
From this and Γ ⊢s Q[x := N] : ρ , we obtain

Γ ⊢s (λ y.M[x := N])Q[x := N]N1 [x := N] . . . Nn [x := N] : τ
by an instance of the (Beta)s rule.
• Suppose the last rule in the derivation is

Γ , x : σ ⊢s M : ρ1 Γ , x : σ , y : ρ2 ⊢s yN1 . . . Nn : τ
(L →)
Γ , x : σ , x : ρ1 → ρ2 ⊢s xMN1 . . . Nn : τ
/ FV(N1 ) ∪ · · · ∪ FV(Nn ) and y ∈
/ Γ , x : σ . By
where {x : σ , x : ρ1 → ρ2 } = {x : σ1 , . . . , x : σm }, y ∈
the subinduction hypothesis, we obtain both

Γ ⊢s M[x := N] : ρ1

(1)

Γ , y : ρ2 ⊢s (yN1 . . . Nn )[x := N] : τ

(2)

and

K. Kikuchi

15

Now consider the assumption Γ ⊢s N : ρ1 → ρ2 and a fresh variable z. Then by Lemma 3.3, we
have Γ , z : ρ1 ⊢s Nz : ρ2 . From this and (1), we have Γ ⊢s NM[x := N] : ρ2 by the main induction
hypothesis. Then, again by the main induction hypothesis, we obtain

Γ ⊢s NM[x := N]N1 [x := N] . . . Nn [x := N] : τ
from (2) and Γ ⊢s NM[x := N] : ρ2 .
• Suppose the last rule in the derivation is

Γ , x : σ , x : ρ1 , x : ρ2 ⊢s xN1 . . . Nn : τ
(L ∩)
Γ , x : σ , x : ρ1 ∩ ρ2 ⊢s xN1 . . . Nn : τ
where {x : σ , x : ρ1 ∩ ρ2 } = {x : σ1 , . . . , x : σm }. Then, applying Proposition 2.2 to the conclusion,
we have Γ , (x : σ )′ , x : ρ1 , x : ρ2 ⊢s xN1 . . . Nn : τ where (x : σ )′ = x : σ \ {x : ρ1 ∩ ρ2 }. Now, from
the assumption Γ ⊢s N : ρ1 ∩ ρ2 , we have Γ ⊢s N : ρ1 and Γ ⊢s N : ρ2 by Lemma 3.4. Hence, by
the main induction hypothesis, we obtain Γ ⊢s NN1 [x := N] . . . Nn [x := N] : τ .
Now we can show that the system λ∩s is closed under the (→ E) rule.
Lemma 3.6. If Γ ⊢s M : σ → τ and Γ ⊢s N : σ then Γ ⊢s MN : τ .
Proof. By Lemma 3.3, we have Γ , x : σ ⊢s Mx : τ for any fresh variable x. Hence by the previous lemma,
we obtain Γ ⊢s (Mx)[x := N] ≡ MN : τ .
Now we can prove the announced theorem.
Theorem 3.7. If Γ ⊢ M : σ then Γ ⊢s M : σ .
Proof. By induction on the derivation of Γ ⊢ M : σ in λ∩ , using Lemmas 3.4 and 3.6.
The converse of this theorem also holds when typing contexts are restricted to those of λ∩ . To prove
it, we need some lemmas on properties of the system λ∩ .
Lemma 3.8. If Γ ⊢ M : τ and z ∈
/ Γ then Γ , z : σ ⊢ M : τ .
Proof. By induction on the derivation of Γ ⊢ M : τ .
Lemma 3.9. λ∩ is closed under substitution, i.e., if Γ , x : σ ⊢ P : τ where x ∈
/ Γ and Γ ⊢ N : σ then
Γ ⊢ P[x := N] : τ .
Proof. By induction on the derivation of Γ , x : σ ⊢ P : τ .
Next we prove a Generation Lemma. For its statement we define a preorder on types.
Definition 3.10. The relation ≤ on types is defined by the following axioms and rules:
1. σ ≤ σ

3. σ ≤ τ , τ ≤ ρ ⇒ σ ≤ ρ

2. σ ∩ τ ≤ σ , σ ∩ τ ≤ τ

4. σ ≤ τ , σ ≤ ρ ⇒ σ ≤ τ ∩ ρ

Lemma 3.11. If Γ ⊢ M : σ and σ ≤ τ then Γ ⊢ M : τ .
Proof. By induction on the definition of σ ≤ τ .

16

Uniform Proofs of Normalisation and Approximation for Intersection Types

Lemma 3.12 (Generation Lemma).
1. Γ ⊢ MN : σ if and only if there exist σ1 , . . . , σn , τ1 , . . . , τn (n ≥ 1) such that σ1 ∩ · · · ∩ σn ≤ σ and,
for all i ∈ {1, . . . , n}, Γ ⊢ M : τi → σi and Γ ⊢ N : τi .
2. Γ ⊢ λ x.M : σ if and only if there exist τ1 , . . . , τn , ρ1 , . . . , ρn (n ≥ 1) such that (τ1 → ρ1 )∩ · · ·∩ (τn →
ρn ) ≤ σ and, for all i ∈ {1, . . . , n}, Γ , x : τi ⊢ M : ρi .
Proof. The implications from right to left are immediate by the typing rules and Lemma 3.11. The
converses are shown by induction on the derivations.
Now we can prove a crucial lemma about type-checking in the system λ∩ .
/ Γ then there exists a type ρ such that
Lemma 3.13. If Γ ⊢ M[x := N] : σ and Γ ⊢ N : τ where x ∈
Γ , x : ρ ⊢ M : σ and Γ ⊢ N : ρ .
Proof. By induction on the structure of M, using Lemma 3.12.
We are now ready to prove the equivalence between the systems λ∩s and λ∩ .
Theorem 3.14. Γ ⊢s M : σ if and only if Γ∩ ⊢ M : σ .
Proof. The implication from right to left follows from Theorem 3.7 and Proposition 2.2. The converse
is shown by induction on the derivation of Γ ⊢s M : σ . If the last applied rule is (Beta)s , we use Lemmas 3.12 and 3.13.
Finally we show that all strongly normalising terms are typable in λ∩s .

Theorem 3.15. If M ∈ SNβ then there exist a typing context Γ and a type σ such that Γ ⊢s M : σ .
Proof. The proof is by main induction on the maximal length of all β -reduction sequences starting from
M and subinduction on the structure of M. We analyse the possible cases according to the shape of the
term M.
• M ≡ x for some variable x. In this case we just have to take x : σ ⊢s x : σ , which is an axiom.
• M ≡ xN1 . . . Nn . By the subinduction hypothesis, for any i ∈ {1, . . . , n}, there exist a typing context
Γi and a type σi such that Γi ⊢s Ni : σi . Then consider the following derivation (recall that λ∩s is
closed under the weakening rule):
∪Γi ⊢s Nn : σn ∪Γi, yn : τ ⊢s yn : τ
(L →)
∪Γi, yn−1 : σn →. τ ⊢s yn−1 Nn : τ
..
.
∪Γi ⊢s N2 : σ2 ∪Γi, y2 : σ3 → · · · → σn → τ ⊢s y2 N3 . . . Nn : τ
(L →)
∪Γi ⊢s N1 : σ1
∪Γi , y1 : σ2 → · · · → σn → τ ⊢s y1 N2 . . . Nn : τ
(L →)
∪Γi , x : σ1 → · · · → σn → τ ⊢s xN1 . . . Nn : τ
• M ≡ λ x.P. By the subinduction hypothesis, there exist a typing context Γ and a type σ such that
Γ , x : σ1 , . . . , x : σn ⊢s P : σ where x ∈
/ Γ and n ≥ 0. Then we have Γ ⊢s λ x.P : σ1 ∩ · · · ∩ σn → σ
by the (L ∩) and (R →) rules. (We use a weakening rule instead of (L ∩) when n = 0.)
• M ≡ (λ x.P)NN1 . . . Nn . By the main induction hypothesis, there exist a typing context Γ1 and a
type σ1 such that Γ1 ⊢s P[x := N]N1 . . . Nn : σ1 , and, by the subinduction hypothesis, there exist a
typing context Γ2 and a type σ2 such that Γ2 ⊢s N : σ2 . Then, by the weakening and (Beta)s rules,
we obtain Γ1 , Γ2 ⊢s (λ x.P)NN1 . . . Nn : σ1 .

K. Kikuchi

17

It is interesting to note that in the above proof we do not use the (R ∩) rule at all, so it is redundant
for characterising the strongly normalising λ -terms. The absence of the (R ∩) rule leads to a restriction
on types that is similar to those investigated in [2].
The results in this section are summarised as follows.
Corollary 3.16. For any λ -term M, the following are equivalent.
1. M is typable in λ∩ .
2. M is typable in λ∩s .
3. M is strongly normalising.
4. M is typable in λ∩s without using the (R ∩) rule.
Proof. (1 ⇒ 2) This follows from Theorem 3.7.
(2 ⇒ 3) This follows from Theorem 3.1.
(3 ⇒ 4) This follows from the proof of Theorem 3.15.
(4 ⇒ 2) This is trivial.
(2 ⇒ 1) This follows from Theorem 3.14.

4

Characterisation of weakly normalising λ -terms

In this section we are concerned with weak normalisation and some type systems obtained by extending
the systems λ∩ and λ∩s . The main goal of this section is to prove the characterisation theorem of weak
normalisation in a similar way to that of strong normalisation in the previous section.
The extended systems are listed in Figure 3. First we introduce a new rule (Beta)l , which is a
general form of the rule considered in [21] (σ is restricted to type variables in [21]). Then the system λ∩l
is obtained from λ∩s by replacing the (Beta)s rule by the (Beta)l rule. The systems λ∩ω , λ∩s ω and λ∩l ω
are obtained from λ∩ , λ∩s and λ∩l , respectively, by adding the type constant ω and the (ω ) rule. In order
to distinguish the judgements of the systems, we use the symbols ⊢l , ⊢ω , ⊢sω and ⊢lω .
For the system λ∩l , we have the following theorem.
Theorem 4.1. If Γ ⊢l M : σ then M ∈ WNβ .
Proof. By induction on the derivation of Γ ⊢l M : τ .

Γ ⊢ M[x := N]N1 . . . Nn : σ
(Beta)l
Γ ⊢ (λ x.M)NN1 . . . Nn : σ

λ∩l
λ∩ω
λ∩s ω
λ∩l ω

λ∩s − (Beta)s + (Beta)l

:=
:= λ∩ + (ω )
:= λ∩s + (ω )
:= λ∩l + (ω )

Γ ⊢M:ω

(ω )

Notation
Γ ⊢l M : σ
Γ ⊢ω M : σ
Γ ⊢ sω M : σ
Γ ⊢lω M : σ

Figure 3: Systems extended with ω

18

Uniform Proofs of Normalisation and Approximation for Intersection Types

For characterisation of weak normalisation in terms of typability in the extended systems, it is necessary to clarify the relationship among them. First we show that the terms typable in the ordinary natural
deduction style system λ∩ω are typable in λ∩s ω , in almost the same way as in the previous section.
Theorem 4.2. If Γ ⊢ω M : σ then Γ ⊢sω M : σ .
Proof. It is easy to see that Lemmas 3.2 through 3.6 hold for λ∩s ω instead of λ∩s . Then the theorem
follows by induction on the derivation of Γ ⊢ω M : σ in λ∩ω .
Next we relate the systems λ∩s ω , λ∩l ω and λ∩l . This completes one direction of the characterisation
theorem of weak normalisation.
Lemma 4.3. Γ ⊢sω M : σ if and only if Γ ⊢lω M : σ .
Proof. The implication from left to right is immediate by forgetting the right premiss of (Beta)s . For
the converse, observe that the (Beta)l rule is derivable in λ∩s ω using the rules (Beta)s and (ω ).
Lemma 4.4. Suppose σ and all types in Γ are ω -free. Then Γ ⊢lω M : σ if and only if Γ ⊢l M : σ .
Proof. The implication from right to left is trivial. For the converse, observe that every type occurring
in the derivation of Γ ⊢lω M : σ also occurs in Γ or σ .
Corollary 4.5. If Γ ⊢ω M : σ where σ and all types in Γ are ω -free, then M ∈ WNβ .
Proof. By Theorem 4.2, Lemmas 4.3 and 4.4, and Theorem 4.1.
Conversely, if a λ -term M is weakly normalising, then there exist a typing context Γ and a type σ ,
both ω -free, such that Γ ⊢ω M : σ . To prove this, we need the following lemmas on properties of the
system λ∩ω . These are shown in similar ways to the proofs of Lemmas 3.8 through 3.12.
Lemma 4.6. If Γ ⊢ω M : τ and z ∈
/ Γ then Γ , z : σ ⊢ω M : τ .
Lemma 4.7. λ∩ is closed under substitution, i.e., if Γ , x : σ ⊢ω P : τ where x ∈
/ Γ and Γ ⊢ω N : σ then
Γ ⊢ω P[x := N] : τ .
Definition 4.8. The relation ≤ω on types is defined by the axioms and rules in Definition 3.10 together
with the axiom σ ≤ω ω .
Lemma 4.9. If Γ ⊢ω M : σ and σ ≤ω τ then Γ ⊢ω M : τ .
Lemma 4.10 (Generation Lemma). Let σ be any type with ω 6≤ω σ . Then
1. Γ ⊢ω MN : σ if and only if there exist σ1 , . . . , σn , τ1 , . . . , τn (n ≥ 1) such that σ1 ∩ · · · ∩ σn ≤ω σ
and, for all i ∈ {1, . . . , n}, Γ ⊢ω M : τi → σi and Γ ⊢ω N : τi .
2. Γ ⊢ω λ x.M : σ if and only if there exist τ1 , . . . , τn , ρ1 , . . . , ρn (n ≥ 1) such that (τ1 → ρ1 ) ∩ · · · ∩
(τn → ρn ) ≤ω σ and, for all i ∈ {1, . . . , n}, Γ , x : τi ⊢ω M : ρi .
Now we can prove a crucial lemma about type-checking in the system λ∩ω .

K. Kikuchi

19

Lemma 4.11. If Γ ⊢ω M[x := N] : σ where x ∈
/ Γ then there exists a type ρ such that Γ , x : ρ ⊢ω M : σ
and Γ ⊢ω N : ρ .
Proof. By induction on the structure of M, using Lemma 4.10. If M ≡ y(6≡ x) or ω ≤ω σ , then we take
ρ = ω.
We can now prove that in the system λ∩ω , types are preserved under the inverse of β -reduction.
Lemma 4.12. If Γ ⊢ω N : σ and M −→β N then Γ ⊢ω M : σ .
Proof. By induction on the structure of M, using Lemma 4.10. If M is the β -redex then we use
Lemma 4.11.
Now we can prove the announced theorem.
Theorem 4.13. If M ∈ WNβ then there exist a typing context Γ and a type σ such that Γ ⊢ω M : σ and
both Γ and σ are ω -free.
Proof. Let M ′ be a normal form of M. By Theorem 3.15, every normal form is typable in λ∩s , so there
exist a typing context Γ and a type σ , both ω -free, such that Γ ⊢ω M ′ : σ . Hence, by Lemma 4.12, we
have Γ ⊢ω M : σ .
We can also prove the equivalence of the systems λ∩ω , λ∩s ω and λ∩l ω .
Theorem 4.14. For any typing context Γ , any λ -term M and any type σ , the following are equivalent.
1. Γ∩ ⊢ω M : σ .
2. Γ ⊢sω M : σ .
3. Γ ⊢lω M : σ .
Proof. (1 ⇒ 2) This follows from Theorem 4.2 and Proposition 2.2 with ⊢sω instead of ⊢s .
(2 ⇒ 3) This follows from Lemma 4.3.
(3 ⇒ 1) This follows by induction on the length of the derivation of Γ ⊢lω M : σ . If the last applied rule
is (Beta)l , we use Lemmas 4.10 and 4.11.
The results in this section are summarised as follows.
Corollary 4.15. For any λ -term M, the following are equivalent.
1. Γ ⊢ω M : σ for some typing context Γ and type σ , both ω -free.
2. Γ ⊢sω M : σ for some typing context Γ and type σ , both ω -free.
3. Γ ⊢lω M : σ for some typing context Γ and type σ , both ω -free.
4. Γ ⊢l M : σ for some typing context Γ and type σ .
5. M is weakly normalising.
Proof. (1 ⇒ 2) This follows from Theorem 4.2.
(2 ⇒ 3) This follows from Lemma 4.3.
(3 ⇒ 4) This follows from Lemma 4.4.
(4 ⇒ 5) This follows from Theorem 4.1.
(5 ⇒ 1) This follows from Theorem 4.13.

Uniform Proofs of Normalisation and Approximation for Intersection Types

20

5

Application to other properties

The sequent calculus style systems we introduced in the previous sections are very useful for proving
properties of intersection type systems. In this section we illustrate that by giving a simple proof of the
(logical) approximation theorem, a property that is usually proved using reducibility predicates parametrised by typing contexts (see, e.g. [11, 4]). Proofs of some other properties through the sequent
calculus style systems are found in [15], which also makes a comparison between general conditions for
applying the reducibility method and our approach.
For the statement of the approximation theorem, we introduce some preliminary definitions. The
set of λ ⊥-terms [5] is obtained by adding the constant ⊥ to the formation rules of λ -terms. The type
systems in the previous section are extended to those for λ ⊥-terms, where any λ ⊥-term containing ⊥ is
typable by the (ω ) rule.
Definition 5.1. The approximation mapping α from λ -terms to λ ⊥-terms is defined inductively by

α (λ x1 . . . xn .xN1 . . . Nm ) := λ x1 . . . xn .xα (N1 ) . . . α (Nm )
α (λ x1 . . . xn .(λ x.M)NN1 . . . Nm ) := λ x1 . . . xn .⊥
where n, m ≥ 0.
Lemma 5.2.
1. If Γ ⊢lω α (M) : σ and M−→∗β N then Γ ⊢lω α (N) : σ .
2. Let M−→β∗ N, M−→∗β N ′ , Γ ⊢lω α (N) : σ and Γ ⊢lω α (N ′ ) : τ . Then there exists N ′′ such that
M−→∗β N ′′ and Γ ⊢lω α (N ′′ ) : σ ∩ τ .
Proof. The first part is proved by induction on the derivation of Γ ⊢lω α (M) : σ . For the second part,
we use confluence of β -reduction.
Now the logical approximation theorem can be formulated as follows.
Theorem 5.3. Γ ⊢ω M : σ if and only if there exists M ′ such that M−→β∗ M ′ and Γ ⊢ω α (M ′ ) : σ .
Proof. (⇒) By Theorem 4.14, it suffices to show that if Γ ⊢lω M : σ then there exists M ′ such that
M−→β∗ M ′ and Γ ⊢lω α (M ′ ) : σ . The proof is by induction on the derivation of Γ ⊢lω M : σ . Here we
consider some cases.
Γ ⊢lω M[x := N]N1 . . . Nn : σ
•
(Beta)l
Γ ⊢lω (λ x.M)NN1 . . . Nn : σ
By the induction hypothesis, there exists M ′ such that M[x := N]N1 . . . Nn −→∗β M ′ and Γ ⊢lω
α (M ′) : σ . This M ′ also satisfies (λ x.M)NN1 . . . Nn −→∗β M ′ .
•

Γ ⊢lω N : σ1 Γ , y : σ2 ⊢lω yN1 . . . Nn : τ
(L →)
Γ , x : σ1 → σ2 ⊢lω xNN1 . . . Nn : τ
where y ∈
/ FV(N1 )∪ · · · ∪ FV(Nn ) and y ∈
/ Γ . By the induction hypothesis, there exist N ′ , N1′ , . . . , Nn′
′
∗
′
∗
such that N−→β N , Ni −→β Ni , Γ ⊢lω α (N ′ ) : σ1 and Γ , y : σ2 ⊢lω yα (N1′ ) . . . α (Nn′ ) : τ . Hence,
by an instance of the (L →) rule, we obtain Γ , x : σ1 → σ2 ⊢lω xα (N ′ )α (N1′ ) . . . α (Nn′ ) : τ . So we
take xN ′ N1′ . . . Nn′ as M ′ .

K. Kikuchi

•

21

Γ , x : σ ⊢lω N : τ
(R →)
Γ ⊢lω λ x.N : σ → τ
where x ∈
/ Γ . By the induction hypothesis, there exists N ′ such that N−→∗β N ′ and Γ , x : σ ⊢lω
α (N ′) : τ . By an instance of the (R →) rule, we obtain Γ ⊢lω λ x.α (N ′ ) : σ → τ . Since α (λ x.N ′ ) ≡
λ x.α (N ′ ), we take λ x.N ′ as M ′ .

•

Γ ⊢lω M : σ Γ ⊢lω M : τ
(R ∩)
Γ ⊢lω M : σ ∩ τ
By the induction hypothesis, there exist M1 , M2 such that M−→β∗ M1 , M−→∗β M2 , Γ ⊢lω α (M1 ) : σ
and Γ ⊢lω α (M2 ) : τ . Then by Lemma 5.2(2), there exists M ′ such that M−→∗β M ′ and Γ ⊢lω
α (M ′) : σ ∩ τ .

(⇐) We can show by induction on the derivation that if Γ ⊢ω α (M ′ ) : σ then Γ ⊢ω M ′ : σ . Hence, by
Lemma 4.12, we have Γ ⊢ω M : σ .
Thus our method has been successfully applied to proving the approximation theorem for the mapping α and the system λ∩ω . It is work in progress to give similar proofs of the approximation theorems
for the η -approximation mapping αη , which maps λ x.⊥ directly to ⊥, and type systems with various
preorders as discussed in [10, 11, 4].

6

Conclusion

We have presented uniform proofs of the characterisation theorems of normalisation properties and the
approximation theorem. The proofs have been given via intersection type systems in sequent calculus
style. As investigated in [15], our method can be considered to have embedded certain conditions for
applying reducibility directly into the typing rules of the sequent calculus style systems. (See [13] for a
recent survey of general conditions for applying the reducibility method.)
As mentioned in the introduction, there are some proofs [18, 16, 9, 1] of strong normalisation for
terms typable with intersection types without using reducibility, but they have not considered any other
properties than normalisation. Other syntactic proofs of strong normalisation for terms typable with
intersection types are found in [14, 6], where the problem is reduced to that of weak normalisation with
respect to another calculus or to another notion of reduction. The proofs of [18, 21] and ours are different
from those of [14, 6] in that strong normalisation is proved directly rather than inferring it from weak
normalisation. Yet another syntactic proof [7] uses a translation from terms typable with intersection
types into simply typed λ -terms.
There are many directions for future work. In addition to the one indicated at the last paragraph of
Section 5, it would be worth investigating the type inference and the inhabitation problems for intersection types by means of our sequent calculus style systems.
Acknowledgements I would like to thank Katsumasa Ishii for drawing my attention to Valentini’s paper
and pointing out that the system includes the η -rule. I also thank the anonymous reviewers of ITRS
2014 workshop for valuable comments. The figures of the derivations have been produced with Makoto
Tatsuta’s proof.sty macros.

22

Uniform Proofs of Normalisation and Approximation for Intersection Types

References
[1] Andreas Abel (2007): Syntactical strong normalization for intersection types with term rewriting rules. In:
Proceedings of HOR’07, pp. 5–12.
[2] Steffen van Bakel (1992): Complete restrictions of the intersection type discipline. Theoretical Computer
Science 102, pp. 135–163, doi:10.1016/0304-3975(92)90297-S.
[3] Steffen van Bakel (2004): Cut-elimination in the strict intersection type assignment system is strongly normalizing. Notre Dame Journal of Formal Logic 45, pp. 35–63, doi:10.1305/ndjfl/1094155278.
[4] Henk Barendregt, Wil Dekkers & Richard Statman (2013): Lambda Calculus with Types. Cambridge University Press, doi:10.1017/CBO9781139032636.
[5] Henk P. Barendregt (1984): The Lambda Calculus: Its Syntax and Semantics, revised edition. North-Holland,
Amsterdam.
[6] Gerard Boudol (2003): On strong normalization in the intersection type discipline. In: Proceedings of TLCA’03, Lecture Notes in Computer Science 2701, Springer-Verlag, pp. 60–74, doi:10.1007/
3-540-44904-3_5.
[7] Antonio Bucciarelli, Adolfo Piperno & Ivano Salvo (2003): Intersection types and λ -definability. Mathematical Structures in Computer Science 13, pp. 15–53, doi:10.1017/S0960129502003833.
[8] Mario Coppo, Mariangiola Dezani-Ciancaglini & Betti Venneri (1981): Functional characters of solvable
terms. Zeitschrift für Mathematische Logik und Grundlagen der Mathematik 27, pp. 45–58, doi:10.1002/
malq.19810270205.
[9] René David (2001): Normalization without reducibility. Annals of Pure and Applied Logic 107, pp. 121–130,
doi:10.1016/S0168-0072(00)00030-0.
[10] Mariangiola Dezani-Ciancaglini, Elio Giovannetti & Ugo de’Liguoro (1998): Intersection types, λ -models,
and Böhm trees. In: Theories of Types and Proofs, MSJ Memoirs 2, Mathematical Society of Japan, Tokyo,
pp. 45–97.
[11] Mariangiola Dezani-Ciancaglini, Furio Honsell & Yoko Motohama (2001): Approximation theorems for
intersection type systems. Journal of Logic and Computation 11, pp. 395–417, doi:10.1093/logcom/11.
3.395.
[12] Felix Joachimski & Ralph Matthes (2003): Short proofs of normalization for the simply-typed λ -calculus,
permutative conversions and Gödel’s T. Archive for Mathematical Logic 42, pp. 59–87, doi:10.1007/
s00153-002-0156-9.
[13] Fairouz Kamareddine, Vincent Rahli & Joe B. Wells (2012): Reducibility proofs in the λ -calculus. Fundamenta Informaticae 121, pp. 121–152, doi:10.3233/FI-2012-773.
[14] Assaf J. Kfoury & Joe B. Wells (1995): New notions of reduction and non-semantic proofs of strong β normalization in typed λ -calculi. In: Proceedings of LICS’95, IEEE Computer Society Press, pp. 311–321,
doi:10.1109/LICS.1995.523266.
[15] Kentaro Kikuchi (2009): On general methods for proving reduction properties of typed lambda terms. In:
Proof theoretical study of the structure of logic and computation, RIMS Kôkyûroku 1635, pp. 33–50. Available at http://hdl.handle.net/2433/140464. (Unrefereed proceedings).
[16] Ralph Matthes (2000): Characterizing strongly normalizing terms of a λ -calculus with generalized applications via intersection types. In: Proceedings of ICALP Satellite Workshops 2000, Carleton Scientific, pp.
339–354.
[17] Garrel Pottinger (1980): A type assignment for the strongly normalizable λ -terms. In: To H. B. Curry: Essays
on Combinatory Logic, Lambda Calculus and Formalism, Academic Press, London, pp. 561–577.
[18] Femke van Raamsdonk & Paula Severi (1995): On normalisation. Technical Report CS-R9545, CWI.
[19] Femke van Raamsdonk, Paula Severi, Morten Heine B. Sørensen & Hongwei Xi (1999): Perpetual reductions
in λ -calculus. Information and Computation 149, pp. 173–225, doi:10.1006/inco.1998.2750.

K. Kikuchi

23

[20] William W. Tait (1967): Intensional interpretations of functionals of finite type I. The Journal of Symbolic
Logic 32, pp. 198–212, doi:10.2307/2271658.
[21] Silvio Valentini (2001): An elementary proof of strong normalization for intersection types. Archive for
Mathematical Logic 40, pp. 475–488, doi:10.1007/s001530000070.

