Subject Reduction and Minimal Types for Higher Order Subtyping

Adriana Compagnoni

                                abc@dcs.ed.ac.uk

Department of Computer Science, University of Edinburgh The King’s Buildings, Edinburgh, EH9 3JZ, United Kingdom Tel: (+44) (131) 650-1000 Fax: (+44) (131) 667-7209

Abstract We define the typed lambda calculus F_{∧}^{ω}, a natural generalization of Girard’s system F^{ω} with intersection types and bounded polymorphism. A novel aspect of our presentation is the use of term rewriting techniques to present intersection types, which clearly splits the computational semantics (reduction rules) from the syntax (inference rules) of the system. We establish properties such as Church-Rosser for the reduction relation on types and terms, and Strong Normalization for the reduction on types. We prove that types are preserved by computation (Subject Reduction property), and that the system satisfies the Minimal Types property. On the way to establishing these results, we define algorithms for type inference and subtype checking.

1 Introduction

The formal study of subtyping in programming languages was begun by Reynolds [36] and Cardelli [10], who used a lambda-calculus with subtyping to model the refinement of interfaces in object oriented languages. This led to a considerable body of work, covering an increasing range of object-oriented features by combining subtyping with other typetheoretic constructs, including polymorphic functions [15, 27, 7], records with update and extension operators [10, 14], recursive types [2, 8], and higher-order polymorphism [11, 13, 12, 33].

Type systems with subtyping have also arisen from the study of lambda-calculi with intersection types at the University of Torino [26, 6]. Most of this work has been carried out in the setting of pure lambda-calculi, but it has also been applied to programming language design by Reynolds [37]. Some work has begun on combining intersections with other typing features [34, 17].

The system F_{∧}^{ω} (F-omega-meet) was first introduced in [23], where it was shown to be rich enough to provide a typed model of object oriented programming with multiple inheritance. F_{∧}^{ω} is an extension of F^{ω} [30] with bounded quantification and intersection types, which can be seen as a natural generalization of the type disciplines present in the current literature, for example in [27, 34, 35, 18]. Systems including either subtyping or intersection types or both have been widely studied for many years. What follows is not intended to be an exhaustive description, but a framework for the present work.

First-order type disciplines with intersection types have been investigated by the group in Torino [25, 6] and elsewhere (see [16] for background and further references). A secondorder λ-calculus with intersection types was studied in [34]. Systems including subtyping were present in [15, 10]. Higher order generalizations of subtyping appear in [9, 24, 33, 8]. F_{≤}, a second-order λ-calculus with bounded quantification, was studied in [29], and in [34].

Because F_{∧}^{ω} has reduction on types, we introduce a conversion rule that includes interconvertible types in the subtype relation. Therefore, our subtyping relation relates types of a more expressive type system than that presented in [18]. In fact, treating the interaction between interface refinement and encapsulation of objects in object oriented programming has required higher-order generalizations of subtyping: the F-bounded quantification of Canning, Cook, Hill, Olthoff and Mitchell [9] or system F_{≤}^{ω} [11, 13, 12, 33, 8].

We present a definition of F_{∧}^{ω} that differs from the one introduced in [23] in two ways. First, the ill-behaved Castagna and Pierce’s quantifier rule has been replaced by Cardelli and Wegner’s kernel Fun rule. Secondly, we introduce a richer notion of reduction on types, and thereby the four distributivity rules become particular cases of the conversion rule. This new reduction is shown to be confluent and strongly normalizing. The latter simplification was motivated by structural properties of the former presentation.

This new perspective suggests that to study the subtyping relation it is enough to concentrate on types in normal form. Note that the solution cannot be as simple as to restrict the subtyping rules of F_{∧}^{ω} to handle only types in normal form and replace conversion by reflexivity. The following is a good example of the problem to be solved. Consider the context Γ ≡ W:K, X ≤ ΛY:K.Y:K→K, Z ≤ X:K→K; observe that X and Z are subtypes of the identity on K. Then Γ ⊢ X(Z W) ≤ W is not derivable without using conversion, i.e. without performing any β-reduction, even when the conclusion is in normal form. (For a derivation see section 6.1.)

The subtyping rules of F_{∧}^{ω} are not syntax directed, in the sense that the form of a derivable subtyping statement does not uniquely determine the last rule of its derivation, i.e. there might be more than one derivation of the same subtyping judgement. To develop a deterministic decision procedure to check subtyping, we need a new presentation of the subtyping relation that provides the foundations for a subtype-checking deterministic algorithm.

We develop a normal subtyping system, NF_{∧}^{ω}, in which only types in normal form are considered. We prove that derivations in NF_{∧}^{ω} can be normalized by eliminating transitivity and simplifying reflexivity. This simplification yields an algorithmic presentation, AlgF_{∧}^{ω}. Moreover, we prove that AlgF_{∧}^{ω} is indeed an alternative presentation of the F_{∧}^{ω} subtyping relation, that is Γ ⊢ S ≤ T if and only if Γ^{nf} ⊢_{Alg} S^{nf} ≤ T^{nf} (proposition 9.2).

In [38] Steffen and Pierce studied F_{≤}^{ω} proving that typing is decidable and that the system satisfies the minimal types property. A central result in the proof of decidability is establishing the decidability of subtyping, a result first proved in [20]. There are several differences between our work and theirs. Our results are for a stronger system which also includes intersection types. A major difference is the choice of the intermediate subtyping system. We define the normal system NF_{∧}^{ω} which provides a generation principle for subtyping, yielding the algorithm AlgF_{∧}^{ω}. In [38] the intermediate system, called a reducing system, leads to a much more complicated proof which involves dealing with several notions of reduction and further reformulation of the intermediate system. A generation principle for subtyping is crucial to prove the Subject Reduction property (proposition 12.7), which is not proved in [38].

1.1 Results

• We define the typed lambda calculus F_{∧}^{ω}, a natural generalization of Girard’s system F^{ω} with intersection types and bounded polymorphism. A novel aspect of our presentation is the use of term rewriting techniques to present intersection types, which clearly splits the computational semantics (reduction rules) from the syntax (inference rules) of the system.

• The reduction rules of F_{∧}^{ω} can be divided into two main groups, reductions on types (→_{β∧}) and reductions on terms (→_{βfors}). Although confluence is not a modular property in general, in our case it is possible to provide a modular proof of it. In section 3, we combine the independent proofs of confluence for reductions on types and confluence for reduction on terms to yield a proof of confluence of the reduction relation in the whole system.

• We prove the strong normalization property of →_{β∧} on well-formed types.

• We define a normalized system NF_{∧}^{ω} equivalent to the original presentation of subtyping, and prove the transitivity elimination and reflexivity simplification properties.

• We define a subtyping algorithm AlgF_{∧}^{ω}, and prove that it is equivalent to the original presentation.

• In section 10, we prove that F_{∧}^{ω} satisfies the minimal types property, and we provide an algorithm for computing minimal types.

• We prove that F_{∧}^{ω} satisfies the subject reduction property using the minimal types property.

The original paper [20] defines the system F_{∧}^{ω} and its equivalent normal subtyping system NF_{∧}^{ω}. In the current paper we extend this framework to prove Subject Reduction and Minimal Typing.

2 SYNTAX OF F_{∧}^{ω} 4

2 Syntax of F_{∧}^{ω}

We now present the rules for kinding, subtyping, and typing in F_{∧}^{ω}. They are organized as proof systems for four interdependent judgement forms:

Γ ⊢ ok  well-formed context
Γ ⊢ T : K well-kinded type
Γ ⊢ S ≤ T subtype
Γ ⊢ e : T well-typed term.

We sometimes use the metavariable Σ to range over statements (right-hand sides of judgements) of any of these four forms.

2.1 Syntactic Categories

The kinds of F_{∧}^{ω} are those of F^{ω}: the kind ⋆ of proper types and the kinds K_{1}→K_{2} of functions on types (sometimes called type operators).

𝕂 ::= ⋆  types
| 𝕂 →𝕂 type operators

The language of types of F_{∧}^{ω} is a straightforward higher-order extension of F_{≤}, Cardelli and Wegner’s second-order calculus of bounded quantification. Like F_{≤}, it includes type variables (written X), function types (T →T′), and polymorphic types (∀X≤T:K.T′), in which the bound type variable X ranges over all subtypes of the upper bound T. Moreover, like F^{ω}, we allow types to be abstracted on types (ΛX:K.T) and applied to argument types (T T′); in effect, these forms introduce a simply typed λ-calculus at the level of types. Finally, we allow arbitrary finite intersections (⋀^{K}[T_{1}..T_{n}]), where all the T_{i}’s are members of the same kind K.

𝕋 ::= X  type variable
| 𝕋→𝕋  function type
| ∀X≤𝕋:𝕂 .𝕋 polymorphic type
| ΛX:𝕂 .𝕋  operator abstraction
| 𝕋 𝕋  operator application
|  ⋀^{𝕂}[𝕋..𝕋] intersection at kind 𝕂

We use the abbreviation ⊤^{K} for nullary intersections and sometimes X:K for X ≤ ⊤^{K}:K.

⊤^{K} ≡ ⋀^{K}[ ]  X:K ≡ X ≤ ⊤^{K}:K

We drop the maximal type Top of F_{≤}, since its role is played here by the empty intersection ⊤^{⋆}. For technical convenience, we provide kind annotations on bound variables and intersections so that every type has an “obvious kind,” which can be read off directly from its structure and the kind declarations in the context.

The language of terms includes the variables (x), applications (e e), and functional abstractions (λx:T.e) of the simply typed λ-calculus, plus the type abstraction (λX≤T:K.e) and application (e T) of F^{ω}. As in F_{≤}, each type variable is given an upper bound at the point where it is introduced.

Intersection types are introduced by expressions of the form “for(X∈T_{1}..T_{n})e”, which can be read as instructions to the type-checker to analyze the expression e separately under the assumptions X ≡ T_{1}, X ≡ T_{2}, …, X ≡ T_{n} and conjoin the results. For example, if + : Int→Int→Int ∧ Real→Real→Real, then we can derive:

for(X∈Int, Real)λx:X.x + x : Int→Int ∧ Real→Real.

e ::= x  variable
| λx:𝕋.e  abstraction
| e e  application
| λX≤𝕋:𝕂 .e type abstraction
| e 𝕋  type application
| for(X∈𝕋..𝕋)e alternation

The operational semantics of F_{∧}^{ω} is given by the following reduction rules on types and terms.

Definition 2.1.1 (Reduction rules for types)

1. (ΛX:K.T_{1})T_{2} →_{β∧} T_{1}[X←T_{2}]

2. S → ⋀^{⋆}[T_{1}..T_{n}] →_{β∧} ⋀^{⋆}[S→T_{1} .. S→T_{n}]

3. ∀X≤S:K.⋀^{⋆}[T_{1}..T_{n}] →_{β∧} ⋀^{⋆}[∀X≤S:K.T_{1} .. ∀X≤S:K.T_{n}]

4. ΛX:K_{1}.⋀^{K_{2}}[T_{1}..T_{n}] →_{β∧} ⋀^{K_{1}→K_{2}}[ΛX:K_{1}.T_{1} .. ΛX:K_{1}.T_{n}]

5. (⋀^{K_{1}→K_{2}}[T_{1}..T_{n}]) U →_{β∧} ⋀^{K_{2}}[T_{1} U .. T_{n} U]

6. ⋀^{K}[T_{1} .. ⋀^{K}[S_{1}..S_{n}] .. T_{m}] →_{β∧} ⋀^{K}[T_{1} .. S_{1}..S_{n} .. T_{m}]

The first rule is the usual β-reduction rule for types. Rules 2 through 5 express the fact that intersections in positive positions distribute with respect to the other type constructors. Rule 6 states that intersection is an associative operator. In section 5 we consider the reduction defined by rules 1 through 5 as →_{β∧}^{−} and the one defined by 6 as →_{a} (a comes from associativity). The left-hand side of each reduction rule is a redex and the right-hand side its reduct. The relation →_{β∧} is extended so as to become a compatible relation with respect to type formation, ↠_{β∧} is the transitive and reflexive closure of →_{β∧}, and =_{β∧} is the least equivalence relation containing →_{β∧}. The capture-avoiding substitution of S for X in T is written T [X←S]. Substitution is written similarly for terms, and is extended point-wise to contexts. The β∧-normal form of a type S is written S^{nf}, and is extended point-wise to contexts.

Definition 2.1.2 (Reduction rules for terms)

1. (λx:T_{1}.e_{1})e_{2} →_{βfors} e_{1}[x←e_{2}]

2. (λX≤T_{1}:K_{1}.e)T →_{βfors} e[X←T]

3. (for(X∈T_{1}..T_{n})e_{1})e_{2} →_{βfors} for(X∈T_{1}..T_{n})(e_{1} e_{2})

4. for(X∈T_{1}..T_{n})e →_{βfors} e, if X ∉ FV(e)

Rules 1 and 2 are the β-reductions on terms. Rule 3 says that the for constructor can be pushed to the outermost level. We consider the reduction defined by rules 1 through 3 as →_{βfor} and the one defined by 4 as →_{s} (s comes from simplification). The left-hand side of each reduction rule is a redex and the right-hand side its reduct. The relation →_{βfors} is extended so as to become a compatible relation with respect to term formation, ↠_{βfors} is the transitive reflexive closure of →_{βfors}, and =_{βfors} is the least equivalence relation containing →_{βfors}.

2.2 Contexts

A context Γ is a finite sequence of typing and subtyping assumptions for a set of term and type variables.

The empty context is written ∅. Term variable bindings have the form x:T; type variable bindings have the form X≤T:K, where T is the upper bound of X and K is the kind of T.

Γ ::= ∅  empty context
| Γ, x:T  term variable declaration
| Γ, X≤T:K type variable declaration

When writing nonempty contexts, we omit the initial ∅. The domain of Γ is written dom(Γ). The functions FV(—) and FTV(—) give the sets of free term variables and free type variables of a term, type, or context. Since we are careful to ensure that no variable is bound more than once, we sometimes abuse notation and consider contexts as finite functions: Γ(X) yields the bound of X in Γ, where X is implicitly asserted to be in dom(Γ).

Types, terms, contexts, statements, and derivations that differ only in the names of bound variables are considered identical. The underlying idea is that variables are de Bruijn indexes [28].

Definition 2.2.1 (Closed)

1. A term e is closed with respect to a context Γ if FV(e) ∪ FTV(e) ⊆ dom(Γ).

2. A type T is closed with respect to a context Γ if FTV(T) ⊆ dom(Γ).

3. A typing statement Γ ⊢ e : T is closed if e and T are closed with respect to Γ.

4. A kinding statement Γ ⊢ T : K is closed if T is closed with respect to Γ.

5. A subtyping statement Γ ⊢ S ≤ T is closed if S and T are closed with respect to Γ.

We consider only closed typing statements. Observe that in the limit case of the rule T-Meet, when n = 0, not having the closure convention would allow nonsensical terms to be typed. On the other hand, the free variable lemma (lemma 4.3) guarantees that kinding statements are closed and the well-kindedness of subtyping (lemma 4.18) ensures that subtyping statements are closed as well.

2.3 Context Formation

The rules for well-formed contexts are the usual ones: a start rule for the empty context and rules allowing a given well-formed context to be extended with either a term variable binding or a type variable binding.

∅ ⊢ ok  (C-Empty)
\frac{Γ ⊢ T : ⋆  x ∉ dom(Γ)}{Γ, x:T ⊢ ok}  (C-Var)

\frac{Γ ⊢ T : K  X ∉ dom(Γ)}{Γ, X≤T:K ⊢ ok}  (C-TVar)

2.4 Type Formation

For each type constructor, we give a rule specifying how it can be used to build wellformed type expressions. The critical rules are K-OAbs and K-OApp, which form type abstractions and type applications (essentially as in a simply typed λ-calculus).

The well-formedness premise Γ ⊢ ok in K-Meet (and in T-Meet below) is required for the case where n = 0.

\frac{Γ_{1}, X≤T:K, Γ_{2} ⊢ ok}{Γ_{1}, X≤T:K, Γ_{2} ⊢ X : K}  (K-TVar)

\frac{Γ ⊢ T_{1} : ⋆  Γ ⊢ T_{2} : ⋆}{Γ ⊢ T_{1}→T_{2} : ⋆}  (K-Arrow)

\frac{Γ, X≤T_{1}:K_{1} ⊢ T_{2} : ⋆}{Γ ⊢ ∀X≤T_{1}:K_{1}.T_{2} : ⋆}  (K-All)

\frac{Γ, X:K_{1} ⊢ T_{2} : K_{2}}{Γ ⊢ ΛX:K_{1}.T_{2} : K_{1}→K_{2}}  (K-OAbs)

\frac{Γ ⊢ S : K_{1}→K_{2}  Γ ⊢ T : K_{1}}{Γ ⊢ S T : K_{2}}  (K-OApp)

\frac{Γ ⊢ ok  for each i ∈ \{1..n\} , Γ ⊢ T_{i} : K}{Γ ⊢ ⋀^{K}[T_{1}..T_{n}] : K}  (K-Meet)

2.5 Subtyping

The rules defining the subtype relation are a natural extension of familiar calculi of bounded quantification. Aside from some extra well-formedness conditions, the rules S-Trans, S-TVar, and S-Arrow are the same as in the usual, second-order case. Rules S-OAbs and S-OApp extend the subtype relation point-wise to kinds other than ⋆. The rule of type conversion in F^{ω}, that is, if Γ ⊢ e : T and T =_{β} T′ then Γ ⊢ e : T′, is captured here as the subtyping rule S-Conv, which also gives reflexivity as a special case. The rule S-All is the rule of Cardelli and Wegner’s Fun language [15] in which the bounds of the quantifiers are equal. Rules S-Meet-G and S-Meet-LB specify that an intersection of a set of types is the set’s order-theoretic greatest lower bound.

\frac{Γ ⊢ S : K  Γ ⊢ T : K  S =_{β∧} T}{Γ ⊢ S ≤ T}  (S-Conv)

\frac{Γ ⊢ S ≤ T  Γ ⊢ T ≤ U}{Γ ⊢ S ≤ U}  (S-Trans)

\frac{Γ_{1}, X≤T:K, Γ_{2} ⊢ ok}{Γ_{1}, X≤T:K, Γ_{2} ⊢ X ≤ T}  (S-TVar)

\frac{Γ ⊢ T_{1} ≤ S_{1}  Γ ⊢ S_{2} ≤ T_{2}  Γ ⊢ S_{1}→S_{2} : ⋆}{Γ ⊢ S_{1}→S_{2} ≤ T_{1}→T_{2}}  (S-Arrow)

\frac{Γ, X≤U:K ⊢ S ≤ T  Γ ⊢ ∀X≤U:K.S : ⋆}{Γ ⊢ ∀X≤U:K.S ≤ ∀X≤U:K.T}  (S-All)

\frac{Γ, X:K ⊢ S ≤ T}{Γ ⊢ ΛX:K.S ≤ ΛX:K.T}  (S-OAbs)

\frac{Γ ⊢ S ≤ T  Γ ⊢ S U : K}{Γ ⊢ S U ≤ T U}  (S-OApp)

\frac{for each i ∈ \{1..n\} , Γ ⊢ S ≤ T_{i}  Γ ⊢ S : K}{Γ ⊢ S ≤ ⋀^{K}[T_{1}..T_{n}]}  (S-Meet-G)

\frac{Γ ⊢ ⋀^{K}[T_{1}..T_{n}] : K}{Γ ⊢ ⋀^{K}[T_{1}..T_{n}] ≤ T_{i}}  (S-Meet-LB)

2.6 Term Formation

Except for T-Meet and T-For, the term formation rules are precisely those of the secondorder calculus of bounded quantification. T-For provides for type checking under any of a set of alternate assumptions. For each S_{i}, the type derived for the instance of the body e when X is replaced by S_{i} is a valid type of the for expression itself. The T-Meet rule can then be used to collect these separate typings into a single intersection. Type-theoretically, T-Meet is the introduction rule for the ∧ constructor; the corresponding elimination rule need not be given explicitly, since it follows from T-Subsumption and S-Meet-LB.

\frac{Γ_{1}, x:T , Γ_{2} ⊢ ok}{Γ_{1}, x:T , Γ_{2} ⊢ x : T}  (T-Var)
\frac{Γ, x:T_{1} ⊢ e : T_{2}}{Γ ⊢ λx:T_{1}.e : T_{1}→T_{2}}  (T-Abs)
\frac{Γ ⊢ f : T_{1}→T_{2}  Γ ⊢ a : T_{1}}{Γ ⊢ f a : T_{2}}  (T-App)
\frac{Γ, X≤T_{1}:K_{1} ⊢ e : T_{2}}{Γ ⊢ λX≤T_{1}:K_{1}.e : ∀X≤T_{1}:K_{1}.T_{2}}  (T-TAbs)
\frac{Γ ⊢ f : ∀X≤T_{1}:K_{1}.T_{2}  Γ ⊢ S ≤ T_{1}}{Γ ⊢ f S : T_{2}[X←S]}  (T-TApp)
\frac{Γ ⊢ e[X←S] : T  S : \{S_{1}..S_{n}\}}{Γ ⊢ for(X∈S_{1}..S_{n})e : T}  (T-For)
\frac{Γ ⊢ ok  for each i ∈ \{1..n\} , Γ ⊢ e : T_{i}}{Γ ⊢ e : ⋀^{⋆}[T_{1}..T_{n}]}  (T-Meet)
\frac{Γ ⊢ e : S  Γ ⊢ S ≤ T}{Γ ⊢ e : T}  (T-Subsumption)

Most of the rules include premises which have two rather different sorts: structural premises, which play an essential role in giving the rule its intended semantic force, and well-formation premises, which ensure that the entities named in the rule are of the expected sorts.

We sometimes omit well-formation premises that can be derived from others. For example, in the rule S-Arrow, we drop the premise Γ ⊢ T_{1}→T_{2} : ⋆, since it follows from Γ ⊢ S_{1}→S_{2} : ⋆ using the properties proved in section 4.

2.7 Discussion

An equivalent presentation of intersection types uses binary intersections as in [25]. The intersection of S and T is then written S ∧T, and there is a maximal element at each kind, ω^{K}. The rules of the system have to be modified according to this alternative notation. In most cases, each of our rules about intersection types has to be replaced by two rules, one for the binary case and another for the maximal element. For example, the reduction rule

∀X≤S:K.⋀^{⋆}[T_{1}..T_{n}] →_{β∧} ⋀^{⋆}[∀X≤S:K.T_{1} .. ∀X≤S:K.T_{n}]

is replaced by

\begin{aligned}∀X≤S:K.T_{1} ∧ T_{2} & →_{β∧} & ∀X≤S:K.T_{1} ∧ ∀X≤S:K.T_{2} & and \\ ∀X≤S:K.ω^{⋆} & →_{β∧} & ω^{⋆}. \end{aligned}

Similar replacement takes place for rules 3 through 5 in definition 2.1.1. The term formation rule K-Meet is replaced by the two following rules.

\frac{Γ ⊢ S : K  Γ ⊢ T : K}{Γ ⊢ S ∧ T : K}  (K-Int)

\frac{Γ ⊢ ok}{Γ ⊢ ω^{K} : K}  (K-Max)

The rule S-Meet-G is replaced by the following two rules.

\frac{Γ ⊢ S ≤ T_{1} Γ ⊢ S ≤ T_{2}}{Γ ⊢ S ≤ T_{1} ∧ T_{2}}  (S-Int-G)

\frac{Γ ⊢ S : K}{Γ ⊢ S ≤ ω^{K}}  (S-Max)

In the λ-cube [4], F^{ω}corresponds to λ_{ω}, the system defined by the rules (⋆, ⋆), (□, ⋆), and (□, □). If K is a kind defined by the grammar 𝕂, then

Γ ⊢_{λ_{ω}} K : □.

The rule (□, □) corresponds to the recursive step in the definition of 𝕂; the rule (⋆, ⋆) corresponds to K-Arrow, and K-All is the parallel of rule (□, ⋆) enriched with subtyping.

3 Confluence

In this section, we show that the system F_{∧}^{ω} is confluent. By that we mean that the reduction →_{βfors} ∪ →_{β∧} defined by putting together the reduction on terms, →_{βfors} (definition 2.1.2), and the reduction on types, →_{β∧} (definition 2.1.1), satisfies the Church-Rosser property. We use the Hindley-Rosen lemma (c.f. 3.3.5 [5]) to establish this result. This factors the proof into two parts:

1. proving that the reductions ↠_{βfors} and ↠_{β∧} commute, and

2. proving that the reductions →_{βfors} and →_{β∧} satisfy the Church-Rosser property.

Full details of the proofs of this section as well as intermediate results can be found in [22]. Remember that two binary relations →_{1} and →_{2} commute if given A →_{1} B and A →_{2} C, there exists D such that C →_{1} D and B →_{2} D. In order to prove that ↠_{βfors} and ↠_{β∧} commute we use the following lemma.

Lemma 3.1 (3.3.6 [5]) Let →_{1} and →_{2} be two binary relations on a set X. Suppose that if A →_{1} B and A →_{2} C, there exists D such that C →_{=1} D and B → →_{2} D, where →_{=1} is the reflexive closure of →_{1}. Hence → →_{1} and → →_{2} commute.

Lemma 3.2 If A →_{βfors} B and A →_{β∧} C, there exists D such that C →_{=βfors} D and B ↠_{β∧} D

Proof: By induction on the structure of E. □

Corollary 3.3 ↠_{β∧} and ↠_{βfors} commute.

The Church-Rosser theorem for →_{β∧}

We now prove the Church-Rosser property for the reduction defined in 2.1.1. The strategy we use here is similar to the one used in chapter 11 section 1 of [5] to prove the corresponding result for →_{β} in the type-free λ-calculus.

In order to prove the Church-Rosser property for →_{β∧} it is sufficient to show the following strip lemma.

Lemma 3.4 (Strip) Let S, T_{1}, and T_{2} ∈ 𝕋. If S →_{β∧} T_{1} and S ↠_{β∧} T_{2}, then there exists T_{3} ∈ 𝕋 such that T_{1} ↠_{β∧} T_{3} and T_{2} ↠_{β∧} T_{3}.

The idea of the proof is as follows. Let T_{1} be the result of replacing the redex R in S by its reduct R′. If we keep track of what happens with R during the reduction S ↠_{β∧} T_{2}, then we can find T_{3}. To be able to trace R we define a new set of terms \underline{𝕋} where redexes can appear underlined. Consequently, if we underline R in S we only need to reduce all occurrences of the underlined R in T_{2} to obtain T_{3}.

Theorem 3.5 (Church-Rosser for →_{β∧})

If S, T_{1}, and T_{2} ∈ 𝕋 are such that S ↠_{β∧} T_{1} and S ↠_{β∧} T_{2}, then there exists T_{3} ∈ 𝕋 such that T_{1} ↠_{β∧} T_{3} and T_{2} ↠_{β∧} T_{3}.

Proof: By induction on the generation of S ↠_{β∧} T_{1}. □

The Church-Rosser theorem for →_{βfors}

Next we prove the Church-Rosser property for the reduction defined in definition 2.1.2.

Theorem 3.6 (Church-Rosser for →_{βfors})

Let e, f_{1}, f_{2} ∈ 𝔼. If e ↠_{βfors} f_{1} and e ↠_{βfors} f_{2}, then there exists f_{3} ∈ 𝔼 such that f_{1} ↠_{βfors} f_{3} and f_{2} ↠_{βfors} f_{3}.

The idea of the proof is as follows. We prove that →_{βfor} and →_{s} are Church-Rosser (theorem 3.7 and lemma 3.8); that →_{s} reduction steps can be postponed (lemma 3.9), and that ↠_{βfor} and ↠_{s} commute (lemma 3.10).

Those four results allow us to prove the Church-Rosser theorem for →_{βfors}. Let e, e_{1}, e_{2} ∈ 𝔼, such that e ↠_{βfors} e_{1} and e ↠_{βfors} e_{2}. Then, by s-postponement, there exist f_{1} and f_{2}; by Church-Rosser for →_{βfor}, there exists f_{3}; and, by lemma 3.10, there exist f_{4} and f_{5}, and finally, by Church-Rosser for →_{s}, there exists e_{3} which completes the following diagram.

[figure: e; βfor; f_{1}; s; e_{1}]

[figure: f_{2}; βfor; .; .; .; .; .; .; .; .; .; βfor; f_{3}; . . . . . . . .; βfor; .; .; .; .; .; .; .; .; .; s; f_{4}; . . . . . . . .; βfor]

[figure: e_{2}; s; .; .; .; .; .; .; .; .; .; βfor; f_{5}; . . . . . . . .; s; .; .; .; .; .; .; .; .; .; s; e_{3}; . . . . . . . . .; s]

The Church-Rosser property for →_{βfor} follows using the same strategy used to prove theorem 3.5.

Theorem 3.7 (Church-Rosser for →_{βfor})

If e, f_{1}, and f_{2} ∈ 𝔼 are such that e ↠_{βfor} f_{1} and e ↠_{βfor} f_{2}, then there exists f_{3} ∈ 𝔼 such that f_{1} ↠_{βfor} f_{3} and f_{2} ↠_{βfor} f_{3}.

The Church-Rosser property for →_{s} is proved using the Newman’s proposition 3.1.25 in [5], by proving that →_{s} is strongly normalizing and weak Church-Rosser.

Lemma 3.8 (Church-Rosser for →_{s}) If e, e_{1}, and e_{2} ∈ 𝔼 are such that e ↠_{s} e_{1} and e ↠_{s} e_{2}, then there exists e_{3} such that e_{1} ↠_{s} e_{3} and e_{2} ↠_{s} e_{3}.

Lemma 3.9 (s-postponement) If e →_{s} e_{1} and e_{1} →_{βfor} e_{2}, then there exists e_{3} such that e →_{βfor} e_{3} and e_{3} ↠_{s} e_{1}.

Lemma 3.10 If e, e_{1}, and e_{2} ∈ 𝔼 are such that e ↠_{βfor} e_{1} and e ↠_{s} e_{2} then there exists e_{3} such that e_{1} ↠_{s} e_{3} and e_{2} ↠_{βfor} e_{3}.

Finally, we can state and prove the confluence property for the reduction relation of F_{∧}^{ω}.

4 STRUCTURAL PROPERTIES 13

Confluence of F_{∧}^{ω}

Theorem 3.11 (Church-Rosser for →_{βfors} ∪ →_{β∧})

If E, F, and G ∈ 𝕋 ∪ 𝔼 are such that E ↠_{βfors∪β∧} F and E ↠_{βfors∪β∧} G, then there exists H ∈ 𝕋 ∪ 𝔼 such that F ↠_{βfors∪β∧} H and G ↠_{βfors∪β∧} H. Proof: By the commutativity of ↠_{βfors} and ↠_{β∧} (corollary 3.3) and the Church-Rosser property of →_{βfors} and →_{β∧} (theorems 3.5 and 3.6). □

The Church-Rosser theorem has interesting corollaries that we will use in the sequel. Corollary 3.12 See chapter 3 of [5]. Let R be a reduction satisfying the Church-Rosser property. Then

1. If T =_{R}S, then there exists U such that T → →_{R} U and S → →_{R} U.

2. If T is a normal form of S, then S → →_{R} T.

3. Each term has at most one R-normal form. Fact 3.13

1. ∀X≤S:K.T =_{β∧} ⊤^{⋆} if and only if T =_{β∧} ⊤^{⋆}.

2. ΛX:K.T =_{β∧} ⊤^{⋆} if and only if T =_{β∧} ⊤^{⋆}.

3. S→T =_{β∧} ⊤^{⋆} if and only if T =_{β∧} ⊤^{⋆}.

4. T S =_{β∧} ⊤^{⋆} if and only if T =_{β∧} ⊤^{⋆}. Lemma 3.14 If S ↠_{β∧} S′, then S[X←U] ↠_{β∧} S′[X←U].

4 Structural properties

This section establishes a number of structural properties of F_{∧}^{ω}. Except where noted, the proofs proceed by structural induction and are straightforward when performed in the order in which they appear. Lemma 4.1 If Γ ⊢ Σ and Γ_{1} is a prefix of Γ, then Γ_{1} ⊢ ok as a subderivation. Moreover, except for the case Γ_{1} ≡ Γ and Σ ≡ ok, the subderivation is strictly shorter. Lemma 4.2 (Generation for context judgements)

1. If Γ_{1}, X≤T:K, Γ_{2} ⊢ ok, then Γ_{1} ⊢ T : K by a proper subderivation.

2. If Γ_{1}, x:T , Γ_{2} ⊢ ok, then Γ_{1} ⊢ T : ⋆ by a proper subderivation. Lemma 4.3 (Free variables)

1. If Γ ⊢ T : K, then FTV(T) ⊆ dom(Γ).

2. If Γ ⊢ ok, then each variable or type variable in dom(Γ) is declared only once.

If one tries to prove Weakening (Corollary 4.6) directly by induction on derivations the induction hypothesis is too weak in the cases for K-All and S-OAbs, for example. This problem occurs in the lambda calculus without subtyping for the abstraction rule, and was identified by McKinna and Pollack for Pure Type Systems. We adapt their idea of renaming [32].

Definition 4.4 (Parallel Substitution) A parallel substitution γ for Γ is an assignment of types to type variables in dom(Γ) and terms to term variables in dom(Γ). A renaming for Γ in Δ is a parallel substitution γ from variables to variables such that

• for every x:A in Γ, γ(x):A[γ] is in Δ, and

• for every X≤T:K in Γ, γ(X)≤A[γ]:K is in Δ.

We write Σ[γ] for the result of performing the substitution γ in the judgement Σ. The renaming γ{x ↦ y} maps x to y and behaves like γ elsewhere, similarly for type variables.

Lemma 4.5 (Renaming) If Δ ⊢ ok and γ is a renaming for Γ in Δ then Γ ⊢ Σ implies Δ ⊢ Σ[γ].

Proof: By induction on the derivation of Γ ⊢ Σ. Most cases follow easily using the induction hypothesis or the definition of renaming. We illustrate here the case for K-All, which is representative of the interesting cases.

Let Z ∉ dom(Δ). Define γ_{0} as γ_{0} ≡ γ{X ↦ Z}, then γ_{0} is a renaming for Γ, X≤T_{1}:K_{1} in Δ, Z≤T_{1}[γ_{0}]:K_{1}. By lemmas 4.1 and 4.2(1), there exists a shorter subderivation of Γ ⊢ T_{1} : K_{1}, and by the free variables lemma (lemma 4.3), X ∉ FV(T_{1}), therefore T_{1}[γ_{0}] ≡ T_{1}[γ].

We need to show that Δ, Z≤T_{1}[γ]:K_{1} ⊢ ok. By assumption we know that Δ ⊢ ok, by the induction hypothesis, Δ ⊢ T_{1}[γ] : K_{1}. Since we chose Z not to be in dom(Δ), by

K-TVar, Δ, Z≤T_{1}[γ]:K_{1} ⊢ ok.

We can now apply the induction hypothesis to prove Δ, Z≤T_{1}[γ]:K_{1} ⊢ T_{2}[γ_{0}] : ⋆. By K-All, Δ ⊢ ∀Z≤T_{1}[γ]:K_{1}.T_{2}[γ_{0}] : ⋆, and by the definition of substitution Δ ⊢ (∀X≤T_{1}:K_{1}.T_{2} : ⋆)[γ]. □

Weakening now follows as a corollary of renaming taking γ to be the identity substitution.

Corollary 4.6 (Weakening/Permutation) Let Γ and Γ′ be contexts such that Γ ⊆ Γ′ and Γ′ ⊢ ok. Then Γ ⊢ Σ implies Γ′ ⊢ Σ.

Proof: Let γ be the identity substitution. Then γ is a renaming for Γ in Δ and Σ[γ] ≡ Σ. Then, by Renaming (Proposition 4.5), it follows that Δ ⊢ Σ. □

Lemma 4.7 (Context, kind, and term strengthening)

1. If Γ_{1}, X≤T:K, Γ_{2} ⊢ ok and X ∉ FTV(Γ_{2}), then Γ_{1}, Γ_{2} ⊢ ok.

2. If Γ_{1}, X≤T:K, Γ_{2} ⊢ S : K′ and X ∉ FTV(Γ_{2}) ∪ FTV(S), then Γ_{1}, Γ_{2} ⊢ S : K′.

3. If Γ_{1}, x:T , Γ_{2} ⊢ Σ and x ∉ FV(Σ), then Γ_{1}, Γ_{2} ⊢ Σ.

Moreover, the derivations of the conclusions are strictly shorter than the derivation of the premises.

Proof: Statements 1 and 2 follow by simultaneous induction on the length of derivations, and statement 3 by induction on the derivation of Γ_{1}, x:T , Γ_{2} ⊢ Σ. In all cases lemmas 4.1 and 4.3 are used. □

Proposition 4.8 (Generation for kinding)

1. Γ ⊢ X : K implies Γ ≡ Γ_{1}, X≤T:K, Γ_{2} for some Γ_{1}, T, and Γ_{2}.

2. Γ ⊢ T_{1}→T_{2} : K implies K ≡ ⋆ and Γ ⊢ T_{1}, T_{2} : ⋆.

3. Γ ⊢ ∀X≤T_{1}:K_{1}.T_{2} : K implies K ≡ ⋆ and Γ, X≤T_{1}:K_{1} ⊢ T_{2} : ⋆.

4. Γ ⊢ Λ(X:K_{1})T_{2} : K implies K ≡ K_{1}→K_{2} and Γ, X≤⊤^{K_{1}}:K_{1} ⊢ T_{2} : K_{2}, for some K_{2}.

5. Γ ⊢ S T : K implies Γ ⊢ S : K′→K and Γ ⊢ T : K′, for some K′.

6. Γ ⊢ ⋀^{K}[T_{1}..T_{n}] : K′ implies K ≡ K′ and Γ ⊢ ok and Γ ⊢ T_{i} : K for each i.

Moreover, the proofs of the consequents are all strictly shorter than those of the antecedents.

Proof: In each case the antecedent uniquely determines the last rule of its derivation. The proof follows by inspection of the rules. □

Lemma 4.9 (Uniqueness of kinds) If Γ ⊢ T : K and Γ ⊢ T : K′, then K ≡ K′.

Lemma 4.10 (Type substitution) Let Γ_{1} ⊢ T : K_{U}. Then

1. If Γ_{1}, X≤U:K_{U}, Γ_{2} ⊢ S : K_{S}, then Γ_{1}, Γ_{2}[X←T] ⊢ S[X←T] : K_{S}.

2. If Γ_{1}, X≤U:K_{U}, Γ_{2} ⊢ ok, then Γ_{1}, Γ_{2}[X←T] ⊢ ok.

Proof: By simultaneous induction on derivations of the premises. The proof of part 2 is straightforward using part 1 of the induction hypothesis. We consider the details of the proof of 1. The cases K-Arrow, K-All, K-OAbs, and K-OApp follow by straightforward application of part 1 of the induction hypothesis and the corresponding rule, while the case of K-Meet also uses part 2 of the induction hypothesis. We examine the case of K-TVar, where S ≡ Y for some variable Y. By proposition 4.8(1) Y ≤T_{Y}:K_{S} : (Γ_{1}, X≤U:K_{U}, Γ_{2}) for some T_{Y}. There are three cases to consider.

Y ≤T_{Y}:K_{S} ∈ Γ_{1} Then we also have Y ≤T_{Y}:K_{S} ∈ (Γ_{1}, Γ_{2}[X←T]). By part 2 of the induction hypothesis, Γ_{1}, Γ_{2}[X←T] ⊢ ok. Applying K-TVar, we get Γ_{1}, Γ_{2}[X←T] ⊢ Y :

K_{S}.

Y ≤T_{Y}:K_{S} ≡ X≤U:K_{U} We know that Γ_{1} ⊢ T : K_{S} ≡ K_{U}. From the premise of K-TVar and part 2 of the induction hypothesis, we have Γ_{1}, Γ_{2}[X←T] ⊢ ok. The result follows by weakening (corollary 4.6).

Y ≤T_{Y}:K_{S} ∈ Γ_{2} Then we have Y ≤T_{Y} [X←T]:K_{S} ∈ (Γ_{1}, Γ_{2}[X←T]). By part 2 of the induction hypothesis, Γ_{1}, Γ_{2}[X←T] ⊢ ok, from which the result follows by K-TVar. □

Lemma 4.11 (Subject reduction for kinding judgements) If S ↠_{β∧} T and Γ ⊢ S : K, then Γ ⊢ T : K.

Proof: In order to prove this result it is enough to prove the following statements by simultaneous induction on the derivation of Γ ⊢ S : K. The rest follows by induction on the definition of ↠_{β∧}.

1. Γ ⊢ ok and Γ →_{β∧} Γ′ implies Γ′ ⊢ ok.

2. Γ ⊢ S : K and S →_{β∧} T implies Γ ⊢ T : K.

3. Γ ⊢ S : K and Γ →_{β∧} Γ′ implies Γ′ ⊢ S : K. □

Theorem 4.12 (Kind invariance under type conversion) If Γ ⊢ S : K_{S} and Γ ⊢ T : K_{T}, with S =_{β∧} T, then K_{S} ≡ K_{T}.

Proof: By the Church-Rosser theorem 3.5, there exists U such that S ↠_{β∧} U and T ↠_{β∧} U, and the result follows by subject reduction and unicity of kinds. □

Lemma 4.13 Let Γ ⊢ S_{j} : K for each j ∈ {1..m}. Then if for every i ∈ {1..n} there exists j ∈ {1..m} such that Γ ⊢ S_{j} ≤ T_{i}, then Γ ⊢ ⋀^{K}[S_{1}..S_{m}] ≤ ⋀^{K}[T_{1}..T_{n}].

A particular case of the previous lemma is the following.

Corollary 4.14 Let Γ ⊢ S_{i} : K for each i ∈ {1..n}. Then Γ ⊢ S_{i} ≤ T_{i}, for every i ∈ {1..n}, implies Γ ⊢ ⋀^{K}[S_{1}..S_{n}] ≤ ⋀^{K}[T_{1}..T_{n}].

Lemma 4.15 Let Γ ⊢ S, T : K. Then Γ ⊢ S ≤ T if and only if Γ ⊢ S^{nf} ≤ T^{nf}.

Proof: We shall consider only one part the other is similar.

⇒) By subject reduction, we have that Γ ⊢ S^{nf} : K, then, by S-Conv, Γ ⊢ S^{nf} ≤ S. By

similar reasoning we have Γ ⊢ T ≤ T^{nf}. The result follows by applying S-Trans twice. □ Lemma 4.16 (Context modification) If Γ_{1} ⊢ U′ : K and Σ is either ok or T : K′, then Γ_{1}, X≤U:K, Γ_{2} ⊢ Σ implies Γ_{1}, X≤U′:K, Γ_{2} ⊢ Σ.

Lemma 4.17 Let Γ ⊢ S_{i} : K for every i ∈ {1..n}. If for every j in {1..m} there exists i in {1..n} such that Γ ⊢ S_{i} ≤ T_{j}, then Γ ⊢ ⋀^{K}[S_{1}..S_{n}] ≤ ⋀^{K}[T_{1}..T_{m}].

Proposition 4.18 (Well-kindedness of subtyping) If Γ ⊢ S ≤ T, then Γ ⊢ S : K and Γ ⊢ T : K for some K.

Proof: By induction on the derivation of Γ ⊢ S ≤ T. We show a few representative cases.

S-Conv We are given that Γ ⊢ S : K and Γ ⊢ T : K′ and S =_{β} T. By lemma 4.12, K ≡ K′.

S-TVar We are given that Γ_{1}, X≤T:K, Γ_{2} ⊢ ok. Γ_{1}, X≤T:K, Γ_{2} ⊢ X : K follows by K-TVar. Moreover, by lemma 4.2, we have Γ_{1} ⊢ T : K, and by weakening (corollary 4.6), Γ_{1}, X≤T:K, Γ_{2} ⊢ T : K.

S-Arrow We are given Γ ⊢ T_{1} ≤ S_{1} and Γ ⊢ S_{2} ≤ T_{2} and Γ ⊢ S_{1}→S_{2} : ⋆. By proposition 4.8, Γ ⊢ S_{1}, S_{2} : ⋆. Further, by the induction hypothesis together with uniqueness of kinds (lemma 4.9), we have Γ ⊢ T_{1}, T_{2} : ⋆. Finally, the result follows by applying

K-Arrow. □

Proposition 4.19 (Well-kindedness of typing) If Γ ⊢ e : T, then Γ ⊢ T : ⋆.

Proof: By induction on the derivation of Γ ⊢ e : T. We show here a few interesting cases

T-Var We are given Γ_{1}, x:T , Γ_{2} ⊢ ok. The result follows by generation for context judgements (lemma 4.2) and weakening (corollary 4.6).

T-Abs We are given Γ, x:T_{1} ⊢ e : T_{2}. By the induction hypothesis, Γ, x:T_{1} ⊢ T_{2} : ⋆. By lemma 4.7, it follows that Γ ⊢ T_{2} : ⋆. Furthermore, by lemmas 4.1 and 4.2, Γ ⊢ T_{1} : ⋆. Hence, K-Arrow yields Γ ⊢ T_{1}→T_{2} : ⋆.

T-TApp We know that Γ ⊢ f : ∀(X≤T_{1}:K_{1})T_{2} and also Γ ⊢ S ≤ T_{1}. By the induction hypothesis, Γ ⊢ ∀(X≤T_{1}:K_{1})T_{2} : ⋆ and, by proposition 4.8, Γ, X≤T_{1}:K_{1} ⊢ T_{2} : ⋆. By lemmas 4.1 and 4.2, there exists a derivation of Γ ⊢ T_{1} : K_{1}. By the well-kindedness of subtyping (proposition 4.18) and uniqueness of kinds (lemma 4.9), we have Γ ⊢ S : K_{1}. Then, by the type substitution lemma (lemma 4.10), Γ ⊢ T_{2}[X←S] : ⋆.

T-Sub By the induction hypothesis, proposition 4.18 and lemma 4.9. □

5 STRONG NORMALIZATION OF →_{β∧} 18

5 Strong normalization of →_{β∧}

We prove that every type that has a kind in F_{∧}^{ω} is strongly normalizing in three steps. We first prove that →_{a} and also →_{β∧}^{−} are strongly normalizing. Then we prove that both reductions commute, i.e. if T →_{a} T_{1} and T_{1} →_{β∧}^{−} T_{2}, then there exists S such that S →_{a} T_{2} and T ↠_{β∧}^{−}^{>0} S (in at least one step). Finally, using the previous two steps we prove that →_{β∧} is strongly normalizing.

A type T is called strongly normalizing if and only if all reduction sequences starting with T terminate. We write 𝕋 for the set of all type expressions and SN for the subset of 𝕋 of strongly normalizing type expressions. If A and B are subsets of 𝕋, then A → B denotes the following subset of 𝕋

A → B = {F ⊆ 𝕋 | for all a ∈ A, F a ∈ B}.

Lemma 5.1 →_{a} is strongly normalizing.

Proof: By induction on the number of intersection symbols of the type expression being reduced. □

To prove strong normalization of →_{β∧}^{−} we use a model-theoretic argument interpreting kinds as sets of normalizing terms, and the soundness of the model gives, as a corollary, the strong normalization property. The interpretation of a kind K, notation [[K]], is defined as follows.

\begin{aligned}[[ ⋆]] & = & SN \\ [[K_{1}→K_{2}]] & = & [[K_{1}]] → [[K_{2}]]. \end{aligned}

Definition 5.2 (Saturated set) S ⊆ SN is saturated if is satisfies the following conditions:

1. If R_{1}..R_{n} ∈ SN, then XR_{1}..R_{n} ∈ S.

2. If R_{1}..R_{n}, Q ∈ SN, then

(a) if P [X←Q]R_{1}..R_{n} ∈ S, then (ΛX:K.P)QR_{1}..R_{n} ∈ S, for every K and

(b) if (⋀^{K_{2}}[T_{1}Q, .., T_{m}Q])R_{1}, .., R_{n} ∈ S, then (⋀^{K_{1}→K_{2}}[T_{1}, .., T_{m}])QR_{1}, .., R_{n} ∈ S, for every K_{1}.

Intuitively, a set of strongly normalizing type expressions is saturated if it contains all type variables and is closed under expansion of expressions which may have a kind of the form K_{1}→K_{2}.

Lemma 5.3

1. SN is saturated.

2. If A, B are saturated, then A → B is saturated.

3. For any kind K, [[K]] is saturated.

Definition 5.4

1. A valuation ρ in 𝕋 is a mapping from type variables to types.

2. The interpretation of a type with respect to ρ is

[[T]]_{ρ} = T [X_{1} ← ρ(X_{1})..X_{n} ← ρ(X_{n})],

where FV(T) = {X_{1}..X_{n}}.

3. Let ρ be a valuation in 𝕋. Then ρ satisfies T : K, written ρ ⊧ T : K, if [[T]]_{ρ} : [[K]] and ρ satisfies X≤T:K, written ρ ⊧ X≤T:K, if ρ(X) : [[K]]. We say that ρ satisfies a context Γ, ρ ⊧ Γ, if ρ ⊧ X ≤ S:K for all X ≤ S:K : Γ.

4. A context Γ satisfies T : K, written Γ ⊧ T : K, if for every ρ such that ρ ⊧ Γ, it follows that ρ ⊧ T : K.

Lemma 5.5

1. ⊤^{K} ∈ [[K]].

2. If A_{i} ∈ [[K]] for each i ∈ {1..n}, then ⋀^{K}[A_{1}..A_{n}] ∈ [[K]].

Proof: We show item 2. Item 1 also follows follows by induction on the structure of K.

K ≡ ⋆ Then, by definition of [[K]], A_{i} ∈ SN for each i ∈ {1..n}. Since every reduction starting from ⋀^{K}[A_{1}..A_{n}] is a reduction consisting only of steps inside the A_{i}′s, one has ⋀^{K}[A_{1}..A_{n}] ∈ SN ≡ [[K]].

K ≡ K_{1}→K_{2} Let B ∈ [[K_{1}]]. By the definition of →, A_{i}B ∈ [[K_{2}]], for each i ∈ {1..n}. By the induction hypothesis, ⋀^{K_{2}}[A_{1}B..A_{n}B] ∈ [[K_{2}]]. Moreover, ⋀^{K_{1}→K_{2}}[A_{1}..A_{n}]B ∈ [[K_{2}]] by the saturation of [[K_{2}]], which means that ⋀^{K_{1}→K_{2}}[A_{1}..A_{n}] ∈ [[K_{1}→K_{2}]]. □

Proposition 5.6 (Soundness) If Γ ⊢ T : K, then Γ ⊧ T : K.

Proof: By induction on the derivation of Γ ⊢ T : K.

We consider the case for K-Meet. The other cases follow by similar reasoning. Let T ≡ ⋀^{K}[T_{1}..T_{n}]. We have to consider two cases.

n ≢ 0 We are given Γ ⊢ T_{i} : K for each i ∈ {1..n}, and, by the induction hypothesis, Γ ⊧ T_{i} : K. Let ρ be a valuation such that ρ ⊧ Γ. Then [[T_{i}]]_{ρ} ∈ [[K]], for each

i ∈ {1..n}. By lemma 5.5(2), ⋀^{K}[[[T_{1}]]_{ρ}..[[T_{n}]]_{ρ}] ∈ [[K]].

n ≡ 0 T ≡ ⊤^{K}. Since [[⊤^{K}]]_{ρ} ≡ ⊤^{K}, the result follows by 5.5(1). □

Theorem 5.7 (Strong normalization for →_{β∧}^{−})

Γ ⊢ T : K implies that every (β∧^{−})-reduction sequence starting from T is finite.

Proof: By soundness, Γ ⊧ T : K. Choose ρ_{0} such that ρ_{0}(X) = X. Observe that ρ_{0} ⊧ Γ trivially. Hence T ≡ [[T]]_{ρ_{0}} ∈ [[K]] ⊆ SN. □

Lemma 5.8 If T →_{a} T_{1} and T_{1} →_{β∧}^{−} T_{2}, then there exists S such that T ↠_{β∧}^{−}^{>0} S and S →_{a} T_{2}.

Proof: By induction on the structure of T. □

Corollary 5.9 (a postponement) If T ↠_{a} T_{1} and T_{1} ↠_{β∧}^{−} T_{2}, then there exists S such that T ↠_{β∧}^{−}^{>0} S and S ↠_{a} T_{2}.

Proof: By induction on the generation of T ↠_{a} T_{1}. □ Finally, we can prove strong normalization for →_{β∧}.

Theorem 5.10 (Strong normalization for →_{β∧}) Γ ⊢ T : K implies that every (β∧)- reduction sequence starting from T is finite.

Proof: Let Γ ⊢ T : K. We reason by contradiction. Assume that there is an infinite β∧-reduction sequence starting from T. Then lemma 5.1 and theorem 5.7 imply that there are infinitely many alternations of →_{a} and →_{β∧}^{−} reduction sequences. By corollary 5.9, we can construct an infinite (β∧^{−})-reduction which contradicts theorem 5.7. □

6 Towards a generation principle for subtyping

In this section we start our quest towards a generation principle for the subtyping relation of F_{∧}^{ω}. First, we develop a normal subtyping system, NF_{∧}^{ω}, in which only types in normal form are considered. We then prove that proofs in NF_{∧}^{ω} can be normalized by eliminating transitivity and simplifying reflexivity. This simplification yields an algorithmic presentation, AlgF_{∧}^{ω}, whose rules are syntax directed. Moreover, we prove that AlgF_{∧}^{ω} is indeed an alternative presentation of the F_{∧}^{ω} subtyping relation. Formally, Γ ⊢ S ≤ T if and only if Γ^{nf} ⊢_{Alg} S^{nf} ≤ T^{nf}, when S and T are well-formed (proposition 9.2).

In the solution for the second order lambda calculus presented in [34], the distributivity rules for intersection types are not considered as rewrite rules. For that reason, new syntactic categories have to be defined (composite and individual canonical types) and an auxiliary mapping (flattening) transforms a type into a canonical type. Our solution does not need either new syntactic categories or elaborate auxiliary mappings, since the role played there by canonical types is performed here by types in normal form.

6.1 Normal Subtyping

An important property of derivation systems is the information that a derivable judgement contains about its proofs. This information is essential to produce results which not only state properties about the subproofs, but also help identify ill formed judgements.

As we mentioned in the introduction, in F_{∧}^{ω} we can prove:

W:K, X ≤ ΛY:K.Y:K→K, Z ≤ X:K→K ⊢ X(Z W) ≤ W (1)

Note that X and Z are subtypes of the identity on K, therefore it makes sense for X(Z W) to be a subtype of W. The derivation is as follows: Let Γ ≡ W:K, X ≤ ΛY:K.Y:K→K, Z ≤ X:K→K. For the sake of readability we omit kinding judgements.

Γ ⊢ ok
\overline{S-TVar}
Γ ⊢ X ≤ ΛY:K.Y
\overline{S-OApp}
Γ ⊢ X(Z W) ≤ (ΛY:K.Y)Z W

(ΛY:K.Y)Z W =_{β∧} Z W ; \overline{S-Conv} ; (ΛY:K.Y)Z W ≤ Z W

\overline{S-Trans}
Γ ⊢ X(Z W) ≤ Z W
Γ ⊢ ok ; \overline{S-TVar} ; Γ ⊢ Z ≤ X

Γ ⊢ ok

\overline{S-TVar}

Γ ⊢ X ≤ ΛY:K.Y

\overline{S-Trans}

Γ ⊢ Z ≤ (ΛY:K.Y)
\overline{S-OApp}
Γ ⊢ Z W ≤ (ΛY:K.Y)W

(ΛY:K.Y)W =_{β∧} W ; \overline{S-Conv} ; (ΛY:K.Y)W ≤ W

\overline{S-Trans}
Γ ⊢ Z W ≤ W
Γ ⊢ X(Z W) ≤ Z W Γ ⊢ Z W ≤ W
\overline{S-Trans}
Γ ⊢ X(Z W) ≤ W

This simple example already shows that S-Trans erases information obtained by S-Conv that is not present in the conclusion any longer. A first step towards an algorithm to check the subtyping relation is to design a set of rules in which the derivable judgements contain all the information about their derivations. To this end we define a set of rules, NF_{∧}^{ω}, in which conversion is reduced to a minimum and, as we show in lemma 7.6, transitivity can be eliminated. Both results are proved with a standard cut-elimination argument. This yields a syntax directed subtyping relation, AlgF_{∧}^{ω}, which constitutes a decision procedure for the original system.

In the rest of this section, we present the subtyping system NF_{∧}^{ω}, which uses the context and type formation rules of F_{∧}^{ω}. We define rewriting rules for derivations in NF_{∧}^{ω} (definitions 7.3 and 7.4), and describe a terminating procedure to normalize proofs, which gives, as a consequence, the generation for subtyping (proposition 7.10) and an algorithmic presentation, AlgF_{∧}^{ω} (see section 9).

Finally, in section 9, we show that there is an equivalence between subtyping in F_{∧}^{ω} and subtyping in AlgF_{∧}^{ω}.

We now define the normal subtyping system, NF_{∧}^{ω}. Subtyping statements in NF_{∧}^{ω} are written Γ ⊢_{n} S ≤ T, and S, T, and all types appearing in Γ are in β∧-normal form.

Notation 6.1.1 A, B, and C range over types whose outermost constructor is not an intersection.

Remark 6.1.2 It is an immediate consequence of the β∧-reduction rules that, if T is in β∧-normal form, then T is either X, S→A, ∀X≤S:K.A, ΛX:K.A, A S where A is not an abstraction, or ⋀^{K}[A_{1}..A_{n}]. We frequently use this notation as a reminder of the shape of types in normal form.

We now define lub_{Γ}(S). We prove in lemma 8.1 and corollary 8.1.2, that, when defined, it is the smallest type beyond S with respect to Γ.

Definition 6.1.3 (Least strict Upper Bound)

lub_{Γ}(X) = Γ(X),
lub_{Γ}(T S) = lub_{Γ}(T) S.

Definition 6.1.4 (NF_{∧}^{ω} subtyping rules)

\frac{Γ ⊢ S : K}{Γ ⊢_{n} S ≤ S}  (NS-Refl)

\frac{Γ ⊢_{n} S ≤ T  Γ ⊢_{n} T ≤ U}{Γ ⊢_{n} S ≤ U}  (NS-Trans)

\frac{Γ ⊢_{n} Γ(X) ≤ A  X ≢ A}{Γ ⊢_{n} X ≤ A}  (NS-TVar)

\frac{Γ ⊢_{n} T ≤ S  Γ ⊢_{n} A ≤ B  Γ ⊢ S→A : ⋆}{Γ ⊢_{n} S→A ≤ T →B}  (NS-Arrow)

\frac{Γ, X≤S:K ⊢_{n} A ≤ B  Γ ⊢ ∀X≤S:K.A : ⋆}{Γ ⊢_{n} ∀X≤S:K.A ≤ ∀X≤S:K.B}  (NS-All)

\frac{Γ, X≤⊤^{K}:K ⊢_{n} A ≤ B}{Γ ⊢_{n} ΛX:K.A ≤ ΛX:K.B}  (NS-OAbs)

\frac{Γ ⊢_{n} (lub_{Γ}(A S))^{nf} ≤ B  Γ ⊢ A S : K  A S ≢ B}{Γ ⊢_{n} T S ≤ A}  (NS-OApp)

\frac{∀i ∈ \{1..m\} Γ ⊢_{n} A ≤ T_{i}  Γ ⊢ A : K}{Γ ⊢_{n} A ≤ ⋀^{K}[T_{1}..T_{m}]}  (NS-∀)

\frac{∃j ∈ \{1..n\} Γ ⊢_{n} S_{j} ≤ A  ∀k ∈ \{1..n\} Γ ⊢ S_{k} : K}{Γ ⊢_{n} ⋀^{K}[S_{1}..S_{n}] ≤ A}  (NS-∃)

\frac{∀i ∈ \{1..m\} ∃j ∈ \{1..n\} Γ ⊢_{n} S_{j} ≤ T_{i}  ∀k ∈ \{1..n\} Γ ⊢ S_{k} : K}{Γ ⊢_{n} ⋀^{K}[S_{1}..S_{n}] ≤ ⋀^{K}[T_{1}..T_{m}]}  (NS-∀∃)

7 STRUCTURAL PROPERTIES OF NF_{∧}^{ω} 23

As we mentioned in the introduction, an important factor to develop this system was to consider the distributivity rules of the presentation of F_{∧}^{ω} in [23] as reduction rules instead of subtyping rules. This new point of view suggested that an algorithmic system should, to a certain extent, concentrate on normal forms replacing the conversion rule by reflexivity. Consequently, a derivation of a subtyping statement should involve only types in normal form. But enlightened by the simple (counter)example 1 it is not possible to perform all reductions at once. In other words, the system does not satisfy an S-Conv postponement property. Without using S-Conv it is not possible to derive example 1. Hence, the solution is not as simple as replacing S-Conv by NS-Refl.

In general, the interaction between S-Trans and S-Conv can be analyzed as follows. In S-Trans the metavariable T of the hypothesis is not present in the conclusion, but this is not a problem by itself (a similar situation appears in the simply typed lambda calculus in its application rule and the system is deterministic). The problem is that in the presence of S-Conv the vanishing T can be β∧-convertible to either S or U or to both S and U. What example 1 shows is that S and U may be different normal forms, which means that searching for T is inherently nondeterministic.

We cannot eliminate transitivity completely, we still need it on type variables and on type applications. In F_{≤} [29] transitivity is eliminated and hidden in a richer variable rule in which deciding whether Γ ⊢ X ≤ T when T ≢ X is reduced to deciding whether the bound of X is smaller than or equal to T. The bound of X has the particular property of being the least strict upper bound of X. This observation motivated the definition of our NS-OApp rule, in which we reduce the decision of whether Γ ⊢ A S ≤ B when B ≢ A S, to checking if the least strict upper bound of A S is smaller than or equal to B (See lemma 8.1 and corollary 8.1.2). The least strict upper bound of A S, lub_{Γ}(A S), is obtained from A S by replacing its leftmost innermost variable by the corresponding bound in Γ. In our example, lub_{Γ}(X(Z W)) is (ΛY:K.Y)(Z W). Consequently, lub_{Γ}(A S) may be other than a normal form. That is the reason we normalize it. The strength of the conversion rule that is not captured by reflexivity is hidden in this normalization step. Since A S is a well kinded type, by the free variables lemma (lemma 4.3), FTV(A S) ⊆ dom(Γ). Therefore, lub_{Γ}(A S) is defined. By lemma 8.1(1), lub_{Γ}(A S) is well-kinded, and since well-kinded types are strongly normalizing, its normal form exists. The rules S-Meet-LB and S-Meet-G are replaced by NS-∃, NS-∀, and NS-∀∃. Except for the restriction of types being in normal

form NS-Arrow, NS-All, and NS-OAbs have the same form as S-Arrow, S-All, and

S-OAbs respectively.

7 Structural properties of NF_{∧}^{ω}

This section establishes a number of structural properties of NF_{∧}^{ω}. The proofs of lemmas 7.1 and 7.2 are similar to those of the corresponding properties for F_{∧}^{ω}.

Lemma 7.1 If Γ ⊢_{n} S ≤ T and Γ_{1} is a prefix of Γ, then Γ_{1} ⊢ ok as a subderivation. Moreover, the subderivation is strictly shorter.

Lemma 7.2 (Weakening/Permutation) Let Γ and Γ′ be contexts such that Γ ⊆ Γ′ and Γ′ ⊢ ok. Then Γ ⊢_{n} S ≤ T implies Γ′ ⊢_{n} S ≤ T.

We present rewriting rules on derivations to simplify instances of NS-Refl and NS-Trans. We give a terminating strategy to transform a given derivation into a derivation with occurrences of NS-Refl only applied to type variables or type applications and without occurrences of NS-Trans. To improve readability we omit kinding judgements in the transitivity elimination rules which appear as hypothesis in the redex or in a proper subderivation of the missing ones, as we proved in generation for kinding (proposition 4.8). The derivations of the kinding judgements of each reduct of the reflexivity rules are proper subderivations of the kinding judgements in its redex.

Definition 7.3 (Reflexivity simplification rules)

1. Γ ⊢ S→A : ⋆ \overline{NS-Refl}

Γ ⊢_{n} S→A ≤ S→A

⇒_{R} Γ ⊢ S : ⋆ ; \overline{NS-Refl} ; Γ ⊢_{n} S ≤ S Γ ⊢ A : ⋆ ; \overline{NS-Refl} ; Γ ⊢_{n} A ≤ A

\overline{NS-Arrow}
Γ ⊢_{n} S→A ≤ S→A

2. Γ ⊢ ∀X≤S:K.A : ⋆ \overline{NS-Refl}

Γ ⊢_{n} ∀X≤S:K.A ≤ ∀X≤S:K.A

⇒_{R}

Γ, X≤S:K ⊢ A : ⋆
\overline{NS-All}

3.

⇒_{R}

\overline{NS-OAbs}

4. Γ ⊢ ⋀^{K}[A_{1}..A_{n}] : K \overline{NS-Refl}

⇒_{R}

\overline{NS-Refl}

\overline{NS-Refl} Γ, X≤S:K ⊢_{n} A ≤ A Γ ⊢_{n} ∀X≤S:K.A ≤ ∀X≤S:K.A Γ ⊢ ΛX:K.A : K→K′

\overline{NS-Refl} Γ ⊢_{n} ΛX:K.A ≤ ΛX:K.A

Γ, X:K ⊢ A : K′

\overline{NS-Refl} Γ, X:K ⊢_{n} A ≤ A Γ ⊢_{n} ΛX:K.A ≤ ΛX:K.A Γ ⊢_{n} ⋀^{K}[A_{1}..A_{n}] ≤ ⋀^{K}[A_{1}..A_{n}]

Γ ⊢ A_{i} : K Γ ⊢_{n} A_{i} ≤ A_{i} ∀i ∈ {1..n}

\overline{NS-∀∃} Γ ⊢_{n} ⋀^{K}[A_{1}..A_{n}] ≤ ⋀^{K}[A_{1}..A_{n}]

7 STRUCTURAL PROPERTIES OF NF_{∧}^{ω} 25 Definition 7.4 (Transitivity elimination rules)

1. Γ ⊢ S : K ; \overline{NS-Refl} ; Γ ⊢_{n} S ≤ S Γ ⊢_{n} S ≤ T

\overline{NS-Trans}
Γ ⊢_{n} S ≤ T

⇒_{T} Γ ⊢_{n} S ≤ T

2. Γ ⊢_{n} S ≤ T Γ ⊢ T : K ; \overline{NS-Refl} ; Γ ⊢_{n} T ≤ T

\overline{NS-Trans}
Γ ⊢_{n} S ≤ T

⇒_{T} Γ ⊢_{n} S ≤ T

3.

Γ ⊢_{n} Γ(X) ≤ A

\overline{NS-TVar}

Γ ⊢_{n} X ≤ A Γ ⊢_{n} A ≤ B

\overline{NS-Trans}
Γ ⊢_{n} X ≤ B

⇒_{T}

Γ ⊢_{n} Γ(X) ≤ A Γ ⊢_{n} A ≤ B
\overline{NS-Trans}
Γ ⊢_{n} Γ(X) ≤ B
\overline{NS-TVar}
Γ ⊢_{n} X ≤ B

4.

Γ ⊢_{n} T ≤ S Γ ⊢_{n} A ≤ B
\overline{NS-Arrow}

Γ ⊢_{n} S→A ≤ T →B

Γ ⊢_{n} U ≤ T Γ ⊢_{n} B ≤ C
\overline{NS-Arrow}
Γ ⊢_{n} T →B ≤ U→C
\overline{NS-Trans}
Γ ⊢_{n} S→A ≤ U→C

⇒_{T}

Γ ⊢_{n} U ≤ T Γ ⊢_{n} T ≤ S
\overline{NS-Trans}
Γ ⊢_{n} U ≤ S

Γ ⊢_{n} A ≤ B Γ ⊢_{n} B ≤ C
\overline{NS-Trans}
Γ ⊢_{n} A ≤ C
\overline{NS-Arrow}
Γ ⊢_{n} S→A ≤ U→C

5. Γ, X≤S:K ⊢_{n} A ≤ B ; \overline{NS-All} ; Γ ⊢_{n} ∀X≤S:K.A ≤ ∀X≤S:K.B Γ, X≤S:K ⊢_{n} B ≤ C ; \overline{NS-All} ; Γ ⊢_{n} ∀X≤S:K.B ≤ ∀X≤S:K.C

\overline{NS-Trans}
Γ ⊢_{n} ∀X≤S:K.A ≤ ∀X≤S:K.C

⇒_{T}

Γ, X≤S:K ⊢_{n} A ≤ B Γ, X≤S:K ⊢_{n} B ≤ C
\overline{NS-Trans}
Γ, X≤S:K ⊢_{n} A ≤ C
\overline{NS-All}
Γ ⊢_{n} ∀X≤S:K.A ≤ ∀X≤U:K.C

6.

Γ, X:K ⊢_{n} A ≤ B
\overline{NS-OAbs}

Γ ⊢_{n} ΛX:K.A ≤ ΛX:K.B

Γ, X:K ⊢_{n} B ≤ C
\overline{NS-OAbs}
Γ ⊢_{n} ΛX:K.B ≤ ΛX:K.C
\overline{NS-Trans}

Γ ⊢_{n} ΛX:K.A ≤ ΛX:K.C

7 STRUCTURAL PROPERTIES OF NF_{∧}^{ω} 26 ⇒_{T}

Γ, X:K ⊢_{n} A ≤ B Γ, X:K ⊢_{n} B ≤ C
\overline{NS-Trans}
Γ, X:K ⊢_{n} A ≤ C
\overline{NS-OAbs}
Γ ⊢_{n} ΛX:K.A ≤ ΛX:K.C

7.

Γ ⊢_{n} lub_{Γ}(A S)^{nf} ≤ B

\overline{NS-OApp}

Γ ⊢_{n} A S ≤ B Γ ⊢_{n} B ≤ C

\overline{NS-Trans}
Γ ⊢_{n} A S ≤ C

⇒_{T}

Γ ⊢_{n} (lub_{Γ}(A S))^{nf} ≤ B Γ ⊢_{n} B ≤ C
\overline{NS-Trans}
Γ ⊢_{n} lub_{Γ}(A S))^{nf} ≤ C
\overline{NS-OApp}
Γ ⊢_{n} A S ≤ C

8. ∀i ∈ \{1..n\} Γ ⊢_{n} A ≤ A_{i} ; \overline{NS-∀} ; Γ ⊢_{n} A ≤ ⋀^{K}[A_{1}..A_{n}] ∃j ∈ \{1..n\} Γ ⊢_{n} A_{j} ≤ B ; \overline{NS-∃} ; Γ ⊢_{n} ⋀^{K}[A_{1}..A_{n}] ≤ B

\overline{NS-Trans}
Γ ⊢_{n} A ≤ B

⇒_{T} ∃j ∈ {1..n} Γ ⊢_{n} A ≤ A_{j} Γ ⊢_{n} A_{j} ≤ B \overline{NS-Trans}

Γ ⊢_{n} A ≤ B

9. Γ ⊢_{n} A ≤ B ∀i ∈ \{1..n\} Γ ⊢_{n} B ≤ A_{i} ; \overline{NS-∀} ; Γ ⊢_{n} B ≤ ⋀^{K}[A_{1}..A_{n}]

\overline{NS-Trans}

Γ ⊢_{n} A ≤ ⋀^{K}[A_{1}..A_{n}]

⇒_{T}

∀i ∈ {1..n} Γ ⊢_{n} A ≤ B Γ ⊢_{n} B ≤ A_{i}
\overline{NS-Trans}
∀i ∈ {1..n} Γ ⊢_{n} A ≤ A_{i}
\overline{NS-∀}
Γ ⊢_{n} A ≤ ⋀^{K}[A_{1}..A_{n}]

10. ∃j ∈ \{1..n\} Γ ⊢_{n} A_{j} ≤ B ; \overline{NS-∃} ; Γ ⊢_{n} ⋀^{K}[A_{1}..A_{n}] ≤ B Γ ⊢_{n} B ≤ A

\overline{NS-Trans}
Γ ⊢_{n} ⋀^{K}[A_{1}..A_{n}] ≤ A

⇒_{T}

∃j ∈ {1..n} Γ ⊢_{n} A_{j} ≤ B Γ ⊢_{n} B ≤ A
\overline{NS-Trans}
∃j ∈ {1..n} Γ ⊢_{n} A_{j} ≤ A
Γ ⊢_{n} ⋀^{K}[A_{1}..A_{n}] ≤ A

\overline{NS-∃}

11. ∃j ∈ \{1..m\} Γ ⊢_{n} A_{j} ≤ A ; \overline{NS-∃} ; Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ A ∀i ∈ \{1..n\} Γ ⊢_{n} A ≤ B_{i} ; \overline{NS-∀} ; Γ ⊢_{n} A ≤ ⋀^{K}[B_{1}..B_{n}]

\overline{NS-Trans}
Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ ⋀^{K}[B_{1}..B_{n}]

⇒_{T}

∃j ∈ {1..m} Γ ⊢_{n} A_{j} ≤ A ∀i ∈ {1..n} Γ ⊢_{n} A ≤ B_{i}
\overline{NS-Trans}
∀i ∈ {1..n} ∃j ∈ {1..m} Γ ⊢_{n} A_{j} ≤ B_{i}
\overline{NS-∀∃}
Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ ⋀^{K}[B_{1}..B_{n}]

12. \begin{matrix}∀i ∈ \{1..n\} ∃j ∈ \{1..m\} Γ ⊢_{n} A_{j} ≤ B_{i} \\ Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ ⋀^{K}[B_{1}..B_{n}] \end{matrix} ∀k ∈ \{1..r\} ∃i ∈ \{1..n\} Γ ⊢_{n} B_{i} ≤ C_{k} ; \overline{NS-∀∃} ; Γ ⊢_{n} ⋀^{K}[B_{1}..B_{n}] ≤ ⋀^{K}[C_{1}..C_{r}]

\overline{NS-Trans}
Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ ⋀^{K}[C_{1}..C_{r}]

⇒_{T}

∀k ∈ {1..r} ∃i ∈ {1..n} ∃j ∈ {1..m} Γ ⊢_{n} A_{j} ≤ B_{i}  Γ ⊢_{n} B_{i} ≤ C_{k}
\overline{NS-Trans}
∀k ∈ {1..r} ∃j ∈ {1..m} Γ ⊢_{n} A_{j} ≤ C_{k}
\overline{NS-∀∃}
Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ ⋀^{K}[C_{1}..C_{r}]

13. ∀i ∈ \{1..n\} ∃j ∈ \{1..m\} Γ ⊢_{n} A_{j} ≤ B_{i} ; \overline{NS-∀∃} ; Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ ⋀^{K}[B_{1}..B_{n}] ∃i ∈ \{1..n\} Γ ⊢_{n} B_{i} ≤ C ; \overline{NS-∃} ; Γ ⊢_{n} ⋀^{K}[B_{1}..B_{n}] ≤ C

\overline{NS-Trans}
Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ C

⇒_{T}

∃j ∈ {1..m} ∃i ∈ {1..n} Γ ⊢_{n} A_{j} ≤ B_{i} Γ ⊢_{n} B_{i} ≤ C
\overline{NS-Trans}
∃j ∈ {1..m} Γ ⊢_{n} A_{j} ≤ C
\overline{NS-∃}
Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ C

14. ∀i ∈ \{1..n\} Γ ⊢_{n} A ≤ B_{i} ; \overline{NS-∀} ; Γ ⊢_{n} A ≤ ⋀^{K}[B_{1}..B_{n}] ∀k ∈ \{1..r\} ∃i ∈ \{1..n\} Γ ⊢_{n} B_{i} ≤ C_{k} ; \overline{NS-∀∃} ; Γ ⊢_{n} ⋀^{K}[B_{1}..B_{n}] ≤ ⋀^{K}[C_{1}..C_{r}]

\overline{NS-Trans}
Γ ⊢_{n} A ≤ ⋀^{K}[C_{1}..C_{r}]

⇒_{T}

∀k ∈ {1..r} ∃i ∈ {1..n} Γ ⊢_{n} A ≤ B_{i}  Γ ⊢_{n} B_{i} ≤ C_{k}
\overline{NS-Trans}
∀k ∈ {1..r} Γ ⊢_{n} A ≤ C_{k}
\overline{NS-∀}
Γ ⊢_{n} A ≤ ⋀^{K}[C_{1}..C_{r}]

A derivation of a subtyping statement is in refl-normal form if it has no reflexivity redexes and it is in trans-normal form if it has no transitivity redexes, and it is in normal form if it has neither reflexivity nor transitivity redexes. The elimination of NS-Trans, and the simplification of NS-Refl follow a standard cut-elimination argument.

Lemma 7.5 (Reflexivity simplification) Let D be a derivation of a subtyping statement with only one application of NS-Refl. Then D has a refl-normal form.

Proof: Same argument as in lemma 7.6. □

Lemma 7.6 (Transitivity elimination) Let D be a derivation of a subtyping statement with only one application of NS-Trans. Then D has a trans-normal form.

Proof: By induction on the size of D following a case analysis of the last rule of D. If the last rule is not NS-Trans, then the result follows by the induction hypothesis. Otherwise we consider all possible last rules of the derivations of the premises and note that each possible configuration determines a trans-redex. Finally, observe that each reduction yields either a derivation in normal form or shorter derivations with only one occurrence of NS-Trans in which case the result follows by the induction hypothesis. □

An immediate corollary of this last result is that transitivity elimination terminates. Given a derivation D of Γ ⊢_{n} S ≤ T, iterate the previous lemma on all subderivations of D that have only one NS-Trans application. The number of times the lemma is applied is equal to the number of occurrences of NS-Trans in D. Furthermore, lemma 7.5 implies that reflexivity simplification terminates. The simplification rules are such that transitivity simplification rules do not create new reflexivity redexes. Therefore, we can reduce all instances of NS-Refl first and then all instances of NS-Trans, which is a terminating procedure to normalize a derivation. Consequently, we have proved the following corollary.

Corollary 7.7 (Existence of normal derivations) Given a derivation of Γ ⊢_{n} S ≤ T. Then there exists a derivation in normal form of Γ ⊢_{n} S ≤ T.

Lemma 7.8

1. A derivation in normal form whose last rule is NS-Refl is either a proof of Γ ⊢_{n} X ≤ X or Γ ⊢_{n} A T ≤ A T.

2. If the last rule of a subtyping derivation D is NS-Trans, then D is not in normal form.

Proof:

1. According to the reflexivity elimination rules, any other possible NS-Refl application is a redex.

2. By case analysis of the last rules of the premises of the last rule of D. In each case the result follows either by the induction hypothesis or because the last rule of at least one of the derivations of the premises of D constitutes a redex. □

We can summarize the previous results as follows.

Corollary 7.9 If Γ ⊢_{n} S ≤ T, then there exists a proof of the same judgement with no applications of NS-Trans and in which NS-Refl is only applied to type variables and type applications.

A consequence of the normalization of proofs is the following generation result. Proposition 7.10 (Generation for normal subtyping)

1. Γ ⊢_{n} X ≤ B implies X ≡ B and Γ ⊢ X : K for some K, or Γ ⊢_{n} Γ(X) ≤ B.

2. Γ ⊢_{n} S→A ≤ B implies B ≡ T →C, Γ ⊢_{n} T ≤ S, Γ ⊢_{n} A ≤ C, and Γ ⊢ S→A : ⋆.

3. Γ ⊢_{n} ∀X≤S:K.A ≤ B implies B ≡ ∀X≤S:K.C, Γ, X≤S:K ⊢_{n} A ≤ C, and Γ ⊢ ∀X≤S:K.A : ⋆.

4. Γ ⊢_{n} ΛX:K.A ≤ B implies B ≡ ΛX:K.C and Γ, X≤⊤^{K}:K ⊢_{n} A ≤ C.

5. Γ ⊢_{n} A S ≤ B implies B ≡ A S, or Γ ⊢_{n} (lub_{Γ}(A S))^{nf} ≤ B, and Γ ⊢ A S : K.

6. Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ B implies that there exists j ∈ {1..m} such that Γ ⊢_{n} A_{j} ≤ B and ∀k ∈ {1..m} Γ ⊢ A_{k} : K.

7. Γ ⊢_{n} A ≤ ⋀^{K}[B_{1}..B_{n}] implies that for each i ∈ {1..n} Γ ⊢_{n} A ≤ B_{i} and Γ ⊢ A : K.

8. Γ ⊢_{n} ⋀^{K}[A_{1}..A_{m}] ≤ ⋀^{K}[B_{1}..B_{n}] implies that for each i ∈ {1..n} there exists j ∈

{1..m} such that Γ ⊢_{n} A_{j} ≤ B_{i} and ∀k ∈ {1..m} Γ ⊢ A_{k} : K. Moreover, given a normal proof of any of the antecedents, the proofs of the consequents are proper subderivations. Proof: In each case, given a proof of the antecedent, there is also a proof in normal form. Due to lemma 7.8(2), such a derivation cannot end with an application of NS-Trans, and, because of lemma 7.8(1), if it ends with NS-Refl, then it is a derivation of a subtyping statement between type variables or type applications. Finally, the result follows by inspection of the other rules. □ Lemma 7.11

1. Γ ⊢_{n} T ≤ ⋀^{K}[A_{1}..A_{n}] if and only if Γ ⊢_{n} T ≤ A_{k} for each k ∈ {1..n} .

2. Γ ⊢_{n} T ≤ ⋀^{K}[A_{1}..A_{n}] if and only if Γ ⊢_{n} T ≤ ⋀^{K}[A_{k}] for each k ∈ {1..n} .

3. Let Γ ⊢ ⋀^{K}[A_{1}..A_{n}] : K. Then Γ ⊢_{n} ⋀^{K}[A_{1}..A_{n}] ≤ T if and only if Γ ⊢_{n} A_{k} ≤ T for

some k ∈ {1..n} . Proof: By induction on derivations, using lemma 7.7 and generation. □

8 Equivalence of ordinary and normal subtyping

In this section, we show that a subtyping statement is derivable in F_{∧}^{ω} if and only if the corresponding normalized statement is derivable in NF_{∧}^{ω}. This equivalence is proved in theorem 8.9. As usual, we need some auxiliary properties and definitions, among which we can highlight propositions 8.2 (Soundness) and 8.8 (Completeness).

Lemma 8.1 Let lub_{Γ}(S) be defined. Then

1. Γ ⊢ S : K implies Γ ⊢ lub_{Γ}(S) : K.

2. Γ ⊢ S ≤ lub_{Γ}(S).

Proof: Item 1 follows by induction on derivations, while item 2 follows by induction on the structure of S. □

Proposition 8.2 (Soundness) If Γ ⊢_{n} S ≤ T, then Γ ⊢ S ≤ T.

Proof: By induction on the derivation of Γ ⊢_{n} S ≤ T. We consider here a few illustrative cases.

NS-TVar By the induction hypothesis, S-TVar and S-trans.

NS-OApp By the induction hypothesis, lemma 8.1(2), S-Conv and S-Trans.

NS-∀∃ We are given that for each k in {1..n} Γ ⊢ A_{k} : K, and for each i in {1..m} there is a j in {1..n} such that Γ ⊢_{n} A_{j} ≤ B_{i}. By K-Meet, Γ ⊢ ⋀^{K}[A_{1}..A_{n}] : K, and, by S-Meet-LB, Γ ⊢ ⋀^{K}[A_{1}..A_{n}] ≤ A_{k} for each k. Hence the result follows by the induction hypothesis, S-Trans and S-Meet-G. □

Note that the cases for type variable and type application reveal the fact that NS-TVar and NS-OApp hide steps of transitivity.

The following lemma says that empty intersections, ⊤^{K}, are maximal elements of the subtyping order.

Lemma 8.3

1. Γ ⊢ T : K implies Γ ⊢_{n} T ≤ ⊤^{K}.

2. Γ ⊢ T : K implies Γ ⊢ T ≤ ⊤^{K}.

Proof: Statement 1 follows by the cases m = 0 in NS-∀ and NS-∀∃. Statement 2 is the case n = 0 in S-Meet-G. □

Lemma 8.4

1. Γ ⊢ ok implies Γ^{nf} ⊢ ok.

2. Γ ⊢ T : K implies Γ^{nf} ⊢ T : K.

3. Γ ⊢ S ≤ T implies Γ^{nf} ⊢ S ≤ T.

4. Let Γ_{1}, Γ_{2} ⊢ ok. Then Γ_{1}^{nf}, Γ_{2} ⊢ T : K implies Γ_{1}, Γ_{2} ⊢ T : K.

5. Let Γ_{1}, Γ_{2} ⊢ ok. Then Γ_{1}^{nf}, Γ_{2} ⊢ S ≤ T implies Γ_{1}, Γ_{2} ⊢ S ≤ T.

6. Let Γ ⊢ S, T : K. Then Γ^{nf} ⊢ S^{nf} ≤ T^{nf} if and only if Γ ⊢ S ≤ T.

Proof: Statements 1 and 2 follow by simultaneous induction on the size of derivations using lemma 4.16. Statement 3 follows by induction on the derivation of Γ ⊢ S ≤ T using part 1, part 2, and lemma 4.16. Statement 4 follows by induction on the derivation of Γ_{1}^{nf}, Γ_{2} ⊢ T : K. Item 5 follows by induction on the derivation of Γ_{1}^{nf}, Γ_{2} ⊢ S ≤ T, using part 4. Item 6 is a corollary of part 3, part 5 and lemma 4.15. □

In the last lemma, items 1, 2, and 3 show that well formation of contexts, kinding judgements, and subtyping judgements are invariant under normalization of contexts, while items 4 and 5 are the converse of 2 and 3 respectively.

The following lemma states that S-TVar is an admissible rule in NF_{∧}^{ω}.

Lemma 8.5 Let Γ be a context in normal form such that Γ ⊢ ok and Y ∈ dom(Γ). Then Γ ⊢_{n} Y ≤ Γ(Y).

Proof: Let Γ ≡ Γ_{1}, Y ≤ T:K, Γ_{2}. By lemma 4.2, Γ_{1} ⊢ T : K. If T is not an intersection, then, by NS-Refl and NS-TVar, we have Γ ⊢_{n} Y ≤ T. If T ≡ ⋀^{K′}[B_{1}..B_{m}], then by generation for kinding and uniqueness of kinds, Γ ⊢ B_{i} : K for each i and K ≡ K′. By NS-Refl, Γ ⊢_{n} B_{i} ≤ B_{i} for each i. Then, by NS-∃ and NS-TVar, it follows that Γ ⊢_{n} Y ≤ B_{i} for each i, and, by NS-∀, Γ ⊢_{n} Y ≤ T. □

The following lemma shows that the normal subtyping system has the substitution property.

Lemma 8.6 (Substitution) If Γ ⊢ U : K and Γ, X:K, Γ′ ⊢_{n} S ≤ T, then Γ, (Γ′[X←U])^{nf} ⊢_{n} (S[X←U])^{nf} ≤ (T [X←U])^{nf}.

Proof: By induction on the derivation of Γ, X:K, Γ′ ⊢_{n} S ≤ T. For the sake of clarity, we sometimes leave out kinding judgements and their justifications which follow easily from the structural properties in section 4. We show here a couple of representative cases. Let Γ′′ ≡ Γ, X:K, Γ′.

NS-TVar We are given Γ′′ ⊢_{n} Γ′′(Y) ≤ A. We have to consider three cases.

1. Y ≡ X. By subject reduction, Γ ⊢ U^{nf} : K, and by lemma 8.3(1), it follows that Γ ⊢_{n} U^{nf} ≤ ⊤^{K}. By weakening, it follows that Γ, (Γ′[X←U])^{nf} ⊢_{n} U^{nf} ≤ ⊤^{K} and, by the induction hypothesis, it follows that Γ, (Γ′[X←U])^{nf} ⊢_{n} ⊤^{K} ≤ (A[X←U])^{nf}. Finally, the result follows by NS-Trans.

2. Y ∈ dom(Γ). By the free variables lemma, X ∉ FV(Γ(Y)) and X ≢ Y. By lemmas 4.10, 8.4(1), and 8.5, it follows that Γ, (Γ′[X←U])^{nf} ⊢_{n} Y ≤ Γ(Y), and, by the induction hypothesis, it follows that Γ, (Γ′[X←U])^{nf} ⊢_{n} Γ(Y) ≤ (A[X←U])^{nf}. Finally, the result follows by NS-Trans.

3. Y ∈ dom(Γ′). By the induction hypothesis, it follows that

Γ, (Γ′[X←U])^{nf} ⊢_{n} (Γ′(Y)[X←U])^{nf} ≤ (A[X←U])^{nf}.

By lemmas 4.10, 8.4(1), and 8.5, Γ, (Γ′[X←U])^{nf} ⊢_{n} Y ≤ (Γ, (Γ′[X←U])^{nf})(Y). Furthermore, (Γ, (Γ′[X←U])^{nf})(Y) = (Γ′(Y)[X←U])^{nf}. Hence the result follows

by NS-Trans.

NS-Arrow We are given that Γ′′ ⊢_{n} T ≤ S and Γ′′ ⊢_{n} A ≤ B. By the induction hypothesis, Γ, (Γ′[X←U])^{nf} ⊢_{n} (T [X←U])^{nf} ≤ (S[X←U])^{nf} and Γ, (Γ′[X←U])^{nf} ⊢_{n} (A[X←U])^{nf} ≤ (B[X←U])^{nf}. There are four cases to consider, since (A[X←U])^{nf} and (B[X←U])^{nf} may be intersections or not. We shall consider only two of them to illustrate the proof method.

1. (A[X←U])^{nf} and (B[X←U])^{nf} are not intersections. Then the result follows by applying NS-Arrow.

2. (A[X←U])^{nf} = ⋀^{⋆}[C_{1}..C_{n}] and (B[X←U])^{nf} is not an intersection. Then we have that ((T →B)[X←U])^{nf} = (T [X←U])^{nf}→(B[X←U])^{nf} and ((S→A)[X←U])^{nf}

= ⋀^{⋆}[(S[X←U])^{nf}→C_{1}..(S[X←U])^{nf}→C_{n}]. By lemma 7.10, it follows that for some i Γ, (Γ′[X←U])^{nf} ⊢_{n} C_{i} ≤ (B[X←U])^{nf}. Applying NS-Arrow, Γ, (Γ′[X←U])^{nf} ⊢_{n} (S[X←U])^{nf}→C_{i} ≤ (T [X←U])^{nf}→(B[X←U])^{nf}. Finally, the result follows by NS-∃. □

This substitution lemma is the key result we use in proving that S-OApp has a corresponding admissible rule in NF_{∧}^{ω}.

Lemma 8.7 Γ ⊢ S U : K. Then Γ ⊢_{n} S ≤ T implies Γ ⊢_{n} (S U)^{nf} ≤ (T U)^{nf}.

Proof: By induction on the derivation of Γ ⊢_{n} S ≤ T, assuming a derivation in normal form. The cases for NS-Arrow and NS-All are impossible because of the assumption Γ ⊢ S U : K. We show here the interesting cases.

NS-TVar We are given Γ ⊢_{n} Γ(X) ≤ A. By the induction hypothesis, Γ ⊢_{n} (Γ(X)U)^{nf} ≤ (AU)^{nf}. We have to consider two cases.

(AU)^{nf} ≡ B By NS-OApp.

(AU)^{nf} ≡ ⋀^{K}[A_{1}..A_{n}] By lemma 7.11, Γ ⊢_{n} (Γ(X)U)^{nf} ≤ A_{k} for each k in {1..n}. By NS-OApp, Γ ⊢_{n} X U ≤ (A_{k}) for each k, which, by NS-∀, implies Γ ⊢_{n} X U ≤

(AU)^{nf}.

NS-OAbs We are given Γ, X:K ⊢_{n} A ≤ B. By the substitution lemma 8.6, it follows that Γ ⊢_{n} (A[X←U])^{nf} ≤ (B[X←U])^{nf}. On the other hand, we have that (ΛX:K.A)U →_{β∧} A[X←U] and (ΛX:K.B)U →_{β∧} B[X←U]. Finally, the result follows by the uniqueness of normal forms. □

Proposition 8.8 (Completeness) If Γ ⊢ S ≤ T, then Γ^{nf} ⊢_{n} S^{nf} ≤ T^{nf}.

Proof: By induction on the derivation of Γ ⊢ S ≤ T, using lemma 8.7 for the case of

S-OApp. □

Theorem 8.9 (Equivalence of ordinary and normal subtyping) Let Γ ⊢ S : K and Γ ⊢ T : K. Then Γ ⊢ S ≤ T if and only if Γ^{nf} ⊢_{n} S^{nf} ≤ T^{nf}.

Proof: ⇒) By completeness (8.8). ⇐) By soundness (8.2), it follows that Γ^{nf} ⊢ S^{nf} ≤ T^{nf}, and, by lemma 8.4(6), it follows that Γ ⊢ S ≤ T. □

8.1 Least strict upper bound

So far we only used that lub_{Γ}(S) is an upper bound of S in the context Γ (See lemma 8.1(2)). We can now give the final motivation of the name we chose, showing that if lub_{Γ}(S) is defined and T ≠_{β∧} S, then Γ ⊢ S ≤ T implies Γ ⊢ lub_{Γ}(S) ≤ T. We first show that the corresponding property holds for the normalized system.

Lemma 8.1.1 Let lub_{Γ}(S) be defined. Then

1. If S ↠_{β∧} S′ and Γ ↠_{β∧} Γ′, then lub_{Γ}(S) ↠_{β∧} lub_{Γ′}(S′).

2. If Γ ⊢_{n} S ≤ T, then Γ ⊢_{n} lub_{Γ}(S)^{nf} ≤ T or S ≡ T.

Proof:

1. By induction on the structure of S, observing that if lub_{Γ}(S) is defined, so is lub_{Γ′}(S′).

2. By induction on the derivation of Γ ⊢_{n} S ≤ T. It is immediate for the case NS-Refl; for NS-Arrow, NS-All, and NS-OAbs lub_{Γ}(S) is not defined; for the other rules the result follows using the induction hypothesis. □

Corollary 8.1.2 Let lub_{Γ}(S) be defined. Then Γ ⊢ S ≤ T and T ≠_{β∧} S implies Γ ⊢ lub_{Γ}(S) ≤ T.

Proof: By completeness, it follows that Γ^{nf} ⊢_{n} S^{nf} ≤ T^{nf}. By lemma 8.1.1(2), Γ^{nf} ⊢_{n} (lub_{Γnf}(S^{nf}))^{nf} ≤ T^{nf}, because S^{nf} ≢ T^{nf}. By soundness, it follows that Γ^{nf} ⊢ (lub_{Γnf}(S^{nf}))^{nf} ≤ T^{nf}, which is equivalent to Γ ⊢ lub_{Γnf}(S^{nf}) ≤ T by lemma 8.4(6). Finally, (using lemmas 8.1(1) and 4.11, and proposition 4.18 to get the corresponding kinding judgements) it follows that Γ ⊢ lub_{Γ}(S) ≤ T by lemma 8.1.1(1), S-Conv and S-Trans. □

9 A SUBTYPE CHECKING ALGORITHM, ALGF_{∧}^{ω} 34

8.2 Example

In this section, we give the derivation in NF_{∧}^{ω} of the example 1 mentioned in the introduction and in section 6.1.

Let Γ ≡ W:K, X ≤ ΛY:K.Y:K→K, Z ≤ X:K→K. We present a proof in the normal system of Γ^{nf} ⊢_{n} X(Z W)^{nf} ≤ W^{nf}, Which is the translation of Γ ⊢ X(Z W) ≤ W. Observe that Γ^{nf} ≡ Γ, (X(Z W))^{nf} ≡ X(Z W), and W^{nf} ≡ W. For the sake of readability we omit kinding judgements. Observe that the derivation in normal form in NF_{∧}^{ω} is substantially shorter than the one in F_{∧}^{ω} shown in section 6.1.

Γ ⊢ W : K
\overline{NS-Refl}
Γ ⊢_{n} ((ΛY:K.Y)W)^{nf} ≤ W
\overline{NS-OApp}
Γ ⊢_{n} X W ≤ W
\overline{NS-OApp}
Γ ⊢_{n} ((ΛY:K.Y)(Z W))^{nf} ≤ W
\overline{NS-OApp}
Γ ⊢_{n} X(Z W) ≤ W

9 A subtype checking algorithm, AlgF_{∧}^{ω}

As it stands, NF_{∧}^{ω} as defined in section 6.1 is not a deterministic algorithm, because its rules are not syntax directed. Fortunately, we are not far away from an algorithmic presentation. In fact, corollary 7.9 is the bridge to the algorithmic presentation of the subtyping relation, AlgF_{∧}^{ω}, which states that transitivity steps can be eliminated and reflexivity steps can be simplified. AlgF_{∧}^{ω} is obtained from NF_{∧}^{ω} by removing NS-Trans and restricting NS-Refl to type variables and type applications.

The new reflexivity rules are:

\frac{Γ ⊢ X : K}{Γ ⊢_{Alg} X ≤ X}  (AlgS-TVarRefl)

\frac{Γ ⊢ T S : K}{Γ ⊢_{Alg} T S ≤ T S}  (AlgS-OAppRefl)

Lemma 9.1 (Equivalence of normal and algorithmic subtyping)

Let Γ ⊢ S, T : K. Then Γ ⊢_{n} S ≤ T if and only if Γ ⊢_{Alg} S ≤ T.

Proof: (⇒) By corollary 7.9. (⇐) Immediate. □

We have thereby proved that AlgF_{∧}^{ω} is indeed a sound and complete algorithm to compute F_{∧}^{ω}’s subtyping relation.

Proposition 9.2 (Equivalence of ordinary and algorithmic subtyping)

Let Γ ⊢ S : K and Γ ⊢ T : K. Then Γ ⊢ S ≤ T if and only if Γ^{nf} ⊢_{Alg} S^{nf} ≤ T^{nf}.

Proof: By the equivalence of ordinary and normal subtyping (theorem 8.9) and the equivalence of normal and algorithmic subtyping (lemma 9.1). □

10 Type checking and type reconstruction

Given a context Γ, a term e, and a type T, type checking consists of analyzing whether the judgement Γ ⊢ e : T is derivable from a given set of inference rules. Type checking algorithms for lambda calculi, unless they are formulated using Gentzen’s sequent calculus style, involve guessing the type of subterms. For example, when e is e_{1} e_{2}, the type of e_{2} is not necessarily a subexpression of T, and in order to corroborate or to refute the assertion Γ ⊢ e : T we need to infer a type for e_{2}.

In this section, we present an algorithm for inferring minimal types in F_{∧}^{ω}. Given Γ and e, the type S constructed by the algorithm is a subtype of every T such that Γ ⊢ e : T. In this way, we reduce the problem of whether Γ ⊢ e : T to that of inferring a type S such that Γ ⊢ e : S and Γ ⊢ S ≤ T. Solving this problem involves not only the typing rules but all the inference rules of F_{∧}^{ω}: the rule T-Subsumption depends on a subtyping judgement, the rule T-Var depends on an ok judgement, and the ok judgements depend on kinding judgements. Consequently, type checking uses the full power of the F_{∧}^{ω} system.

As an example, consider type checking the following judgement:

Γ, X ≤ T_{1}→T_{2}, f:X, a:T_{1} ⊢ f a : T_{2}.

The application f a can only be formed if f has an arrow type. Using T-Var we can assign type X to f, which means that in order to obtain an arrow type for f we have to replace X by its bound, which has the right form. Observe how this replacement is performed by T-Subsumption in the following derivation.

\begin{matrix}Γ, X ≤ T_{1}→T_{2}, f:X, a:T_{1} ⊢ ok \\ Γ, X ≤ T_{1}→T_{2}, f:X, a:T_{1} ⊢ f : X \end{matrix} \begin{matrix}Γ, X ≤ T_{1}→T_{2}, f:X, a:T_{1} ⊢ ok \\ Γ, X ≤ T_{1}→T_{2}, f:X, a:T_{1} ⊢ X ≤ T_{1}→T_{2} \end{matrix}
\overline{T-Sub}

Γ, X ≤ T_{1}→T_{2}, f:X, a:T_{1} ⊢ f : T_{1}→T_{2}

Γ, X ≤ T_{1}→T_{2}, f:X, a:T_{1} ⊢ f : T_{1}→T_{2} \begin{matrix}Γ, X ≤ T_{1}→T_{2}, f:X, a:T_{1} ⊢ ok \\ Γ, X ≤ T_{1}→T_{2}, f:X, a:T_{1} ⊢ a : T_{1} \end{matrix}
\overline{T-App}

Γ, X ≤ T_{1}→T_{2}, f:X, a:T_{1} ⊢ f a : T_{2}

Note that, in the presence of T-Subsumption, we may actually perform the application when the type of a is a subtype of T_{1}. Namely, if

Γ, X ≤ T_{1}→T_{2}, f:X, a:U_{1} ⊢ a : U_{1} Γ, X ≤ T_{1}→T_{2}, f:X, a:U_{1} ⊢ U_{1} ≤ T_{1}

\overline{T-Sub}

Γ, X ≤ T_{1}→T_{2}, f:X, a:U_{1} ⊢ a : T_{1}

Moreover, we may want to check whether Γ, X ≤ T_{1}→T_{2}, f:X, a:U_{1} ⊢ f a : U_{2}, where T_{2} is a subtype of U_{2}.

The situation gets more complicated if f has an intersection type. Suppose that

Γ, X ≤ T_{1}→T_{2}, Y ≤ S_{1}→S_{2}, f:X ∧ Y ∧ ∀Z≤V_{1}:K.V_{2}, a:U_{1} ⊢ f a : U_{2}, where U_{1} is a subtype of T_{1} and S_{1}. An algorithm should not consider the type ∀Z≤V_{1}:K.V_{2} for f since, in this case, f is applied to a term and not to a type. Then it has to replace X and Y by their bounds, T_{1}→T_{2} and S_{1}→S_{2}. Moreover, given that the type of a, U_{1}, is a subtype of both S_{1} and T_{1}, it should check whether S_{2} ∧ T_{2} is a subtype of U_{2}.

Another source of problems in the search for an algorithmic presentation of the typing rules is that types may not be in normal form. Consider the judgement

Γ, X ≤ T_{1}→T_{2}, Z ≤ ΛY: ⋆ .Y , f:Z X, a:T_{1} ⊢ f a : T_{2}, (2)

In order to type the application, f should be assigned type T_{1}→T_{2}. To do that, Z should be replaced by its bound in Z X. This replacement produces a type which is not in normal form, so ΛY: ⋆ .Y X has to be normalized to obtain X. Finally, X is replaced by its bound and then the application can be typed.

The main new source of difficulty is the interaction between the need for normalization and the presence of intersection types.

An algorithm to infer types should proceed structurally on the form of the term whose type is to be inferred. This requires us to remove the rules which make our typing rules non-deterministic: we should eliminate T-Subsumption and T-Meet from the original presentation, and modify the other rules in such a way that we can still type the same set of terms.

We give some preliminary definitions and results before presenting the rules of our new system:

• We define the mapping flub, which performs the “replacements” which we motivated with the previous examples.

• We define the function arrows, to filter arrow types in order to deal with term application.

• We define the function alls to filter polymorphic types to deal with type application.

The function lub (definition 6.1.3) is a partial function which is only defined for type variables and type applications. Here, we extend the definition of lub to intersection types in such a way that it is defined if the least upper bound is defined for at least one of the types in the intersection.

Definition 10.1 (Homomorphic extension of lub to intersections, lub^{∗})

lub_{Γ}^{∗}(X) = Γ(X),
lub_{Γ}^{∗}(S T) = lub_{Γ}^{∗}(S) T,
lub_{Γ}^{∗}(⋀^{K}[T_{1}..T_{n}]) = ⋀^{K}[T′_{1}..T′_{n}], if ∃i ∈ {1..n} such that lub_{Γ}^{∗}(T_{i})↓,

where T′_{i} is lub_{Γ}^{∗}(T_{i}), if lub_{Γ}^{∗}(T_{i})↓, and T_{i} otherwise, and T ↓ means T is defined.

Lemma 10.2 If lub_{Γ}^{∗}(T) is defined, then Γ ⊢ T ≤ lub_{Γ}^{∗}(T).

Proof: By induction on the complexity of T, using corollary 4.14. □

We define the mapping flub which given a type T (and a context Γ) finds the smallest type larger than T (with respect to the subtype relation) having structural information to perform an application.

Definition 10.3 (Functional Least Upper Bound) The functional least upper bound of a type T, in a context Γ, flub_{Γ}(T) is defined as follows.

flub_{Γ}(T) = \{ \begin{matrix}flub_{Γ}(lub_{Γ}^{∗}(T^{nf})), & if lub_{Γ}^{∗}(T^{nf})↓; \\ T^{nf}, & otherwise.^{1} \end{matrix}

The intuition behind the definition of the function flub is to find T_{1}→T_{2} starting form ZX in the example 2 above. In other words, flub_{Γ}(Z X) = T_{1}→T_{2}. For simplicity we assume T_{1}→T_{2} in normal form. Step by step,

flub_{Γ}(Z X) = flub_{Γ}(lub_{Γ}^{∗}(Z X))
= flub_{Γ}((ΛY:K.Y) X)
= flub_{Γ}(lub_{Γ}^{∗}(((ΛY:K.Y) X)^{nf}))
= flub_{Γ}(lub_{Γ}^{∗}(X))
= flub_{Γ}(T_{1}→T_{2})
= T_{1}→T_{2}.

More generally, flub climbs the subtyping hierarchy until it finds an arrow, a quantifier, or an intersection of these two.

Lemma 10.4 Let Γ ⊢ S, T : ⋆ and S =_{β∧} T. Then flub_{Γ}(S) ≡ flub_{Γ}(T).

Definition 10.5 (arrows and alls )

1. arrows (T_{1}→T_{2})  = {T_{1}→T_{2}},

arrows (⋀^{⋆}[T_{1}..T_{n}]) = ∪_{i∈{1..n}} arrows (T_{i}),
arrows (T)  = ∅, if T ≢ T_{1}→T_{2} and T ≢ ⋀^{⋆}[T_{1}..T_{n}].

2. alls (∀X≤T_{1}:K.T_{2}) = {∀X≤T_{1}:K.T_{2}},

alls (⋀^{⋆}[T_{1}..T_{n}])  = ∪_{i∈{1..n}} alls (T_{i}),
alls (T)  = ∅, if T ≢ ∀X≤T_{1}:K.T_{2} and T ≢ ⋀^{⋆}[T_{1}..T_{n}].

1This step can be optimised in an implementation of the type checking algorithm, allowing us to avoid the normalization of T when T is either an arrow type or a quantified type.

The situation here is significantly more complex than in [34] for F_{∧}, an extension of the second order λ-calculus. There it is enough to recursively search for arrows or polymorphic types in the context, because in F_{∧} there is no reduction on types. The information to be searched for is explicit in the context, so the job done here by flub is simply an extra case in the definition of arrows and alls . Namely,

arrows (X) = arrows (Γ(X)) and
alls (X) = alls (Γ(X)).

Moreover, to prove that flub is well-founded is similar for us in complexity to proving termination of subtype checking. The similarity comes from the fact that computing flub involves replacing variables by their bounds in a given context and normalizing with respect to →_{β∧}. A proof of the well-foundation of flub can be found in [19]. In contrast, in [34] it is enough to observe that well-formed contexts cannot contain cycles of variable references.

Notation 10.6 We introduce a new notation for intersection types. The intersection of all types T such that ϕ(T) holds is written ⋀^{K}[T | ϕ(T)]. Note that this is an alternative notation to ⋀^{K}[T_{1}..T_{n}] such that ϕ(T_{i}) holds if and only if i ∈ {1..n}.

We can now define a type inference algorithm for F_{∧}^{ω}.

Definition 10.7 (A type inference algorithm, inf)

\frac{Γ_{1}, x:T , Γ_{2} ⊢ ok}{Γ_{1}, x:T , Γ_{2} ⊢_{inf} x : T}  (AT-Var)

\frac{Γ, x:T_{1} ⊢_{inf} e : T_{2}}{Γ ⊢_{inf} λx:T_{1}.e : T_{1}→T_{2}}  (AT-Abs)

\frac{Γ ⊢_{inf} f : T  Γ ⊢_{inf} a : S}{Γ ⊢_{inf} f a : ⋀^{⋆}[T_{i} | S_{i}→T_{i} ∈ arrows (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}]}  (AT-App)

\frac{Γ, X≤T_{1}:K_{1} ⊢_{inf} e : T_{2}}{Γ ⊢_{inf} λX≤T_{1}:K_{1}.e : ∀X≤T_{1}:K_{1}.T_{2}}  (AT-TAbs)

\frac{Γ ⊢_{inf} f : T}{Γ ⊢_{inf} f S : ⋀^{⋆}[T_{i}[X←S] | ∀X≤S_{i}:K.T_{i} ∈ alls (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}]} (AT-TApp)

\frac{for all i ∈ \{1..n\} Γ ⊢_{inf} e[X←S_{i}] ∈ T_{i}}{Γ ⊢_{inf} for(X∈S_{1}..S_{n})e : ⋀^{⋆}[T_{1}..T_{n}]}  (AT-For)

The algorithmic information of rule AT-App is that in order to find a type for f a in Γ, we need to infer a type S for a and a type T for f, and to take the intersection of all the T′_{i}s such that T_{i}→S_{i} ∈ arrows (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}.

11 Minimal typing

In this section we show that F_{∧}^{ω} satisfies the minimal typing property (theorem 11.11). We first prove that the algorithm inf is sound with respect to F_{∧}^{ω}: if Γ ⊢_{inf} e : T, then Γ ⊢ e : T (proposition 11.4). We then prove that every closed term is typeable using either set of typing rules (lemma 11.8). Finally, we prove that inf computes minimal types for F_{∧}^{ω} terms (proposition 11.10).

Lemma 11.1 Let Γ ⊢ T : ⋆. Then Γ ⊢ T ≤ flub_{Γ}(T).

Proof: Since flub is well-founded, we can proceed by induction on the number of unfolding steps in flub_{Γ}(T). If flub_{Γ}(T) = T^{nf}, the result follows by S-Conv. Otherwise, flub_{Γ}(T) = flub_{Γ}(lub_{Γ}^{∗}(T^{nf})). By S-Conv, Γ ⊢ T ≤ T^{nf}. By lemma 10.2, Γ ⊢ T^{nf} ≤ lub_{Γ}^{∗}(T^{nf}). By the induction hypothesis, Γ ⊢ lub_{Γ}^{∗}(T^{nf}) ≤ flub_{Γ}(lub_{Γ}^{∗}(T^{nf})). Finally, by S-Trans, the result follows. □

Lemma 11.2 Let Γ ⊢ T : ⋆. Then

1. Γ ⊢ T ≤ ⋀^{⋆}[S | S ∈ arrows (flub_{Γ}(T))].

2. Γ ⊢ T ≤ ⋀^{⋆}[S | S ∈ alls (flub_{Γ}(T))].

Proof: Item 1: Using lemma 11.1, we reduce our problem to proving that

Γ ⊢ T ≤ ⋀^{⋆}[S | S ∈ arrows (T)], which follows by induction on the structure of T. Item 2 follows similarly. □

Lemma 11.3

1. If Γ ⊢ T ≤ T_{1}→T_{2}, then Γ ⊢ ⋀^{⋆}[S | S ∈ arrows (flub_{Γ}(T))] ≤ T_{1}→T_{2}.

2. If Γ ⊢ T ≤ ∀X≤T_{1}:K.T_{2}, then Γ ⊢ ⋀^{⋆}[S | S ∈ alls (flub_{Γ}(T))] ≤ ∀X≤T_{1}:K.T_{2}.

Proof: We show only case 1 here, case 2 is similar. By induction on the derivation of Γ ⊢ T ≤ T_{1}→T_{2}. The last rule of a derivation of this subtyping statement can only be S-Conv, S-TVar, S-Trans, or S-Meet-LB. The first three cases use similar arguments, therefore we consider here only the cases for S-Conv and S-Meet-LB.

S-Conv We are given that T =_{β∧} T_{1}→T_{2}. By lemma 10.4 and the definition of flub, we have that: arrows (flub_{Γ}(T)) = arrows (flub_{Γ}(T_{1}→T_{2})) = arrows ((T_{1}→T_{2})^{nf})

We now have two cases to analyze.

1. If (T_{1}→T_{2})^{nf} = T_{1}^{nf}→T_{2}^{nf}, then the result follows by S-Meet-LB and S-Conv.

2. Otherwise, let (T_{1}→T_{2})^{nf} = ⋀^{⋆}[T_{1}^{nf}→U_{1}..T_{1}^{nf}→U_{n}], where T_{2}^{nf} = ⋀^{⋆}[U_{1}..U_{n}]. Then,

arrows (flub_{Γ}(T)) = {T_{1}^{nf}→U_{1}..T_{1}^{nf}→U_{n}}. Consequently,

⋀^{⋆}[S | S ∈ arrows (flub_{Γ}(T))] = (T_{1}→T_{2})^{nf}, and the result follows by S-Conv.

S-Meet-LB We are given that Γ ⊢ ⋀^{⋆}[S_{1}..T_{1}→T_{2}..S_{n}] ≤ T_{1}→T_{2}. By the definition of flub, flub_{Γ}(⋀^{⋆}[S_{1}..T_{1}→T_{2}..S_{n}]) = ⋀^{⋆}[....T_{1}^{nf}→A_{1}..T_{1}^{nf}→A_{m}....], where T_{2}^{nf} = ⋀^{⋆}[A_{1}..A_{m}] or T_{2}^{nf} = A_{1}. Now, arrows (flub_{Γ}(⋀^{⋆}[S_{1}..T_{1}→T_{2}..S_{n}])) ⊇ {T_{1}^{nf}→A_{1}..T_{1}^{nf}→A_{m}}. Then, if T_{2}^{nf} = ⋀^{⋆}[A_{1}..A_{m}], by lemma 4.17; and, if T_{2}^{nf} = A_{1}, by S-Meet-LB, we have that

Γ ⊢ ⋀^{⋆}[S | S ∈ arrows (flub_{Γ}(⋀^{⋆}[S_{1}..T_{1}→T_{2}..S_{n}]))] ≤ (T_{1}→T_{2})^{nf}.

Finally, the result follows by S-Conv. □

Proposition 11.4 (Soundness of inf) If Γ ⊢_{inf} e : T, then Γ ⊢ e : T.

Proof: By induction on the derivation of Γ ⊢_{inf} e : T. The interesting cases are when the last applied rule is either AT-App and AT-TApp.

AT-App Γ ⊢_{inf} f a : ⋀^{⋆}[T_{i} | S_{i}→T_{i} ∈ arrows (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}] is derived from Γ ⊢_{inf} f : T Γ ⊢_{inf} a : S. If ⋀^{⋆}[T_{i} | S_{i}→T_{i} ∈ arrows (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}] =_{β∧} ⊤^{⋆}, then the result follows immediately using T-Meet. Otherwise, by the induction hypothesis, we have that Γ ⊢ f : T. By lemma 11.2(1), S-Meet-LB, S-Trans, and T-Subsumption, Γ ⊢ f : S_{i}→T_{i}. By the induction hypothesis and T-Subsumption, Γ ⊢ a : S_{i}. By T-App, Γ ⊢ f a : T_{i}. Finally, by T-Meet,

Γ ⊢ f a : ⋀^{⋆}[T_{i} | S_{i}→T_{i} ∈ arrows (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}].

AT-TApp Γ ⊢_{inf} f S : ⋀^{⋆}[T_{i}[X←S] | ∀X≤S_{i}:K.T_{i} ∈ alls (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}] is derived from Γ ⊢_{inf} f : T. If ⋀^{⋆}[T_{i} | S_{i}→T_{i} ∈ arrows (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}] =_{β∧} ⊤^{⋆}, then the result follows immediately, using T-Meet. Otherwise, assume

alls (flub_{Γ}(T)) ≡ ⋀^{⋆}[∀X≤S_{1}:K.T_{1}..∀X≤S_{n}:K.T_{n}].

By the induction hypothesis, we have that, Γ ⊢ f : T. By lemma 11.2(2), S-Meet-LB,

S-Trans, and T-Subsumption, it follows that

Γ ⊢ f : ∀X≤S_{i}:K.T_{i}. Since Γ ⊢ S ≤ S_{i}, by T-App, Γ ⊢ f S : T_{i}[X←S]. Finally, by

T-Meet, Γ ⊢ f S : ⋀^{⋆}[T_{i}[X←S] | ∀X≤S_{i}:K.T_{i} ∈ alls (flub_{Γ}(T)) and Γ ⊢ S ≤ S_{i}]. □

Lemma 11.5 (Term application)

If Γ ⊢ ⋀^{⋆}[S_{1}→T_{1}..S_{n}→T_{n}] ≤ S→T and Γ ⊢ U ≤ S, then Γ ⊢ ⋀^{⋆}[T_{j} | Γ ⊢ U ≤ S_{j}] ≤ T.

Proof: There are two cases to be considered according to the normal form of S→T. The case when (S→T)^{nf} ≡ S^{nf}→T^{nf} is similar to but simpler than the one we consider here. Assume

(S→T)^{nf} ≡ ⋀^{⋆}[S^{nf}→A_{1}..S^{nf}→A_{m}], where T^{nf} ≡ ⋀^{⋆}[A_{1}..A_{m}].

By the equivalence of ordinary and normal subtyping (theorem 8.9),

Γ^{nf} ⊢_{n} ⋀^{⋆}[S_{1}^{nf}→B_{1}^{1}..S_{1}^{nf}→B_{1}^{k_{1}}..S_{n}^{nf}→B_{n}^{1}..S_{n}^{nf}→B_{n}^{k_{n}}] ≤ ⋀^{⋆}[S^{nf}→A_{1}..S^{nf}→A_{m}],

where T_{i}^{nf} = \{ \begin{matrix}B_{i}^{1}, & if it is not an intersection; \\ ⋀^{⋆}[B_{i}^{1}..B_{i}^{k_{i}}], & otherwise. \end{matrix} By generation for normal subtyping (proposition 7.10), for each i ∈ {1..m} there exist j ∈ {1..n} and l_{j} ∈ {i..k_{j}} such that Γ^{nf} ⊢_{n} S_{j}^{nf}→B_{j}^{l_{j}} ≤ S^{nf}→A_{i}. Again, by generation for normal subtyping (proposition 7.10), for each i ∈ {1..m} there exist j ∈ {1..n} and l_{j} ∈ {i..k_{j}} such that Γ^{nf} ⊢_{n} S^{nf} ≤ S_{j}^{nf} and Γ^{nf} ⊢_{n} B_{j}^{l_{j}} ≤ A_{i}. By NS-Trans and the equivalence of ordinary and normal subtyping (theorem 8.9), for each i ∈ {1..m} there exist j ∈ {1..n} and l_{j} ∈ {i..k_{j}} such that Γ ⊢ U ≤ S_{j} and Γ^{nf} ⊢_{n} B_{j}^{l_{j}} ≤ A_{i}. By NS-∃, for each i ∈ {1..m} there exist j ∈ {1..n} such that Γ ⊢ U ≤ S_{j} and Γ^{nf} ⊢_{n} ⋀^{⋆}[B_{j}^{1}..B_{j}^{k_{j}}] ≤ A_{i}. By the equivalence of ordinary and normal subtyping (theorem 8.9), for each i ∈ {1..m} there exist j ∈ {1..n} such that Γ ⊢ U ≤ S_{j} and Γ ⊢ T_{j} ≤ A_{i}. By lemma 4.13, S-Conv, and S-Trans, Γ ⊢ ⋀^{⋆}[T_{j} | Γ ⊢ U ≤ S_{j}] ≤ T. □

Lemma 11.6 (Substitution for subtyping)

If Γ_{1} ⊢ S_{1} ≤ T_{1} and Γ_{1}, X≤T_{1}:K_{1}, Γ_{2} ⊢ S_{2} ≤ T_{2}, then Γ_{1}, Γ_{2}[X←S_{1}] ⊢ S_{2}[X←S_{1}] ≤ T_{2}[X←S_{1}].

Proof: By straightforward induction on the derivation of Γ_{1}, X≤T_{1}:K_{1}, Γ_{2} ⊢ S_{2} ≤ T_{2}, using weakening (corollary 4.6), the type substitution lemma (lemma 4.10), and lemma 3.14. □

Lemma 11.7 (Type application)

If Γ ⊢ ⋀^{⋆}[∀X≤S_{1}:K_{1}.T_{1}..∀X≤S_{n}:K_{n}.T_{n}] ≤ ∀X≤S:K.T and Γ ⊢ U ≤ S,

then Γ ⊢ ⋀^{⋆}[T_{j}[X←U] | Γ ⊢ U ≤ S_{j}] ≤ T [X←U].

Proof: There are two cases to be considered according to the normal form of ∀X≤S:K.T. The case when (∀X≤S:K.T)^{nf} ≡ ∀X≤S^{nf}:K.T^{nf} is similar to but simpler than the one we consider here. Assume (∀X≤S:K.T)^{nf} ≡ ⋀^{⋆}[∀X≤S^{nf}:K.A_{1}..∀X≤S^{nf}:K.A_{m}]where T^{nf} ≡ ⋀^{⋆}[A_{1}..A_{m}]. By the equivalence of ordinary and normal subtyping (theorem 8.9),

Γ^{nf} ⊢_{n} ⋀^{⋆}[∀X≤S_{1}^{nf}:K_{1}.B_{1}^{1}..∀X≤S_{1}^{nf}:K_{1}.B_{1}^{k_{1}}..∀X≤S_{n}^{nf}:K_{n}.B_{n}^{1}..∀X≤S_{n}^{nf}:K_{n}.B_{n}^{k_{n}}] ≤ ⋀^{⋆}[∀X≤S^{nf}:K.A_{1}..∀X≤S^{nf}:K.A_{m}],

where T_{i}^{nf} = \{ \begin{matrix}B_{i}^{1}, & if it is not an intersection; \\ ⋀^{⋆}[B_{i}^{1}..B_{i}^{k_{i}}], & otherwise. \end{matrix}

By generation for normal subtyping (proposition 7.10), for each i ∈ {1..m} there exist j ∈ {1..n} and l_{j} ∈ {i..k_{j}} such that Γ^{nf} ⊢_{n} ∀X≤S_{j}^{nf}:K_{j}.B_{j}^{l_{j}} ≤ ∀X≤S^{nf}:K.A_{i}. Again, by generation for normal subtyping (proposition 7.10), for each i ∈ {1..m} there exist j ∈ {1..n} and l_{j} ∈ {i..k_{j}} such that K ≡ K_{j},S^{nf} ≡ S_{j}^{nf}, and Γ^{nf}, X≤S_{j}^{nf}:K ⊢_{n} B_{j}^{l_{j}} ≤ A_{i}. By NS-∀∃, for each i ∈ {1..m} there exist j ∈ {1..n} such that Γ^{nf}, X≤S_{j}^{nf}:K ⊢_{n} T_{j}^{nf} ≤ A_{i}. By the equivalence of ordinary and normal subtyping (theorem 8.9), for each i ∈ {1..m} there exist j ∈ {1..n} such that Γ, X≤S_{j}:K ⊢ T_{j} ≤ A_{i}. Furthermore, by S-Conv and S-Trans, Γ ⊢ U ≤ S_{j}. Then, by the substitution lemma for subtyping (lemma 11.6), for each i ∈ {1..m} there exist j ∈ {1..n} such that Γ ⊢ T_{j}[X←U] ≤ A_{i}[X←U]. By NS-∀∃, Γ ⊢ ⋀^{⋆}[T_{j}[X←U] | Γ ⊢ U ≤ S_{j}] ≤ ⋀^{⋆}[A_{1}[X←U]..A_{m}[X←U]]. By the definition of substitution, Γ ⊢ ⋀^{⋆}[T_{j}[X←U] | Γ ⊢ U ≤ S_{j}] ≤ T^{nf}[X←U]. Finally, by lemma 3.14, S-Conv, and S-Trans, Γ ⊢ ⋀^{⋆}[T_{j}[X←U] | Γ ⊢ U ≤ S_{j}] ≤ T [X←U], □

Usually, the next step to prove the accuracy of an algorithm, inf in our case, would be to prove a completeness result: if the term e has type T with respect to the context Γ in the the typing system F_{∧}^{ω} then the algorithm inf finds a type T′ for e in Γ. In the present situation this result is not strong enough, since every closed term is typeable in both systems. One easily proves that

Lemma 11.8

1. If e is closed in Γ, then there exists T such that Γ ⊢ e : T.

2. If e is closed in Γ, then there exists T such that Γ ⊢_{inf} e : T.

We use the fact that inf is deterministic, which means that the rules are invertible, to prove that inf finds a minimal type.

Proposition 11.9 (Generation for inf) The form of a derivable typing statement uniquely determines the last applied rule.

Proposition 11.10 (inf computes minimal types)

If Γ ⊢ e : T and Γ ⊢_{inf} e : T′, then Γ ⊢ T′ ≤ T.

Proof: By induction on the derivation of Γ ⊢ e : T. We illustrate the proof technique showing the case for T-App. We are given that e ≡ f a, Γ ⊢ f : V →T , and Γ ⊢ a : V. By generation for inf (proposition 11.9), Γ ⊢_{inf} f : U, Γ ⊢_{inf} a : S, and T′ ≡ ^{⋀⋆}[T_{i} | S_{i}→T_{i} ∈ arrows (flub_{Γ}(U)) and Γ ⊢ S ≤ S_{i}]. By the induction hypothesis, Γ ⊢ U ≤ V →T, and Γ ⊢ S ≤ V. By lemma 11.3(1), Γ ⊢ ⋀^{⋆}[S_{i}→T_{i} | S_{i}→T_{i} ∈ arrows (flub_{Γ}(U))] ≤ V →T. Finally, by the term application lemma (lemma 11.5), it follows that Γ ⊢ ⋀^{⋆}[T_{i} | Γ ⊢ S ≤ S_{i}] ≤ T, where S_{i}→T_{i} ∈ arrows (flub_{Γ}(U)). In other words, Γ ⊢ ⋀^{⋆}[T_{i} | S_{i}→T_{i} ∈ arrows (flub_{Γ}(U))] ≤ T. □

Finally, we have proved the following result.

Theorem 11.11 (Minimal typing for F_{∧}^{ω}) Given a term e and a context Γ, there exists T such that for every T′, if Γ ⊢ e : T′, then Γ ⊢ T ≤ T′.

12 Subject reduction

The F_{∧}^{ω} system is layered in three syntactic categories: kinds, types, and terms. Since terms do not appear in either types or kinds, reductions in type expressions can be studied independently from the reductions of terms. In section 2, we proved that reduction on types preserves kinding properties: the sub-language of types and kinds satisfies the subject reduction property (lemma 4.11):

if Γ ⊢ S : K and S ↠_{β∧} T, then Γ ⊢ T : K.

In this section, we show the subject reduction property for typing judgements (proposition 12.7):

if Γ ⊢ e : T and e ↠_{βfor} e′, then Γ ⊢ e′ : T.

In other words, reductions on terms are also safe.

Lemma 12.1 If Y ∉ FV(S), then

1. e[Y ←T][X←S] ≡ e[X←S][Y ←T [X←S]]

2. U[Y ←T][X←S] ≡ U[X←S][Y ←T [X←S]]

Proof: By induction on the structure of e and U respectively. □

Lemma 12.2 (Substitution for typing)

1. If Γ_{1} ⊢ e_{1} : S_{1} and Γ_{1}, x:S_{1}, Γ_{2} ⊢ e_{2} : S_{2}, then Γ_{1}, Γ_{2} ⊢ e_{2}[x←e_{1}] : S_{2}.

2. If Γ_{1} ⊢ S≤S_{1} and Γ_{1}, X≤S_{1}:K_{1}, Γ_{2} ⊢ e_{2} : S_{2}, then Γ_{1}, Γ_{2}[X←S] ⊢ e_{2}[X←S] : S_{2}[X←S].

Proof:

1. By induction on the derivation of Γ_{1}, x:S_{1}, Γ_{2} ⊢ e_{2} : S_{2}.

2. By induction on the derivation of Γ_{1}, X≤S_{1}:K_{1}, Γ_{2} ⊢ e_{2} : S_{2}, using the type substitution lemma (lemma 4.10) in the T-Var and T-Meet cases; the substitution lemma for subtyping (lemma 11.6) and lemma 12.1 in the case for T-TApp; lemma 12.1 in the T-For case, and the substitution lemma for subtyping (lemma 11.6) in the

T-Subsumption case. □

Lemma 12.3 Γ ⊢ ⊤^{⋆} ≤ T if and only if T =_{β∧} ⊤^{⋆} and Γ ⊢ T : ⋆.

Proof: If T =_{β∧} ⊤^{⋆}, then the result follows by S-Conv. Otherwise, if Γ ⊢ ⊤^{⋆} ≤ T, by the well-kindedness of subtyping (proposition 4.18), T-Meet, and uniqueness of kinds (lemma 4.9), Γ ⊢ T : ⋆. By the equivalence of ordinary and algorithmic subtyping (proposition 9.2), Γ^{nf} ⊢_{Alg} ⊤^{⋆} ≤ T^{nf}, which can only be derived using AlgS-∀∃ where T^{nf} is the empty intersection. □

Given Γ ⊢ S ≤ T, generation for normal subtyping (proposition 7.10) and the equivalence of ordinary and normal subtyping (theorem 8.9) provide subtyping information about the normal forms of S and T. We can also show that subtyping is structural for arrow types, quantified types and type operators, without reducing the terms in the subtyping relation to normal form. An implementation of a subtyping algorithm for F_{∧}^{ω} could take advantage of this fact by delaying normalizing steps, which might result in having to consider fewer recursive calls or calls with smaller arguments.

Lemma 12.4 (Generation for ordinary subtyping)

1. Γ ⊢ T_{1}→T_{2} ≤ S_{1}→S_{2} and S_{2} ≠_{β∧} ⊤^{⋆} if and only if Γ ⊢ S_{1} ≤ T_{1} and Γ ⊢ T_{2} ≤ S_{2}.

2. Γ ⊢ ∀X≤T_{1}:K_{T} .T_{2} ≤ ∀X≤S_{1}:K_{S}.S_{2} and S_{2} ≠_{β∧} ⊤^{⋆} if and only if K_{S} ≡ K_{T}, T_{1} =_{β∧} S_{1}, and Γ, X≤T_{1}:K_{T} ⊢ T_{2} ≤ S_{2}.

3. Γ ⊢ ΛX:K_{T} .T_{2} ≤ ΛX:K_{S}.S_{2} and S_{2} ≠_{β∧} ⊤^{⋆} if and only if Γ, X:K_{S} ⊢ T_{2} ≤ S_{2} and K_{T} ≡ K_{S}.

Proof: The three statements are proved using a similar argument. We consider here the proof of part 2. If K_{S} ≡ K_{T}, T_{1} =_{β∧} S_{1}, and Γ, X≤T_{1}:K_{T} ⊢ T_{2} ≤ S_{2}, then, by S-All and S-Conv, Γ ⊢ ∀X≤T_{1}:K_{T} .T_{2} ≤ ∀X≤S_{1}:K_{S}.S_{2}. Conversely, let Γ ⊢ ∀X≤T_{1}:K_{T} .T_{2} ≤ ∀X≤S_{1}:K_{S}.S_{2} and S_{2} ≠_{β∧} ⊤^{⋆}. Lemma 12.3 implies that T_{2}^{nf} ≠_{β∧} ⊤^{⋆}. Then we have to consider four cases according to whether S_{2}^{nf} and T_{2}^{nf} are intersection types or not. We illustrate the proof argument considering just one case. Let

(∀X≤T_{1}:K_{T} .T_{2})^{nf} ≡ ∀X≤T_{1}^{nf}:K_{T} .T_{2}^{nf}, and
(∀X≤S_{1}:K_{S}.S_{2})^{nf} ≡ ⋀^{⋆}[∀X≤S_{1}^{nf}:K_{S}.A_{1}..∀X≤S_{1}^{nf}:K_{S}.A_{n}],

where S_{2}^{nf} ≡ ⋀^{⋆}[A_{1}..A_{n}]. By the equivalence of ordinary and normal subtyping (theorem 8.9) and generation for normal subtyping (proposition 7.10), for each i ∈ {1..n} Γ^{nf} ⊢_{n} ∀X≤T_{1}^{nf}:K_{T} .T_{2}^{nf} ≤ ∀X≤S_{1}^{nf}:K_{S}.A_{i} and, again generation for normal subtyping (proposition 7.10) implies that Γ^{nf}, X≤T_{1}^{nf}:K_{T} ⊢_{n} T_{2}^{nf} ≤ A_{i}, and T_{1}^{nf} ≡ S_{1}^{nf}. By NS-∀, Γ^{nf}, X≤T_{1}^{nf}:K_{T} ⊢_{n} T_{2}^{nf} ≤ S_{2}^{nf} and Γ, X≤T_{1}:K_{T} ⊢ T_{2} ≤ S_{2}, by the equivalence of ordinary and normal subtyping (theorem 8.9). □

Lemma 12.5 (Generation for typing)

1. If Γ ⊢ λx:S_{1}.e : S, then there exists S_{2} such that Γ, x:S_{1} ⊢ e : S_{2} and Γ ⊢ S_{1}→S_{2} ≤ S.

2. If Γ ⊢ λX≤S_{1}:K_{1}.e : S, then there exists S_{2} such that Γ, X≤S_{1}:K_{1} ⊢ e : S_{2} and Γ ⊢ ∀X≤S_{1}:K_{1}.S_{2} ≤ S.

3. If Γ ⊢ for(X∈{U_{1}..U_{n}})e : T, then there exist T_{1}..T_{n} such that, for each i in {1..n}, Γ ⊢ e[X←U_{i}] : T_{i} and Γ ⊢ ⋀^{⋆}[T_{1}..T_{n}] ≤ T.

Proof: Each statement is proved by induction on the derivation of the typing statement in the antecedent. We exhibit here the proof of part 3. We proceed by case analysis on the last rule of the derivation of Γ ⊢ for(X∈{U_{1}..U_{n}})e : T.

T-For We are given that Γ ⊢ e[X←U] : T for some U ∈ {U_{1}..U_{n}}. Since every closed term has a type, we have that, for each i in {1..n}, Γ ⊢ e[X←U_{i}] : T_{i}, and, by S-Meet-LB,

Γ ⊢ ⋀^{⋆}[T_{1}..T ..T_{n}] ≤ T.

T-Meet Let T ≡ ⋀^{⋆}[S_{1}..S_{k}]. We are given that, Γ ⊢ ok and Γ ⊢ for(X∈{U_{1}..U_{n}})e : S_{j}, for each j in {1..k}. By the induction hypothesis, for each j ∈ {1..k} and each i ∈ {1..n} , there exist T_{j_{i}} such that Γ ⊢ e[X←U_{i}] : T_{j_{i}}, and Γ ⊢ ⋀^{⋆}[T_{j_{1}}..T_{j_{n}}] ≤ S_{j}, and, by the minimal type property (theorem 11.11), there exist T_{1}..T_{n} such that Γ ⊢ e[X←U_{i}] : T_{i}, and Γ ⊢ T_{i} ≤ T_{j_{i}}, by lemma 4.17, it follows that Γ ⊢ ⋀^{⋆}[T_{1}..T_{n}] ≤ ⋀^{⋆}[T_{j_{1}}..T_{j_{n}}], and by S-Trans, Γ ⊢ ⋀^{⋆}[T_{1}..T_{n}] ≤ S_{j}. Finally, by S-Meet-G, it follows that Γ ⊢ ⋀^{⋆}[T_{1}..T_{n}] ≤ ⋀^{⋆}[S_{1}..S_{k}].

T-Sub We are given that Γ ⊢ for(X∈{U_{1}..U_{n}})e : S, and Γ ⊢ S ≤ T. The result follows by the induction hypothesis and S-Trans. □

Since terms cannot occur in types, subject reduction for terms does not need to consider reductions in contexts.

Proposition 12.6 (One step subject reduction for typing judgements)

If Γ ⊢ e : T and e →_{βfor} e′, then Γ ⊢ e′ : T.

Proof: Since every term has type ⊤^{⋆}, the interesting case is when T ≠_{β∧} ⊤^{⋆}. This proposition follows by induction on the derivation of Γ ⊢ e : T. We consider the cases where e is a redex; the other cases follow by straightforward application of the induction hypothesis.

T-App There are two possibilities for e to be a redex.

1. e ≡ (λx:S_{1}.e_{1}) e_{2}, e′ ≡ e_{1}[x←e_{2}], and T ≡ T_{2} . We are given that Γ ⊢ λx:S_{1}.e_{1} : T_{1}→T_{2} and Γ ⊢ e_{2} : T_{1}. By the generation lemma for typing (lemma 12.5), there exists S_{2} such that, Γ, x:S_{1} ⊢ e_{1} : S_{2} and Γ ⊢ S_{1}→S_{2} ≤ T_{1}→T_{2}. Since T_{2} ≠_{β∧} ⊤^{⋆}, by the generation lemma for ordinary subtyping (lemma 12.4), Γ ⊢ T_{1} ≤ S_{1} and Γ ⊢ S_{2} ≤ T_{2}. Then, by T-Subsumption, it follows that Γ, x:S_{1} ⊢ e_{1} : T_{2} and Γ ⊢ e_{2} : S_{1}. Finally, by the substitution lemma for typing (lemma 12.2(1)), Γ ⊢ e_{1}[x←e_{2}] : T_{2}.

2. e ≡ (for(X∈U_{1}..U_{n})e_{2}) e_{1}, e′ ≡ for(X∈U_{1}..U_{n})(e_{2} e_{1}), and T ≡ T_{2}. We are given that Γ ⊢ for(X∈U_{1}..U_{n})e_{2} : T_{1}→T_{2} and Γ ⊢ e_{1} : T_{1}. By the generation lemma for typing (lemma 12.5), there exist V_{1}..V_{n} such that Γ ⊢ e_{2}[X←U_{i}] : V_{i} for each i ∈ {1..n}, and Γ ⊢ ⋀^{⋆}[V_{1}..V_{n}] ≤ T_{1}→T_{2}. We write V_{i}^{nf} ≡ A_{i_{1}}, if it is not an intersection, V_{i}^{nf} ≡ ⋀^{⋆}[A_{i_{1}}..A_{i_{k_{i}}}], otherwise.

Note that ⋀^{⋆}[V_{1}..V_{n}]^{nf} ≡ ⋀^{⋆}[A_{1_{1}}..A_{1_{k_{1}}}..A_{n_{1}}..A_{n_{kn}}]. By the equivalence of ordinary and normal subtyping (theorem 8.9), Γ^{nf} ⊢_{n} ⋀^{⋆}[A_{1_{1}}..A_{1_{k_{1}}}..A_{n_{1}}..A_{n_{kn}}] ≤ (T_{1}→T_{2})^{nf}. There are two cases to consider according to the form of (T_{1}→T_{2})^{nf}. If (T_{1}→T_{2})^{nf} is T_{1}^{nf}→T_{2}^{nf} or ⋀^{⋆}[T_{1}^{nf}→B_{1}..T_{1}^{nf}→B_{r}] where T_{2}^{nf} ≡ ⋀^{⋆}[B_{1}..B_{r}]. We show here the latter; the former is simpler. By generation for normal subtyping (proposition 7.10), for every s ∈ {1..r} there exist l ∈ {1..n} and j ∈ {1..k_{l}} such that Γ^{nf} ⊢_{n} A_{l_{j}} ≤ T_{1}^{nf}→B_{s}, and, by NS-∃ or NS-Refl, Γ^{nf} ⊢_{n} V_{l}^{nf} ≤ A_{l_{j}}, by NS-Trans, for every s ∈ {1..r} there exists l ∈ {1..n} such that Γ^{nf} ⊢_{n} V_{l}^{nf} ≤ T_{1}^{nf}→B_{s}, and, by the equivalence of ordinary and normal subtyping (theorem 8.9), Γ ⊢ V_{l} ≤ T_{1}→B_{s}. By T-Subsumption, for every s ∈ {1..r} there exists l ∈ {1..n} Γ ⊢ e_{2}[X←S_{l}] : T_{1}→B_{s}. By T-App, for every s ∈ {1..r} there exists l ∈ {1..n} Γ ⊢ (e_{2}[X←S_{l}]) e_{1} : B_{s}, and since X is not a free variable of e_{1} we have that, for every s ∈ {1..r} there exists l ∈ {1..n} Γ ⊢ e_{2} e_{1}[X←S_{l}] : B_{s}. Applying T-For, we get that for every s ∈ {1..r} Γ ⊢ for(X∈U_{1}..U_{n})e_{2} e_{1} : B_{s}, by T-Meet, Γ ⊢ for(X∈U_{1}..U_{n})e_{2} e_{1} : T_{2}^{nf}. Finally, by

S-Conv and T-Subsumption, Γ ⊢ for(X∈U_{1}..U_{n})e_{2} e_{1} : T_{2}.

T-TApp There are two possibilities for e to be a redex. We show only one case here. The case when e ≡ (for(X∈U_{1}..U_{n})e_{2}) S follows a similar argument to the one used for the case e ≡ (for(X∈U_{1}..U_{n})e_{2}) e_{1} in T-App.

If e ≡ (λX≤S_{1}:K_{S}.e_{2}) S, e′ ≡ e_{2}[X←S], and T ≡ T_{2}[X←S], we have that Γ ⊢ λX≤S_{1}:K_{S}.e_{1} : ∀X≤T_{1}:K_{T} .T_{2} and Γ ⊢ S ≤ T_{1}. By the generation lemma for typing (lemma 12.5), there exists S_{2} such that Γ, X≤S_{1}:K_{S} ⊢ e_{2} : S_{2} and Γ ⊢ ∀X≤S_{1}:K_{S}.S_{2} ≤ ∀X≤T_{1}:K_{T} .T_{2}. Since T_{2}[X←S] ≠_{β∧} ⊤^{⋆}, lemma 3.14 implies that T_{2} ≠_{β∧} ⊤^{⋆}. Then, by the generation lemma for ordinary subtyping (lemma 12.4), Γ, X≤S_{1}:K_{S} ⊢ S_{2} ≤ T_{2}, S_{1} =_{β∧} T_{1}, and K_{S} ≡ K_{T} . By T-Subsumption, Γ, X≤S_{1}:K_{S} ⊢ e_{2} : T_{2}, and, by S-Trans and S-Conv, Γ ⊢ S ≤ S_{1}. Finally, by the substitution lemma for typing (lemma 12.2(2)), Γ ⊢ e_{2}[X←S] : T_{2}[X←S].

T-For Let e ≡ for(X∈U_{1}..U_{n})e_{1}, where X ∉ FTV(e_{1}) and e′ ≡ e_{1}. We are given that Γ ⊢ e_{1}[X←U] : T, with U ∈ {U_{1}..U_{n}}. Since e_{1} ≡ e_{1}[X←U], the result holds. □

We now have all the results needed in order to prove that reduction on terms preserves typing. The following proposition, the subject reduction property for F_{∧}^{ω} terms, is a consequence of the previous one.

Proposition 12.7 (Subject reduction for typing judgements)

If Γ ⊢ e : T and e ↠_{βfor} e′, then Γ ⊢ e′ : T.

Proof: By induction on the derivation of e ↠_{βfor} e′, using proposition 12.6. □

13 Conclusions

We defined the typed lambda calculus F_{∧}^{ω}, a natural generalization of Girard’s system F^{ω} with intersection types and bounded polymorphism. A novel aspect of our presentation is the use of term rewriting techniques to present intersection types, which clearly splits the computational semantics (reduction rules) from the syntax (inference rules) of the system. We prove the Church-Rosser property of the reduction relation for types and terms in F_{∧}^{ω} and the strong normalization result for the reduction on types.

The normalized subtyping system, NF_{∧}^{ω}, is a significant technical contribution which is the key to finding a generation principle for the subtyping relation in F_{∧}^{ω} and an algorithm, AlgF_{∧}^{ω}, which is shown to be equivalent to the original presentation. A generation principle is the key result needed to prove the Subject Reduction property for F_{∧}^{ω}, which we established in section 12.

We also presented a type inference algorithm and prove that it computes Minimal Types for F_{∧}^{ω}.

The work presented here has been extracted from the Ph.D thesis of the author [22], and a short version of sections 6 to 9 has been published in CSL’94 [21]. The techniques developed here have been applied to study the combination of dependent types and subtyping in [3]. Martín Abadi and Luca Cardelli used these techniques in their book “A Theory of Objects” [1], demonstrating that our method extends naturally to a higher-order system with recursive types and object constructors.

14 Acknowledgements

I want to express my gratitude to Mariangiola Dezani-Ciancaglini for her scientific and moral support which made the present work possible. I am also grateful for discussions with Henk Barendregt, Healfdene Goguen, James McKinna, Ugo de’Liguoro, and Benjamin Pierce.

This research was supported by the Dutch organization for scientific research, NWO-SION project Typed lambda calculus, and by a European Community TMR grant.

References

[1] M. Abadi and L. Cardelli. A Theory of Objects. Springer-Verlag, 1996.

[2] R. M. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, 1993. A preliminary version appeared in POPL ’91 (pp. 104–118), and as DEC Systems Research Center Research Report number 62, August 1990.

[3] D. Aspinall and A. Compagnoni. Subtyping dependent types. In Eleventh Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA., July 27-30 1996. Preliminary version July 1995.

[4] H. Barendregt. Lambda calculi with types. In T. S. E. M. S. Abramsky, Dov M. Gabbay, editor, Handbook of Logic in Computer Science, volume 2, pages 117–309. Clarendon Press. Oxford, 1992.

[5] H. P. Barendregt. The Lambda Calculus. North Holland, revised edition, 1984.

[6] H. P. Barendregt, M. Coppo, and M. Dezani-Ciancaglini. A filter lambda model and the completeness of type assignment. Journal of Symbolic Logic, 48(4):931–940, 1983.

[7] V. Breazu-Tannen, T. Coquand, C. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93:172–221, 1991.

REFERENCES 48

[8] K. B. Bruce and J. Mitchell. PER models of subtyping, recursive types and higher-order polymorphism. In Proceedings of the Nineteenth ACM Symposium on Principles of Programming Languages, Albequerque, NM, January 1992.

[9] P. Canning, W. Cook, W. Hill, W. Olthoff, and J. Mitchell. F-bounded quantification for object-oriented programming. In Fourth International Conference on Functional Programming Languages and Computer Architecture, pages 273–280, September 1989.

[10] L. Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988. Preliminary version in Semantics of Data Types, Kahn, MacQueen, and Plotkin, eds., Springer-Verlag LNCS 173, 1984.

[11] L. Cardelli. Types for data-oriented languages. In First Conference on Extending Database Technology, volume 303 of Lecture Notes in Computer Science. Springer-Verlag, May 1988.

[12] L. Cardelli. Notes about F_{<:}^{ω}. Unpublished manuscript, October 1990.

[13] L. Cardelli. Typeful programming. In E. J. Neuhold and M. Paul, editors, Formal Description of Programming Concepts. Springer-Verlag, 1991. An earlier version appeared as DEC Systems Research Center Research Report #45, February 1989.

[14] L. Cardelli and J. Mitchell. Operations on records. Mathematical Structures in Computer Science, 1:3–48, 1991. Also in [31], and available as DEC Systems Research Center Research Report #48, August, 1989, and in the proceedings of MFPS ’89, Springer LNCS volume 442.

[15] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4), December 1985.

[16] F. Cardone and M. Coppo. Two extensions of Curry’s type inference system. In P. Odifreddi, editor, Logic and Computer Science, number 31 in APIC Studies in Data Processing, pages 19–76. Academic Press, 1990.

[17] F. Cardone, M. Dezani-Ciancaglini, and U. de’ Liguoro. Combining type disciplines, 1993. Manuscript.

[18] G. Castagna and B. Pierce. Decidable bounded quantification. In Proceedings of Twenty-First Annual ACM Symposium on Principles of Programming Languages, Portland, OR. ACM, January 1994.

[19] A. Compagnoni. Decidable higher order subtyping. Technical report, University of Edinburgh, LFCS, August 1997.

[20] A. B. Compagnoni. Subtyping in F_{∧}^{ω} is decidable. Technical Report ECS-LFCS-94-281, LFCS, University of Edinburgh, January 1994.

[21] A. B. Compagnoni. Decidability of higher-order subtyping with intersection types. In Proceedings of the Annual Conference of the European Association for Computer Science Logic, CSL’94, Kazimierz, Poland, number 933 in Lecture Notes in Computer Science. Springer-Verlag, June 1995. Preliminary version available as University of Edinburgh technical report ECS-LFCS-94-281, under the title “Subtyping in F_{∧}^{ω} is decidable”, January 1994.

[22] A. B. Compagnoni. Higher-Order Subtyping with Intersection Types. PhD thesis, University of Nijmegen, The Netherlands, January 1995. ISBN 90-9007860-6.

[23] A. B. Compagnoni and B. C. Pierce. Higher-order intersection types and multiple inheritance. Mathematical Structures in Computer Science, 6:469–501, 1996. Preliminary version available under the title Multiple Inheritance via Intersection Types as University of Edinburgh technical report ECS-LFCS-93-275 and Catholic University Nijmegen computer science technical report 93-18, Aug. 1993.

[24] W. R. Cook, W. L. Hill, and P. S. Canning. Inheritance is not subtyping. In Seventeenth Annual ACM Symposium on Principles of Programming Languages, pages 125–135, San Francisco, CA, January 1990. Also in [31].

[25] M. Coppo and M. Dezani-Ciancaglini. A new type-assignment for λ-terms. Archiv. Math. Logik, 19:139–156, 1978.

[26] M. Coppo and M. Dezani-Ciancaglini. An extension of the basic functionality theory for the λ-calculus. Notre-Dame Journal of Formal Logic, 21(4):685–693, October 1980.

[27] P.-L. Curien and G. Ghelli. Coherence of subsumption: Minimum typing and type-checking in F_{≤}. Mathematical Structures in Computer Science, 2:55–91, 1992.

[28] N. G. de Bruijn. Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indag. Math., 34(5):381– 392, 1972.

[29] G. Ghelli. Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism. PhD thesis, Università di Pisa, March 1990. Technical report TD–6/90, Dipartimento di Informatica, Università di Pisa.

[30] J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l’arithmétique d’ordre supérieur. PhD thesis, Université Paris VII, 1972.

[31] C. A. Gunter and J. C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. The MIT Press, 1994.

[32] J. McKinna and R. Pollack. Pure type systems formalized. In M. Bezem and J. F. Groote, editors, Proceedings of the International Conference on Typed Lambda Calculi and Applications, pages 289–305. Springer–Verlag, LNCS 664, Mar. 1993.

[33] J. C. Mitchell. Toward a typed foundation for method specialization and inheritance. In Proceedings of the 17th ACM Symposium on Principles of Programming Languages, pages 109–124, January 1990. Also in [31].

[34] B. C. Pierce. Programming with Intersection Types and Bounded Polymorphism. PhD thesis, Carnegie Mellon University, December 1991. Available as School of Computer Science technical report CMU-CS-91-205.

[35] B. C. Pierce and D. N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–247, Apr. 1994. A preliminary version appeared in Principles of Programming Languages, 1993, and as University of Edinburgh technical report ECS-LFCS-92-225, under the title “Object-Oriented Programming Without Recursive Types”.

[36] J. Reynolds. Using category theory to design implicit conversions and generic operators. In N. D. Jones, editor, Proceedings of the Aarhus Workshop on Semantics-Directed Compiler Generation, number 94 in Lecture Notes in Computer Science. Springer-Verlag, January 1980. Also in [31].

[37] J. C. Reynolds. Preliminary design of the programming language Forsythe. Technical Report CMU-CS-88-159, Carnegie Mellon University, June 1988.

[38] M. Steffen and B. Pierce. Higher-order subtyping. In IFIP Working Conference on Programming Concepts, Methods and Calculi (PROCOMET), June 1994. An earlier version appeared as University of Edinburgh technical report ECS-LFCS-94-280 and Universität Erlangen-Nürnberg Interner Bericht IMMD7-01/94, February 1994.