A Logic of Subtyping^{∗}

Giuseppe Longo

LIENS(CNRS) and DMI Ecole Normale Supérieure

45 rue d’Ulm 75005 Paris, France longo@dmi.ens.fr

Kathleen Milsted

France Télécom CNET 38–40 rue du Gal. Leclerc 92131 Issy-les-Moulineaux France milsted@issy.cnet.fr

Sergei Soloviev

SPIIRAN, 14th line, 39 199178, St. Petersburg Russia gor@iias.spb.su or soloviev@dmi.ens.fr

June 1996

Abstract

The relation of inclusion between types has been suggested by the practice of programming, as it enriches the polymorphism of functional languages. We propose a simple (and linear) calculus of sequents for subtyping as logical entailment. This allows us to derive a complete and coherent approach to subtyping from a few, logically meaningful, sequents. In particular, transitivity and anti-symmetry will be derived from elementary logical principles, which stresses the power of sequents and Gentzen-style proof methods. Proof techniques based on cut-elimination will be at the core of our results.

1 Introduction

1.1 Motivations, Theories and Models

In recent years, several extensions of core functional languages have been proposed to deal with the notion of subtyping; see, for example, [CW85, Mit88, BL90, BCGS91, CMMS91, CG92, PS94, Tiu96, TU96]. These extensions were suggested by the practice of programming in computer science. In particular, they were inspired by the notion of inheritance as used in object-oriented programming languages, or by other concrete implementations of the following form of polymorphism: data living in a type σ, which is a subtype of τ, may also be seen as living in type τ, in some suitable sense. So, an integer is also a real, modulo an obvious “almost identical” coercion from integers to reals.

∗A preliminary version, with no proofs and not dealing with base types, appeared in the proceedings of the LICS’95 Symposium (San Diego, U.S.A.), July 1995.

However, subtyping, in the presence of the functional arrow → (and second order universal quantification ∀) presents some problems. Indeed, in all functional approaches to subtyping, arrow is formalized as being contravariant or antimonotone in the first argument. More formally:

(→) {σ ≤ τ  ρ ≤ ρ′ \atop τ → ρ ≤ σ → ρ′}

where σ ≤ τ is read “σ is a subtype of τ”. The contravariant behavior of → (on the left) intuitively fits with the categorical notion of (contravariant) Hom functor, but also with the intuitive understanding of programs as transformations acting on inputs: if a program M acts on inputs N in τ, then it can take as input any element in a subtype σ of τ. This poses a first well-known mathematical challenge: can we give a general mathematical meaning of this formal construct and universal quantification, in the sense, say, of denotational semantics or of logical calculi?

1.1.1 Proof-Theoretic Analyses

In light of the proof-theoretic investigations that the problem of subtyping has stimulated, it is fair to say that “the notion of subtyping is one of the most important concepts introduced recently into the theory of functional languages” [Tiu96].

Let’s quote some relevant papers. [CG92] solves the difficult problems of coherence and minimum typing. Clearly, if a term belongs to a type and to any larger type, then it has no unique type nor does it code a unique proof (or type derivation). Of course, the contravariant behavior of → (on the left) and second order quantification complicate the problem. Yet, in [CG92], it is shown that each proof reduces to a unique “normal” one, which also yields the minimum type of its coding term. Other extensions of various lambda-calculi further clarified the issue of subtyping at a syntactic level. The approach in [BCGS91] significantly departs from the “intended” meaning in the previous papers: the subtyping relation is interpreted by the existence of a certain definable term between type expressions. These terms are called “coercions”.

Yet another approach may be found in [CMMS91]. This is directly related to Cardelli’s ideas for the programming language Quest and contains its main features as a basis (the Top type, bounded quantification, etc.). In short, a type-inference system is proposed which fully formalizes Quest’s rules and investigates conservativity of typing judgements and some categorical properties in a proof-theoretic frame (e.g., the syntactic isomorphisms between closed terms). Moreover, [CMMS91] suggests a rule for equality of terms, (eq appl2), a variant of which will be largely used in our approach.

Both [BCGS91] and [CMMS91] are “orthogonal” to this paper, as they contain features (a Top type, records, variants, bounded quantification, etc.) that were motivated mostly by the practice of programming and which are not present in our approach. Our perspective stresses the logical (indeed, the “implicative”) nature of subtyping and, for now, it presents only the “pure logic”. It takes care of the introduction and elimination of universal quantification, which are not present in the other approaches except in that of Mitchell [Mit88]. In a sense, the present paper may be seen as a proof-theoretic analysis of Mitchell’s axiomatic approach (see section 7.1). Further extensions, besides the addition of base types (section 8), may be a reason for further work.

The word “coercion” occurs in varying contexts. For example, in programming languages, coercions are known as “casting functions”, whereby variables of one datatype (e.g., boolean) are “converted” or “cast” to another datatype (e.g., integer). In some languages, such conversions may actually change the underlying representation (in bits) of the variable’s contents, in which case the conversion must be done at run-time when the contents are known. More semantic interpretations characterise coercions with respect to identity functions, which do not imply a change to underlying representations. The conversions implied by such coercions are performed statically at compile-time, for type-checking, etc. Coercions are used in this sense in [Mit88] for example, where they are known as “retyping functions”.

1.1.2 Models

As regards the key covariance/contravariance issue, the semantic problem should be clear. In a naive way, one may interpret “σ is a subtype of τ” as “σ is a subset of τ” or “σ can be identically injected into τ”. This set-theoretic understanding is usually expressed by the following rule, known as subsumption (Cardelli): if N has type σ and σ is a subtype of τ, then N also has type τ. However, in Set Theory, the rule (→) is not realized, as there is no way to inject τ → ρ into σ → ρ when σ is a subset of τ. There are, of course, several possible injections (by trivially extending functions) of σ → ρ into τ → ρ, but this is the opposite of what is desired. Even Category Theory, where Hom functors are contravariant on the left, doesn’t help: if “subtype” is interpreted as “subobject”, there is no way to extend a monomorphism m : σ → τ to a monomorphism from C[τ, ρ] to C[σ, ρ] or, in a Cartesian Closed Category, from ρ^{τ} to ρ^{σ}.

An early solution was proposed in [BL90] by constructing a specific categorical interpretation with “set-theoretic features”: the model of Partial Equivalence Relations (PER) accommodates Cartesian Closure as well as subtyping when σ ≤ τ is interpreted as “σ is a subrelation, a subset of pairs, of τ”. Indeed, the PER model also provides an interpretation of higher order quantification as closure under indexed products. (Except for a better understanding of this informal introduction, the reader will need no knowledge of PER models nor of Category Theory in the technical parts of this paper.) The overall categorical construction of PER, as a model of higher order lambda-calculus, in particular, Girard’s system F [Gir71], works because it is embedded in a constructive approach to Set Theory (the category of ω-Sets [LM91] or the Effective Topos [Hyl82]).

In spite of the categorical relevance of the Effective Topos (and of other categories which interpret higher order lambda-calculi) and the proof-theoretic accounts in [BCGS91, CMMS91, CG92], up to now, there has been no general categorical or purely logical understanding of subtyping (although a recent, and complex, categorical frame has been proposed in [Jac95] and the axiomatic approach in [Mit88] is also a “complete logic” for subtyping). In this paper, we propose a sequent calculus of subtyping, as a fragment of intuitionistic (linear) second order propositional calculus. In particular, we focus on the introduction and elimination rules for ∀, which are at the core of second order systems, and on a “cut-elimination” theorem. We claim that this is a crucial property for the partial order of subtyping (the “cut” rule corresponds to “transitivity”) as much as it is fundamental in logic (see also [PS94]).

The idea is that one can give an obvious logical (constructive) understanding of “σ is a subtype of τ” as “σ implies τ”, or more precisely, as “σ entails τ” (σ ⊢ τ). Note first that, with this interpretation, the usual contra(co)-variance rule for → makes perfect sense: if σ entails σ′ and τ′ entails τ, then σ′ → τ′ entails σ → τ. Moreover, if terms in σ may also be in τ, then this should be possible using some sort of effective transformation: either the identity or a “suitable” coercion, as an effective map from σ to τ. Thus, by the Curry-Howard isomorphism, subtyping is a special case of intuitionistic implication: a computation from σ to τ is a proof of σ ⊢ τ. But which special case? And how to characterize it? Coercions shouldn’t be arbitrary maps. Of course, the simplest idea would be to assume that they are identities. This makes no sense though in typed frameworks: if σ ≤ τ but σ and τ are different, there is no identity from σ to τ. This is so both in models and in theories. A way out is suggested by the PER model. PER models are constructed over an underlying model of the type-free lambda calculus. Indeed, any model of partial combinatory logic may suffice, see [Hyl88] say, and in particular Kleene’s (ω, .): in this case, n.m stays for the n-th index or Turing Machine applied to m.

Thus, in the PER model, terms are interpreted as equivalence classes of elements of ω. More precisely, define the erasure of a typed term to be the type-free term obtained by erasing all type information. Then, a term is interpreted by the equivalence class of (the interpretation of) its erasure. This allows second order quantification to be interpreted as intersection, since the intersection is isomorphic to a categorical product (see [LM91]). In short, in the model in [BL90] (more precisely in the variant of it in [CL91], sect.4), a coercion c from σ to τ transforms each {n}_{σ} into {n}_{τ}, where {n}_{σ} denotes the equivalence class of n in σ and {n}_{σ} is generally smaller than {n}_{τ}. Thus, c is computed, in particular, by any index i of the identity function; equivalently, c is represented by {i}_{σ→τ}, since {i}_{σ→τ} .{n}_{σ} = {i.n}_{τ} = {n}_{τ}. Clearly, {i}_{σ→τ} contains many more elements than the indices of the identity function on ω, when σ or τ are different from ω. Using erasures in order to interpret typed terms, then this suggests that syntactic coercions are typed terms, different, in general, from the identity, but whose erasure is equal to the identity λx.x. This idea is nicely used in [Mit88]. It will give a syntactic completeness theorem for our “logic of subtyping” described next.

1.2 Subtyping as restricted Linear Implication

The logical frame we use here is intuitionistic second-order propositional logic. The intended meaning of σ ⊢ τ is that σ is contained in τ. An obvious axiom and the contra(co)-variance rule for → are the first requests for a logic of subtyping:

(ax) σ ⊢ σ  (→) {σ′ ⊢ σ  τ ⊢ τ′ \atop σ → τ ⊢ σ′ → τ′}

Consider now a logical interpretation of second order ∀. Assume that σ contains X free and that from a specific instance of σ (with ρ substituted for X say), one can deduce τ. Then, from ∀X.σ one can, a fortiori, deduce τ. This is the (∀ left) rule of Gentzen’s sequent calculus. A semantic understanding of this second order deduction, can be given in the PER model of subtyping: if a specific instance of a family of types is a subtype of τ, then, in the model, the intersection of the entire family is a subtype of τ.

(∀ left) {[ρ/X]σ ⊢ τ \atop ∀X.σ ⊢ τ}

Moreover, if σ entails τ, and σ does not contain X free, then σ also entails ∀X.τ. This is Gentzen’s (∀ right) rule. Semantically, if σ is a subtype of τ and σ does not depend on X, then σ is also a subtype of the intersection of all τs over X:

(∀ right) {σ ⊢ τ \atop σ ⊢ ∀X.τ}
∗ for X not ; free in σ

Recall now that the principal idea here is that the embedding of a type into another should be very simple: indeed, as close to the identity as possible in a typed language. Identities are linear maps, to say the least, as our system will be a fragment of the Linear Sequent Calculus. Even more so: we allow only one premise in a sequent σ ⊢ τ, as even the swapping of inputs is forbidden. Thus, in order to deal with nested implications, we generalize (∀ right) to:

(∀_{n≥0} right) {σ ⊢ τ_{1} → … (τ_{n} → τ) …) \atop σ ⊢ τ_{1} → … (τ_{n} → ∀X.τ) …)}
∗ for X not ; free in σ nor ; in τ_{1}, …, τ_{n}

(∀_{n} right) is a family of rules indexed by n ≥ 0. Note that, if more than one premise was allowed, (∀_{n} right) would be the curried variant of (∀ right) with n premises.

These four rules are all we need. The reader may wonder what happened to a fundamental property of subtyping, that is, to transitivity. Indeed, we will prove that ⊢ is a partial order, thus, in particular that it is transitive and anti-symmetric. But transitivity is just a (cut) rule:

(cut) {σ ⊢ τ  τ ⊢ ρ \atop σ ⊢ ρ}

Proving transitivity will thus be the proof of admissibility for the rule (cut), that is, that each time the premises are derivable, then the consequence is derivable too. Or, equivalently, that the system extended with (cut) has the cut-elimination property. Notice now that the proof one can “eliminate cuts” is non trivial for weak systems (as we will discuss at length below), as, in general, these results and proofs are not inherited to subsystems.

Remark that ∀ is introduced to the left and to the right of entailment by two separate rules while → is symmetrically introduced both to the left and to the right of entailment by a single rule, the familiar (→) rule defined previously. This will turn out to be important in our proof of cut-elimination.

Cut-elimination is a fundamental property in constructive logical systems. It guarantees consistency as it shows that each derivation can be given a “minimal” structure. In the various lambda-calculi, it relates deductions to computations as cut-elimination corresponds to a β-reductions. In those systems, (cut) is a non-primitive rule, as it corresponds to the sequential application of (→-introduction) and (→-elimination) rules; moreover, it is usually considered as a (side) consequence of normalization. In contrast to this, for the purposes of subtyping, (cut) is as basic as transitivity: our non-obvious result is that transitivity can be derived or, from a logical perspective, that our system, in the presence of the rules for universal quantification and extended with (cut), has the cut-elimination property.

The seemingly simple logical system above will be shown to be complete and coherent as a logic for deriving subtyping relations. By completeness, we mean that σ ⊢ τ is derivable iff there is a term of type σ → τ that erases to the identity. We define a coercion to be such a term. By a result in [Mit88] this will also guarantee completeness with respect to subtyping in all PER models, in the sense of [BL90]. Transitivity will be essential to this result.

Coherence will mean that derivability of σ ⊢ τ implies a unique coercion from σ to τ. One of its consequences will be anti-symmetry. Coherence will be easily shown in our system, while it requires cut-elimination if proved in the system extended with (cut).

Once the formal system is fully written down, with proof-terms displayed (see Section 3), the next thing to be described is term equality. The notion of equality we use here may be viewed the “generalized dual” of an early result of Girard’s [Gir71]: in system F, there is no definable term that discriminates between types. Namely, there is no definable term J_{σ} such that J_{σ} applied to type ρ is 1 if σ = ρ, and is 0 if σ ≠ ρ. This idea was taken up in [LMS93] by extending system F with the following axiom:

(Axiom C) {M : ∀X.σ \atop Mτ_{1} = Mτ_{2}}
∗for X not ; free in σ

Intuitively, as there are no type discriminators, (Axiom C) forces terms of universally quantified type, whose outputs live in the same type, to be constant. System F extended with (Axiom C) satisfies the Genericity Theorem (see [LMS93]), which states that if two second-order functions (of the same type) coincide on an input type, then they are, in fact, the same function. Equivalently, types are generic inputs to second-order functions.

(Axiom C) was proposed following [Gir71] and independently of [CMMS91], where the system F_{≤} is defined which includes the following inference rule. This rule is more general than (Axiom C) by a crucial use of subsumption:

(eq appl2) {M : ∀X.σ  [τ_{1}/X]σ ≤ μ  [τ_{2}/X]σ ≤ μ \atop Mτ_{1} = Mτ_{2} : μ}

Observe that M gives outputs in (possibly) different types [τ_{1}/X]σ and [τ_{2}/X]σ. Then, intuitively, (eq appl2) says that if these two types (of outputs) have a common supertype μ, then the outputs are equal when seen as elements of μ. Thus, in particular, if σ does not contain X free, one obtains (Axiom C).

Note that (Axiom C) is valid in all proper models of system F, in particular in all “parametric models” in the sense of Reynolds ([MR92, ACC93]). Moreover, (eq appl2) holds in the only semantic models of system F with subtyping, namely in PER models, of course with the intended coercions. The relevance of (eq appl2) is that it allows one to prove the (categorical) universality of key definable constructs in System F (binary products, coproducts, existentials, etc.).

However, (eq appl2) relies implicitly on the subsumption rule, i.e., if M : σ and σ ≤ τ, then M : τ. And, as already pointed out, subsumption has neither type-theoretic nor categorical meaning, even though it may have solid practical motivations and intuitive meaning. Subsumption may be avoided in (eq appl2) if coercions are used explicitly as follows:

{M : ∀X.σ  y_{1} : [τ_{1}/X]σ ⊢ N_{1} : μ  y_{2} : [τ_{2}/X]σ ⊢ N_{2} : μ \atop [Mτ_{1}/y_{1}]N_{1} = [Mτ_{2}/y_{2}]N_{2}}

This “coercion version” of (eq appl2) will be used in our type-theory as an interplay between subtyping and equality.

In conclusion then, our logic of subtyping will be based on the simple four-rule sequent calculus presented previously, and the proof terms will satisfy the usual equational rules plus a coercion version of (eq appl2).

2 System F

We first recall System F [Gir71]. The language has two kinds of expression, types and terms, defined by the following syntax:

(Types)  σ ::= X | σ → τ | ∀X.σ
(Terms) M ::= x | λx:σ.M | MN | λX.M | Mτ

We will use:

σ, τ, ρ, μ for types  M, N, P, Q, R for terms
X, Y, Z for type variables  x, y, z for term variables

An environment Γ is a set of term variables with their types. We write Γ, x:σ to extend Γ with a new term variable x of type σ, where x must not already occur in Γ.

We use the notation Γ ⊢_{F} M : σ for type assignment in system F. This is read “term M is assigned type σ relative to environment Γ”. The following rules define valid type assignments.

System F

(ax) Γ, x:σ ⊢_{F} x : σ

(→ intro)  {Γ, x:σ ⊢_{F} M : τ \atop Γ ⊢_{F} λx:σ.M : σ → τ}  (→ elim) {Γ ⊢_{F} M : σ → τ  Γ ⊢_{F} N : σ \atop Γ ⊢_{F} MN : τ}

(∀ intro) {Γ ⊢_{F} M : σ \atop Γ ⊢_{F} λX.M : ∀X.σ}

∗

for X not free in the type of any free term variable in M

(∀ elim)

{Γ ⊢_{F} M : ∀X.σ \atop Γ ⊢_{F} Mτ : [τ/X]σ}

Reduction of terms is defined as usual by the closure of the following rules:

\begin{matrix}(β_{1}) & (λx:σ.M)N ⟶_{β1} [N/x]M & (β_{2}) & (λX.M)τ ⟶_{β2} [τ/X]M \\ (η_{1}) & \begin{matrix}λx:σ.Mx ⟶_{η1} M \\ ∗ & for x ∉ F V (M) \end{matrix} & (η_{2}) & \begin{matrix}λX.MX ⟶_{η2} M \\ ∗ & for X ∉ F V (M) \end{matrix} \end{matrix}

Where F V (M) is the collection of free type and term variables in M. We will write ⟶_{βη} for the transitive closure of all four reductions, ⟶_{β} for the closure of just β_{1} and β_{2}; and ⟶_{η} for the closure of η_{1} and η_{2}. We also write “nf” prefixed by a reduction relation to indicate normal form with respect to the relation.

Equality of terms is defined by the compatible, reflexive, transitive closure of ⟶_{βη}. We write M =_{βη} N for this equality, known as βη-convertibility. We reserve the notation M ≡ N for syntactic identity of terms up to renaming of bound variables, i.e., α-equivalence. For types, equality, σ = τ, is just syntactic identity up to renaming of bound variables.

3 Systems Co^{⊢} and Co^{⊢}+(cut)

3.1 System Co^{⊢}

Let us define a sequent calculus of subtyping, referred to as System Co^{⊢} (pronounced “co”, for coercions). We will use ⊢_{co} for entailment in this system.

We give two (equivalent) presentations of Co^{⊢}. The first presentation gives only the types involved in each judgment, which are of the form σ ⊢_{co} τ. This presentation emphasizes the (intended) subtyping relation between types but, of course, the calculus may be considered independently of this interpretation by referring just to its logical significance.

System Co^{⊢} (unlabelled)

(ax)  σ ⊢_{co} σ  (→)  {σ′ ⊢_{co} σ  τ ⊢_{co} τ′ \atop σ → τ ⊢_{co} σ′ → τ′}

(∀ left) {[ρ/X]σ ⊢_{co} τ \atop ∀X.σ ⊢_{co} τ}  (∀_{0≤n} right) {σ ⊢_{co} τ_{1} → … (τ_{n} → τ) …) \atop σ ⊢_{co} τ_{1} → … (τ_{n} → ∀X.τ) …)}
∗ for X not ; free in σ nor ; in τ_{1}, …, τ_{n}

In the second presentation of the system, we label each type with a term, yielding judgments of the form x: σ ⊢_{co} M : τ. This presentation makes explicit the coercion terms involved in each subtyping judgment. We will refer to the first presentation as the “unlabelled” system, to the second as the “labelled” system.

System Co^{⊢} (labelled)

(ax)  x:σ ⊢_{co} x : σ

(→)  {x′:σ′ ⊢_{co} M : σ  y:τ ⊢_{co} N : τ′ \atop x:σ → τ ⊢_{co} λx′:σ′ . [xM/y]N : σ′ → τ′}

(∀ left)  {y:[ρ/X]σ ⊢_{co} M : τ \atop x:∀X.σ ⊢_{co} [xρ/y]M : τ}

(∀_{0≤k≤n} right)  {x:σ ⊢_{co} λx_{1} :τ_{1} … λx_{k}:τ_{k}.M : τ_{1} → … (τ_{n} → τ) …) \atop x:σ ⊢_{co} \begin{matrix}λx_{1} :τ_{1} … λx_{k}:τ_{k} … λx_{n}:τ_{n}.λX.Mx_{k+1} … x_{n} \\ : τ_{1} → … (τ_{n} → ∀X.τ) …) \end{matrix}}

∗

for X not free in σ

nor in τ_{1}, …, τ_{n}, for M not of the form λy.M′, for x_{k+1}, …, x_{n} fresh

(∀_{0≤n<k} right)  {x:σ ⊢_{co} λx_{1} :τ_{1} … λx_{k}:τ_{k}.M : τ_{1} → … (τ_{n} → τ) …) \atop x:σ ⊢_{co} \begin{matrix}λx_{1} :τ_{1} … λx_{n}:τ_{n}.λX.λx_{n+1} :τ_{n+1} … λx_{k}:τ_{k}.M \\ : τ_{1} → … (τ_{n} → ∀X.τ) …) \end{matrix}}

∗

for X not free in σ

nor in τ_{1}, …, τ_{n}, for M not of the form λy.M′ for τ ≡ τ_{n+1} → … (τ_{k} → τ′) …)

We shall shortly see that the two cases of (∀_{n} right) labeled with coercion terms are disjoint.^{1} In the rest of the paper, we shall refer to judgments of either presentation (with/without coercion terms) of Co^{⊢} as “sequents”. We will use S for sequents and α, γ for derivations of sequents.

Many of the proofs in this paper are by induction on the size of a derivation. This notion of size is defined as the total number of applications of rules in a derivation.

In this work, a coercion is defined as follows:

Definition (Coercion) A sequent x: σ ⊢_{co} M : τ is a coercion from σ to τ iff it is derivable.

Example. In Co^{⊢}, ⊥ = ∀X.X (the empty type) is provably a subtype of all types. The corresponding coercion is obtained from the following derivation:

y:[σ/X]X ⊢_{co} y : σ
(∀ left)
x:∀X.X ⊢_{co} x σ : σ

1Tiuryn in [Tiu96] presents (∀_{n} right) in another slightly simpler form.

Lemma 1 (Structure of coercions) If x : σ ⊢_{co} M : τ, then the set of free term variables of M is exactly {x}, and x occurs exactly once and always at the leftmost position in M. Furthermore, each bound term variable occurs exactly once in M. Proof: By induction on the size of the derivation of x:σ ⊢_{co} M : τ.

This lemma shows that, in particular, coercions are linear terms (in the usual sense).

Lemma 2 (Coercions are functions) If x:σ ⊢_{co} M : τ then x:σ ⊢_{F} M : τ. Proof: By induction on the size of the derivation of x:σ ⊢_{co} M : τ.

Lemma 3 (Coercions are in β-nf) If x:σ ⊢_{co} M : τ then M is in β-nf. Proof: By induction on the size of the derivation of x:σ ⊢_{co} M : τ, as no inference rule creates a β-redex.

This shows that the coercion terms involved in (∀_{n} right) are unambiguously defined since M, in the assumption, must be in β-nf. Note too that, though (→) and (∀ left) may introduce η-redexes, the system is easily shown to be closed under η-reduction. It is also closed under those η-expansions that do not introduce β-redexes.

Lemma 4 For M in β-nf, assume x : σ ⊢_{F} M : τ and M ⟶_{η} M′. Then x:σ ⊢_{co} M : τ iff x:σ ⊢_{co} M′ : τ.

Clearly, ⊢_{co} is strictly weaker than ⊢_{F} . Consider, for example:

x:∀X.X ⊢_{F} x(∀X.X → ∀X.X)x : ∀X.X

but

x:∀X.X ⊬_{co} x(∀X.X → ∀X.X)x : ∀X.X

Even restricting terms to linear ones, and environments to those containing exactly one variable, is not enough to produce a coercion. For example,

x:σ → (τ → ρ) ⊢_{F} λy:τ.λz:σ.(x z y) : τ → (σ → ρ)

is not a coercion. Theorem 16 (completeness) will characterize those System F functions that are coercions.

By the Curry-Howard isomorphism, Co^{⊢} is thus a proper subsystem of Intuitionistic (Linear) Second-order Propositional Logic. This is only natural since coercions are intended to represent “inclusions” of types. Clearly, there is no reason why arbitrary F-entailment (or even isomorphisms of types) should be interpreted as inclusion.

3.2 System Co^{⊢}+(cut)

We are going to show below that ⊢_{co} is a transitive relation. That is, in the unlabelled system, the rule:

(cut) {σ ⊢_{co} τ  τ ⊢_{co} ρ \atop σ ⊢_{co} ρ}

is admissible.

Its labelled version needs some discussion. A “naive” variant would be:

{x:σ ⊢_{co} M : τ y:τ ⊢_{co} N : ρ \atop x:σ ⊢_{co} [M/y]N : ρ}

Note though that [M/y]N does not need to be a coercion; in particular, it does not need to be in β-nf. However, without making use of Strong Normalization for System F, we can prove that:

Lemma 5 (Cut-rule coercions) Consider the coercions x: σ ⊢_{co} M : τ and y: τ ⊢_{co} N : ρ. Let n be the number of λs in [M/y]N. Then each β-reduction path from [M/y]N has at most n steps and reduces to a unique term P in β-nf. Proof: By the linearity of coercions, the term [M/y]N is linear and each β-reduction decreases the number of λs.

This lemma motivates the following alternative version of labelled (cut)-rule, where nf([M/y]N) means β-nf of [M/y]N:

(cut)  {x:σ ⊢_{co} M : τ  y:τ ⊢_{co} N : ρ \atop x:σ ⊢_{co} nf([M/y]N) : ρ}

Our aim is to show that x : σ ⊢_{co} nf([M/y]N) : ρ is actually a coercion, that is, a derivable term in Co^{⊢}, or in other words, the rule above is admissible.

In section 6, the proof of admissibility of (cut) can be obtained from a cut-elimination theorem for Co^{⊢} extended with (cut). We will thus work with derivations in the extended system Co^{⊢}+(cut), where we use ⊢_{co+cut} for entailment. Clearly, a “cut-free” derivation in Co^{⊢}+(cut) is just a derivation in Co^{⊢}. Note, that by this approach to the cut-rule, the Subject Reduction Theorem trivially holds in Co^{⊢}+(cut).

3.3 Equality in Co^{⊢} and Co^{⊢}+(cut)

Equality of coercions is defined, essentially, by η-equality plus a coercion version of the F_{≤} rule (eq appl2) given in [CMMS91]. We write x: σ ⊢_{co} M =_{ηco} N : τ to mean that M and N are equal coercions from σ to τ. This relation is defined as follows.

Definition (Equality of terms) =_{ηco} is the least equivalence relation generated by α-convertibility plus

(eq η)  {x:σ ⊢_{co} M : τ  x:σ ⊢_{co} M′ : τ  M =_{η} M′ \atop x:σ ⊢_{co} M =_{ηco} M′ : τ}

(eq appl2 co)  {y_{1} : [τ_{1}/X]σ ⊢_{co} N_{1} : μ  y_{2} : [τ_{2}/X]σ ⊢_{co} N_{2} : μ \atop x:∀X.σ ⊢_{co} [xτ_{1}/y_{1}]N_{1} =_{ηco} [xτ_{2}/y_{2}]N_{2} : μ}

plus two rules, (eq →) and (eq ∀_{n} right), which state, respectively, that (→) and (∀_{n} right) preserve equality of coercions. These other rules are given in full in the appendix.

Remark that (eq appl2 co) implies (∀ left) preserves equality of coercions: given y: [ρ/X]σ ⊢_{co} M =_{ηco} N : τ, apply (eq appl2 co) with τ_{1} ≡ τ_{2} ≡ ρ and N_{1} ≡ M and N_{2} ≡ N to obtain x:∀X.σ ⊢_{co} [xρ/y]M =_{ηco} [xρ/y]N : τ.

The rules (eq →) and (eq ∀_{n} right) are derivable in system F using β-convertibility. Rule (eq appl2 co), on the other hand, is not derivable in system F as it equates terms that are not β-convertible, as shown by the following instance of the rule.

y_{1} : [τ_{1}/X]Y ⊢_{co} y_{1} : Y y_{2} : [τ_{2}/X]Y ⊢_{co} y_{2} : Y

(eq appl2 co)

x:∀X.Y ⊢_{co} [xτ_{1}/y_{1}]y_{1} =_{ηco} [xτ_{2}/y_{2}]y_{2} : Y

Thus, xτ_{1} =_{ηco} xτ_{2} whereas xτ_{1} ≠_{βη} xτ_{2} in general, i.e., they are not equal in system F. Clearly, though, xτ_{1} and xτ_{2} are equal in system F_{≤} using the corresponding “noncoercion” rule (eq appl2).

Here are two examples to illustrate =_{ηco} (reminder: ⊥ = ∀X.X). Note that these equalities are not provable in system F.

Example 1: x:⊥ ⊢_{co} x =_{ηco} x⊥ : ⊥

y_{1} :[X/X]X ⊢_{co} y_{1} : X  y:[X/X]X ⊢_{co} y : X ; (∀ left) ; y_{2} :[⊥/X]X ⊢_{co} y_{2}X : X

(eq appl2 co)

x:⊥ ⊢_{co} xX =_{ηco} x⊥X : X

(eq ∀_{0} right)
x:⊥ ⊢_{co} λX.xX =_{ηco} λX.x⊥X : ⊥
(eq η)
x:⊥ ⊢_{co} x =_{ηco} x⊥ : ⊥

Example 2: x:∀X . X → X ⊢_{co} λy:⊥ . λX . xX(yX) =_{ηco} x⊥ : ⊥ → ⊥

\begin{aligned}y′:X ⊢_{co} y′ : X ; (∀ left) ; y:⊥ ⊢_{co} yX : X & x′:X ⊢_{co} x′ : X \\ & (→) \\ y_{1} :X → X ⊢_{co} λy:⊥ . y_{1}(yX) : ⊥ → X \end{aligned} \begin{matrix}y:⊥ ⊢_{co} y : ⊥ & y′:X ⊢_{co} y′ : X ; (∀ left) ; x′:⊥ ⊢_{co} x′X : X \\ (→) \\ y_{2} :⊥ → ⊥ ⊢_{co} λy:⊥ . y_{2}yX : ⊥ → X \end{matrix}

(eq appl2 co)

x:∀X.X → X ⊢_{co} λy:⊥ . xX(yX) =_{ηco} λy:⊥ . x⊥yX : ⊥ → X

(eq ∀_{1} right)

x:∀X.X → X ⊢_{co} λy:⊥ . λX . xX(yX) =_{ηco} λy:⊥ . λX . x⊥yX : ⊥ → ⊥ Besides equality of terms, we shall need equality of derivations. To clarify the relationship between different systems, we introduce here several equality relations.

Definition (Equality of derivations) Let α_{1} be a derivation of x:σ ⊢_{co} M : τ and α_{2} a derivation of x:σ ⊢_{co} N : τ. We write:

• α_{1} = α_{2} iff M ≡ N

• α_{1} =_{η} α_{2} iff x:σ ⊢_{co} M =_{η} N

• α_{1} =_{ηco} α_{2} iff x:σ ⊢_{co} M =_{ηco} N.

In the unlabelled system, equality relations are defined via equality relations between corresponding derivations of the labelled system.

Equality of derivations in System Co^{⊢}+(cut) are defined likewise. In our cut-elimination proof, we shall show that, for each derivation α of x: σ ⊢_{co+cut} M : τ, there exists a derivation α′ in Co^{⊢} with the same M so only = will actually be needed there.

3.4 Semantics of =_{ηco}

Clearly, the semantics of rules (eq →) and (eq ∀_{n} right) pose no problems. However, the semantics, indeed the consistency, of (eq appl2 co) deserves closer attention. The following remarks are intended for the reader familiar with PER models.

Rule (eq appl2 co) is valid in the PER model of subtyping [BL90]. More precisely, it is valid in the interpretation of subtyping with explicit coercions, given in [CL91] for the system Quest_{C}. This can be seen as follows. Recall that, under an environment ξ, the interpretation of M : ρ is given by the equivalence class {[[erase(M)_{ξ}]]}_{ρ}, where, by an abuse of language, we use the same name for both a type σ and its meaning as a p.e.r.. (See the introduction and [CL91] on how type-free and typed environments are related; in short, a type-free environment ξ “picks out” an element of the equivalence class of the typed ξ′). Assume now that y_{i} : [τ_{i}/X]σ for i = 1, 2, and x : ∀X.σ. If both [τ_{i}/X]σ for i = 1, 2 are subtypes of μ, then the equivalence classes {ξ(y_{i})}_{[τ_{i}/X]σ} are coerced to the (larger) equivalence classes {ξ(y_{i})}_{μ} for i = 1, 2. Note now that, for x : ∀X.σ, one has xτ_{i} : [τ_{i}/X]σ and erase(xτ_{i}) = erase(x) = x. Then, by the interpretation of polymorphic application (see [LM91]), {ξ(x)}_{∀X.σ} . τ_{i} = {ξ(x)}_{[τ_{i}/X]σ}, which is also equal to the interpretation of xτ_{i} : [τ_{i}/X]σ.

The validity of the premises of (eq appl2 co) means that, in the model, N_{i} coerces the meaning of any term in [τ_{i}/X]σ into an equivalence class of μ. In particular, both interpretations {ξ(x)}_{[τ_{i}/X]σ} of xτ_{i} : [τ_{i}/X]σ, i = 1, 2, are coerced by N_{i} to the same equivalence class {ξ(x)}_{μ}, which does not depend on i. This is exactly the validity of the consequence of (eq appl2 co).

As recalled in the introduction, the coercions N_{1}, N_{2} are interpreted by functions computed (also) by indexes of the identity function. In general, though, they are not themselves identities and {ξ(y_{i})}_{[τ_{i}/X]σ} may be strictly smaller than {ξ(y_{i})}_{μ} (and each of the {ξ(x)}_{[τ_{i}/X]σ} may be strictly smaller than {ξ(x)}_{μ}). In [CMMS91], it is said that (eq appl2), which contains no coercions, is valid in PER models. This is correct but only modulo “forgetting” the coercions in the model (as was suggested in [BL90]). However, this does not correspond exactly to the structure of PER models, where coercions are non-identical maps (see [CL91] for a more detailed discussion). Thus, (eq appl2 co) is a more precise formalisation of “truth”, as given in PER models, than (eq appl2).

4 Some special classes of derivations

4.1 Pure variable derivations

Definition (Pure variable derivation) A pure variable derivation is a derivation such that no type variable occurs both free and bound in the same sequent (in the unlabelled and labelled systems Co^{⊢} and Co^{⊢}+(cut)).

This notion of pure variable derivations is comparable with that of Kleene’s (see [Kle67]).

Lemma 6 Every derivation in Co^{⊢} or in Co^{⊢}+(cut) is = to any derivation obtained by safely renaming bound type variables in types and terms, without capturing free type variables. Proof: By induction on the size of the derivation. In the case of (∀ left), use the identity [ρ/X]σ = [ρ/X′]([X′/X]σ) where X′ does not occur free in σ (otherwise X′ would be captured), and in the case of (∀_{n} right), uniformly substitute [X′/X] in the derivation of the premise and then use (∀_{n} right) with X′ instead of X (the side-condition is used). For (→) and (cut), it is enough to use the induction hypothesis.

Lemma 7 Every derivation in Co^{⊢} or in Co^{⊢}+(cut) is = to a pure variable derivation. Proof: By induction, using the previous lemma (always choosing fresh bound variables).

To illustrate the utility of pure variable derivations, consider the following derivation:

{α_{l} \atop x′:σ′ ⊢_{co} M : σ}  {α_{r} \atop y:τ ⊢_{co} N : τ′} ; (∀_{0} right) ; y:τ ⊢_{co} λX.N : ∀X.τ′
(→)
x:σ → τ ⊢_{co} λx′:σ′ . λX . [xM/y]N : σ′ → ∀X.τ′

By the side-condition on (∀_{0} right), we know that X is not free in τ. Our aim now is to permute the applications of (∀_{0} right) and (→) as follows:

{α_{l} \atop x′:σ′ ⊢_{co} M : σ}  {α_{r} \atop y:τ ⊢_{co} N : τ′}
(→)
x:σ → τ ⊢_{co} λx′:σ′ . [xM/y]N : σ′ → τ′
(∀_{1} right)
x:σ → τ ⊢_{co} λx′:σ′ . λX . [xM/y]N : σ′ → ∀X.τ′

However, this second derivation is only possible if the variable X is not free in σ nor in σ′, as required by (∀_{1} right). This is the case if the first derivation is a pure variable one, for then the X bound in ∀X.τ′ would be fresh.

From now on, we will work exclusively with pure variable derivations, referring to them as just “derivations”.

4.2 Permutations of rules

The following lemma gives the rule pairs that can be permuted in a derivation of Co^{⊢}, resulting in an equal derivation.

Lemma 8 (Rule permutations I) The following pairs of derivations are equal in Co^{⊢}, up to =:

1.  \begin{aligned}α \\ & (∀_{n} right) \\ S_{1} \end{aligned} (∀ left) S_{2}  =  \begin{aligned}α \\ & (∀ left) \\ S′_{1} \end{aligned} ; (∀_{n} right) ; S_{2}

2.  \begin{aligned}α_{l} & & \begin{aligned}α_{r} \\ & (∀_{n} right) \\ S_{1} \end{aligned} \\ & & (→) \\ & S_{2} \end{aligned}  =  \begin{aligned}α_{l} & & α_{r} \\ & & & (→) \\ & S′_{1} \end{aligned} ; (∀_{n+1} right) ; S_{2}

Proof: By simple consideration of the types and terms involved in each sequent. Case 1 applies to any kind of derivation whereas case 2 requires a pure variable derivation. Indeed, the proof of case 2, permuting (∀_{n} right) for n = 0 and (→), is given by the examples of pure variable derivations above. Remember that, by the definition of = on derivations, the terms labelling the end sequents of both the left and right derivations above, are identical.

Note that (∀_{n} right) becomes (∀_{n+1} right) when it is permuted downwards with (→). Note also that case 1 applies only when (∀_{n} right) is permuted downwards with (∀ left), not conversely.

In the next lemma we describe permutability of rules with (cut) (in Co^{⊢}+(cut)).

Lemma 9 (Rule permutations II) The following pairs of derivations are equal, up to =:

1. (∀_{n} right) on the right permutes with (cut):

{α_{l} \atop S_{1}}  {α_{r} \atop S_{2}} ; (∀_{n} right) ; S_{3} (cut) S_{4}  =  \begin{aligned}{α_{l} \atop S_{1}} & & {α_{r} \atop S_{2}} \\ & & & (cut) \\ & S′_{3} \end{aligned} (∀_{n} right) S_{4}

2. (∀ left) on the left permutes with (cut):

\begin{aligned}{α_{l} \atop S_{1}} ; (∀ left) ; S_{3} & {α_{r} \atop S_{2}} \\ & & (cut) \\ S_{4} \end{aligned}  =  \begin{aligned}{α_{l} \atop S_{1}} & & {α_{r} \atop S_{2}} \\ & & & (cut) \\ & S′_{3} \end{aligned} ; (∀ left) ; S_{4}

Recall that equality of derivations = means that the terms labelling the end-sequents are identical.

Other rule pairs cannot be permuted at all, either because the resulting derivation would end with a sequent containing totally different types, or because of structural mismatches in types. In particular, the following derivations ending with (cut) cannot be permuted in the same way as above because of structural mismatches in types in the premises:

• (→) on the left does not permute with (cut):

\begin{aligned}{α_{l1} \atop σ′ ⊢_{co} σ} & {α_{l2} \atop τ ⊢_{co} τ′} \\ & (→) \\ σ → τ ⊢_{co} σ′ → τ′ \end{aligned}  {α_{r} \atop σ′ → τ′ ⊢_{co} ρ}

(cut)

σ → τ ⊢_{co+cut} ρ

• (→) on the right does not permute with (cut):

{α_{l} \atop ρ ⊢_{co} σ → τ}  \begin{aligned}{α_{r1} \atop σ′ ⊢_{co} σ} & {α_{r2} \atop τ ⊢_{co} τ′} \\ & (→) \\ σ → τ ⊢_{co} σ′ → τ′ \end{aligned}

(cut)

ρ ⊢_{co+cut} σ′ → τ′

• (∀ left) on the right does not permute with (cut):

{α_{l} \atop μ ⊢_{co} ∀X.σ}  {α_{r} \atop [ρ/X]σ ⊢_{co} τ} ; (∀ left) ; ∀X.σ ⊢_{co} τ

(cut)

μ ⊢_{co+cut} τ

• (∀_{n} right) on the left does not permute with (cut):

{α_{l} \atop σ ⊢_{co} τ_{1} → … (τ_{n} → τ) …)} ; (∀_{n} right) ; σ ⊢_{co} τ_{1} → … (τ_{n} → ∀X.τ) …)  {α_{r} \atop τ_{1} → … (τ_{n} → ∀X.τ) …) ⊢_{co} ρ}

(cut)

σ ⊢_{co+cut} ρ

4.3 Atomic derivations

The following notion of “atomic” derivations is defined for System Co^{⊢} only.

Definition (Atomic derivation) An atomic derivation is one in which all axioms are of the form x:X ⊢_{co} x : X.

Lemma 10 Every derivation is =_{η} to an atomic derivation.

Proof: Let α be a derivation of x:σ ⊢_{co} M : τ. If α is not atomic then an axiom of the form x:ρ ⊢_{co} x : ρ where ρ is not a type variable, is used at a leaf. It suffices to prove the thesis for such axioms. Proceed by case analysis of the structure of ρ.

Case: ρ = ∀X.ρ′. Construct then the following atomic derivation:

y:[X/X]ρ′ ⊢_{co} y : ρ′
(∀ left)
x:∀X.ρ′ ⊢_{co} xX : ρ′
(∀_{0} right)
x:∀X.ρ′ ⊢_{co} λX.xX : ∀X.ρ′

where λX.xX =_{η} x.

Case: ρ = ρ_{1} → ρ_{2}. Construct the following atomic derivation:

y:ρ_{1} ⊢_{co} y : ρ_{1} y′:ρ_{2} ⊢_{co} y′ : ρ_{2}
(→)
x:ρ_{1} → ρ_{2} ⊢_{co} λy:ρ_{1}.xy : ρ_{1} → ρ_{2}

where λy:ρ_{1}.xy =_{η} x.

Atomic derivations simplify matters in the rest of this section by allowing us to work up to = with atomic derivations, instead of up to =_{η} with general derivations.

In the following lemma, we “transform” atomic derivations to a useful form (for later purposes) by permuting rules as appropriate.

Lemma 11 (Transforming atomic derivations) Let α be an atomic derivation of x: σ ⊢_{co} M : τ_{1} → (… (τ_{n} → ∀X.τ) …). Then, there exists an atomic derivation α′ = α, with α and α′ of equal size, and where (∀_{n} right) is the last rule used in α′.

Proof: Proceed by induction on the derivation of α. Clearly, (ax) cannot have been used, and if (∀_{n} right) was used last in α, then we are done. In the other two cases, use Lemma 8 to permute rules as follows:

Case: (∀ left) used last. Apply the induction hypothesis to the premise then permute (∀ left) with (∀_{n} right) (Lemma 8, case 1).

Case: (→) used last. Apply the induction hypothesis to the left premise then permute (→) with (∀_{n−1} right), the latter becoming (∀_{n} right) in the final derivation (Lemma 8, case 2).

Lemma 12 Let α_{1} and α_{2} be two atomic derivations of x:σ ⊢_{co} M:τ and x:σ ⊢_{co} N:τ respectively. Then, there exist atomic derivations α′_{1} = α_{1} and α′_{2} = α_{2} such that α′_{1} and α′_{2} end with the same rule.

Proof: If α_{1} and α_{2} end with the same rule, then, trivially, we are done. Otherwise, based on the structure of σ and τ, it is sufficient to consider two cases: either α_{1} ends with (∀_{n} right) and α_{2} with (→), or α_{1} ends with (∀_{n} right) and α_{2} with (∀ left). In the first case, the end sequent in both derivations must be of the form x: σ ⊢_{co} M : τ_{1} → ∀X.τ_{2}. Apply then Lemma 11 to α_{2} yielding a derivation α′_{2} = α_{2} ending with (∀_{n} right), and take α′_{1} ≡ α_{1}. The second case is treated likewise. If α_{1} ends with (∀_{n} right), apply Lemma 11 to α_{2} yielding a derivation α′_{2} = α_{2} ending with (∀_{n} right). Take α′_{1} ≡ α_{1}.

5 Coherence of Co^{⊢}

By coherence, we mean that a coercion from type σ to type τ should be independent of its derivation in Co^{⊢}, in the sense that if a coercion from σ to τ exists, then it is unique, up to =_{ηco}.

We are now in a position to prove the coherence of Co^{⊢} derivations. Note that this is where =_{ηco} and thus the rule (eq appl2 co) is used.

Theorem 13 (Coherence of Co^{⊢} derivations) Let α_{1} and α_{2} be two derivations of x:σ ⊢_{co} M:τ and x:σ ⊢_{co} N:τ respectively. Then, α_{1} =_{ηco} α_{2}.

Proof: By Lemmas 10 and 12, there exist atomic derivations α′_{1} =_{η} α_{1} and α′_{2} =_{η} α_{2} such that α′_{1} and α′_{2} both end with the same rule. The proof is easy now. However, it uses induction in a peculiar way (which stresses the strength of (eq appl2 co)). Consider the obvious syntactic length of a type. Then the induction is on the length of τ, when x:σ ⊢_{co} M:τ is the final sequent.

Case: (→) applied last. Use induction and (eq →).

Case: (∀_{n} right) applied last. Use induction and (eq ∀_{n} right).

Case: (∀ left) applied last. In this case, the length of τ is not changed, but we do not need the inductive hypothesis, here, in view of (eq appl2 co)

Indeed, the final steps in α′_{1} and α′_{2} are respectively:

{α_{l} \atop y_{1} :[τ_{1}/X]σ ⊢_{co} N_{1} :τ} ; (∀ left) ; x:∀X.σ ⊢_{co} [xτ_{1}/y_{1}]N_{1} :τ  {α_{r} \atop y_{2} :[τ_{2}/X]σ ⊢_{co} N_{2} :τ} ; (∀ left) ; x:∀X.σ ⊢_{co} [xτ_{2}/y_{2}]N_{2} :τ

Now, use (eq appl2 co) on both premises:

{α_{l} \atop y_{1} :[τ_{1}/X]σ ⊢_{co} N_{1} :τ}  {α_{r} \atop y_{2} :[τ_{2}/X]σ ⊢_{co} N_{2} :τ}

(eq appl2 co)

x:∀X.σ ⊢_{co} [xτ_{1}/y_{1}]N_{1} =_{ηco} [xτ_{2}/y_{2}]N_{2}

Hence, by definition, α′_{1} =_{ηco} α′_{2}.

It will be an easy corollary of coherence and the admissibility of (cut) in the next section that x: σ ⊢_{co} M : τ and x: τ ⊢_{co} N : σ implies that σ is isomorphic to τ. In other words, ⊢_{co} is anti-symmetric up to isomorphism.

6 Admissibility of Cut

In this section, we show that ⊢_{co} is a transitive relation.

The reader may wonder why a full section is needed to prove “cut-elimination” for a subsystem of System F. The point is that normalization and cut-elimination results are not inherited by subsystems; we will discuss the issue more closely after the proof of the main theorem.

Theorem 14 (Cut-elimination) Every derivation in Co^{⊢}+(cut) is equal (=) to a cut-free derivation, i.e., a derivation in Co^{⊢}.

Proof: By induction on the size of the derivation. Note that derivations here are not atomic. We prove the theorem for derivations with one application of (cut) in the end. Cut-elimination then holds for derivations with arbitrary numbers of cuts by simply eliminating the cuts one by one beginning with uppermost cuts. Consider then the first application of (cut) in a derivation:

\begin{aligned}{α_{l} \atop S_{L}} & & {α_{r} \atop S_{R}} \\ & & & (cut) \\ & S \end{aligned}

The derivations of S_{L} and S_{R} are cut-free, i.e., α_{l} and α_{r} are ⊢_{co} derivations, whereas S is a ⊢_{co+cut} sequent. We proceed by case analysis of the last rule used in these derivations.

\underline{Case:} S_{R} derived by (ax). The derivation of S looks like:

{α_{l} \atop x:σ ⊢_{co} M : τ}  y:τ ⊢_{co} y : τ

(cut)

x:σ ⊢_{co+cut} [M/y]y : τ

Clearly, this derivation is = to the derivation of the left premise, which is cutfree.

\underline{Case:} S_{L} derived by (ax). The derivation of S looks like:

x:σ ⊢_{co} x : σ  {α_{r} \atop y:σ ⊢_{co} N : ρ}

(cut)

x:σ ⊢_{co+cut} [x/y]N : ρ Take the derivation α_{r} of the right premise S_{R} ≡ y: σ ⊢_{co} N : ρ. Everywhere that y occurs, replace it by x. This can be done without fear of wrong variable capture because the derivation of S is a pure variable one: since x occurs free in S_{L}, it does not occur bound in S_{R}. The “renamed” derivation of S_{R}, which is cut-free, is then = to the derivation of S.

\underline{Case:} S_{R} derived by (∀_{n} right). First, permute (∀_{n} right) on the right with (cut) by Lemma 9, case 1:

{α_{l} \atop S_{L}}  {α_{r} \atop S_{2}} ; (∀_{n} right) ; S_{R} (cut) S  =  \begin{aligned}{α_{l} \atop S_{L}} & & {α_{r} \atop S_{2}} \\ & & & (cut) \\ & S′_{R} \end{aligned} (∀_{n} right) S

By induction, there exists an equal cut-free derivation of S′_{R}, which replaces the one with (cut).

\underline{Case:} S_{L} derived by (∀ left). First, permute (∀ left) on the left with (cut) by Lemma 9, case 2:

\begin{aligned}{α_{l} \atop S_{1}} ; (∀ left) ; S_{L} & {α_{r} \atop S_{R}} \\ & & (cut) \\ S \end{aligned}  =  \begin{aligned}{α_{l} \atop S_{1}} & & {α_{r} \atop S_{R}} \\ & & & (cut) \\ & S′_{L} \end{aligned} ; (∀ left) ; S

\underline{Case:} S_{L} derived by (→). The cut formula is a → type so S_{R} was derived either by (∀_{n} right) or (→). The first of these subcases has been treated already, by permuting the (cut).

Subcase: S_{R} derived by (→). This is a situation where (cut) cannot be permuted “as such” (see page 17). The derivation of S looks like:

\begin{aligned}{α_{l1} \atop x′:σ′ ⊢_{co} M:σ} & {α_{l2} \atop y:τ ⊢_{co} N:τ′} \\ & (→) \\ x:σ → τ ⊢_{co} P_{1} : σ′ → τ′ \end{aligned}  \begin{aligned}{α_{r1} \atop x′′:σ′′ ⊢_{co} M′:σ′} & {α_{r2} \atop y′:τ′ ⊢_{co} N′:τ′′} \\ & (→) \\ z:σ′ → τ′ ⊢_{co} P_{2} : σ′′ → τ′′ \end{aligned}

(cut)

x:σ → τ ⊢_{co+cut} P : σ′′ → τ′′

where \begin{aligned}P_{1} & ≡ & λx′:σ′ . [xM/y]N \\ P_{2} & ≡ & λx′′:σ′′ . [zM′/y′]N′ \\ P & ≡ & nf([P_{1}/z]P_{2}) \\ & ≡ & nf(λx′′:σ′′ . [(λx′:σ′.[xM/y]N)/z][zM′/y′]N′) \end{aligned}

First, rearrange the derivations of the premises to apply (cut) earlier and (→) last:

\begin{aligned}{α_{r1} \atop x′′:σ′′ ⊢_{co} M′:σ′} & {α_{l1} \atop x′:σ′ ⊢_{co} M:σ} \\ & (cut) \\ x′′:σ′′ ⊢_{co+cut} nf([M′/x′]M) : σ \end{aligned}  \begin{aligned}{α_{l2} \atop y:τ ⊢_{co} N:τ′} & {α_{r2} \atop y′:τ′ ⊢_{co} N′:τ′′} \\ & (cut) \\ y:τ ⊢_{co+cut} nf([N/y′]N′) : τ′′ \end{aligned}
(→)
x:σ → τ ⊢_{co+cut} Q : σ′′ → τ′′

where Q ≡ λx′′:σ′′ . [x(nf([M′/x′]M))/y] nf([N/y′]N′).

By induction, there exist equal cut-free derivations of the premises to replace the ones with (cut). The labels of these cut-free derivations are the same coercions nf([M′/x′]M) and nf([N/y′]N′). Since the (→) rule preserves coercions, the term Q is a coercion and is in β-nf, i.e., nf(Q) ≡ Q. Finally, we prove P ≡ Q as follows. Note that we make use of Lemma 1, that coercions contain at most one free term variable, given by their environment.

P ≡ nf(λx′′:σ′′ . [(λx′:σ′.[xM/y]N)/z][zM′/y′]N′)
≡ nf(λx′′:σ′′ . [(λx′:σ′.[xM/y]N)M′/y′]N′) z not free in M′, N′
≡ nf(λx′′:σ′′ . [[M′/x′]([xM/y]N)/y′]N′)

β-reduction inside nf preserves β-nf

≡ nf(λx′′:σ′′ . [([x([M′/x′]M)/y]N)/y′]N′)  x′ not free in N
≡ nf(λx′′:σ′′ . [x([M′/x′]M)/y]([N/y′]N′))  y not free in N′
≡ nf(λx′′:σ′′ . [x(nf([M′/x′]M))/y] nf([N/y′]N′))

Strong Normalization

≡ nf(Q)
≡ Q

\underline{Case:} S_{L} derived by (∀_{n} right). This is another situation where (cut) cannot be permuted “as such” (see page 17). The derivation of S looks like:^{2}

{α_{l} \atop x:σ ⊢_{co} P′ : τ_{1} → … τ_{n} → τ} ; (∀_{n} right) ; x:σ ⊢_{co} P : τ_{1} → … τ_{n} → ∀X.τ  {α_{r} \atop z:τ_{1} → … τ_{n} → ∀X.τ ⊢_{co} Q : ρ}

(cut)

x:σ ⊢_{co+cut} R : ρ

where

P′ ≡ λx_{1} :τ_{1} … x_{k}:τ_{k}.M  where M does not start with λy
P ≡ \begin{cases}λx_{1} :τ_{1} … λx_{k}:τ_{k} … λx_{n}:τ_{n}.λX.Mx_{k+1} … x_{n} & for 0 ≤ k ≤ n \\ λx_{1} :τ_{1} … λx_{n}:τ_{n}.λX.λx_{n+1} :τ_{n+1} … λx_{k}:τ_{k}.M & for 0 ≤ n < k \end{cases}
R ≡ nf([P/z]Q)

and X not free in σ nor in τ_{1}, …, τ_{n}. Moreover, by the definition of pure variable derivation, X is also not free in ρ.

Proceed now by analysis of the cut-free right derivation:

{α_{r} \atop z:τ_{1} → … τ_{n} → ∀X.τ ⊢_{co} Q : ρ}

Observe that ρ will have the following general form:

ρ ≡ ρ_{1} → … ρ_{m} → ρ′

2In the proof of this case, we will minimise the number of brackets () by employing the standard convention that → associates to the right. Thus, for example, instead of writing τ_{1} → (… → (τ_{n} → τ) …) we will write τ_{1} → … τ_{n} → τ.

for some 0 ≤ m and some types ρ_{1}, …, ρ_{m}, ρ′. It can be proven, by induction on n, that the derivation α_{r} satisfies at least one of the following cases:

Subcase 1: ρ′ ≡ ∀Y.ρ′′, and the “∀Y ” can be traced back to an application of (∀_{m−j} right) for some 0 ≤ j ≤ m. The derivation α_{r} looks like:

{γ_{1} \atop y_{1} :ρ_{1} ⊢_{co} M_{1} :τ_{1}} {γ_{j} \atop y_{j}:ρ_{j} ⊢_{co} M_{j}:τ_{j}}  γ′ ; \begin{matrix}z_{j}:τ_{j+1} → … τ_{n} → ∀X.τ \\ ⊢_{co} Q′_{j}:ρ_{j+1} → … ρ_{m} → ρ′′ \end{matrix} ; \overline{(∀_{m−j} right)} ; \begin{matrix}z_{j}:τ_{j+1} → … τ_{n} → ∀X.τ \\ ⊢_{co} Q_{j}:ρ_{j+1} → … ρ_{m} → ∀Y.ρ′′ \end{matrix} ; (→) ; \begin{matrix}· \\ · \\ · \\ · \end{matrix} ; (→) ; \begin{matrix}z_{1} :τ_{2} → … τ_{n} → ∀X.τ \\ ⊢_{co} Q_{1} :ρ_{2} → … ρ_{j} → ρ_{j+1} → … ρ_{m} → ∀Y.ρ′′ \end{matrix}
(→)

z:τ_{1} → … τ_{n} → ∀X.τ ⊢_{co} Q:ρ_{1} → … ρ_{j} → ρ_{j+1} → … ρ_{m} → ∀Y.ρ′′

Subcase 2: m = n and, for some 0 ≤ j ≤ m, ρ_{j+1} ≡ τ_{j+1}, …, ρ_{n} ≡ τ_{n}, ρ′ ≡ ∀X.τ, and the “∀X” in ∀X.τ can be traced back to an occurrence of an axiom. The derivation α_{r} looks like:

{γ_{1} \atop y_{1} :ρ_{1} ⊢_{co} M_{1} :τ_{1}} {γ_{j} \atop y_{j}:ρ_{j} ⊢_{co} M_{j}:τ_{j}}  \begin{matrix}z_{j}:τ_{j+1} → … τ_{n} → ∀X.τ \\ ⊢_{co} z_{j}:τ_{j+1} → … τ_{n} → ∀X.τ \end{matrix} ; (→) ; \begin{matrix}z_{j−1} :τ_{j} → … τ_{n} → ∀X.τ \\ ⊢_{co} Q_{j−1} :ρ_{j} → τ_{j+1} → … τ_{n} → ∀X.τ \end{matrix} ; \begin{matrix}· \\ · \\ · \\ · \end{matrix} ; (→) ; \begin{matrix}z_{1} :τ_{2} → … τ_{n} → ∀X.τ \\ ⊢_{co} Q_{1} :ρ_{2} → … ρ_{j} → τ_{j+1} → … τ_{n} → ∀X.τ \end{matrix}
(→)

z:τ_{1} → … τ_{n} → ∀X.τ ⊢_{co} Q:ρ_{1} → … ρ_{j} → τ_{j+1} → … τ_{n} → ∀X.τ

where Q_{j−1} ≡ λy_{j}:ρ_{j} . [(z_{j−1} M_{j})/z_{j}]z_{j} ≡ λy_{j}:ρ_{j} . z_{j−1} M_{j} ; ⋮ ; Q_{1} ≡ λy_{2} :ρ_{2} . [(z_{1} M_{2})/z_{2}]Q_{2} ; Q ≡ λy_{1} :ρ_{1} . [(z M_{1})/z_{1}]Q_{1} ; ≡ λy_{1} :ρ_{1} … λy_{j}:ρ_{j} . z M_{1} … M_{j}

The fact that each term variable z_{1}, …, z_{j} occurs in a coercion term only once (Lemma 1) has been used.

Subcase 3: n ≤ m, and the “∀X” in ∀X.τ can be traced back to an application of (∀ left). The derivation α_{r} looks like:

{γ_{1} \atop y_{1} :ρ_{1} ⊢_{co} M_{1} :τ_{1}} {γ_{n} \atop y_{n}:ρ_{n} ⊢_{co} M_{n}:τ_{n}} {γ′ \atop z′_{n}:[μ/X]τ ⊢_{co} Q′_{n}:ρ_{n+1} → … ρ_{m} → ρ′} ; \overline{(∀ left)} ; z_{n}:∀X.τ ⊢_{co} Q_{n}:ρ_{n+1} → … ρ_{m} → ρ′ ; (→) ; \begin{matrix}· \\ · \\ · \\ · \end{matrix} ; (→) ; \begin{matrix}z_{1} :τ_{2} → … τ_{n} → ∀X.τ \\ ⊢_{co} Q_{1} :ρ_{2} → … ρ_{n} → ρ_{n+1} → … ρ_{m} → ρ′ \end{matrix}
(→)

z:τ_{1} → … τ_{n} → ∀X.τ ⊢_{co} Q:ρ_{1} → … ρ_{n} → ρ_{n+1} → … ρ_{m} → ρ′

where Q_{n} ≡ [(z_{n} μ)/z′_{n}]Q′_{n} ; Q_{n−1} ≡ λy_{n}:ρ_{n} . [(z_{n−1} M_{n})/z_{n}]Q_{n} ; ⋮ ; Q_{1} ≡ λy_{2} :ρ_{2} . [(z_{1} M_{2})/z_{2}]Q_{2} ; Q ≡ λy_{1} :ρ_{1} . [(z M_{1})/z_{1}]Q_{1} ; ≡ λy_{1} :ρ_{1} … λy_{n}:ρ_{n}.[(z M_{1} … M_{n})/z_{n}]Q_{n} ; ≡ λy_{1} :ρ_{1} … λy_{n}:ρ_{n} . [(z M_{1} … M_{n} μ)/z′_{n}]Q′_{n}

Again, the fact that each term variable z_{1}, …, z_{n} occurs in a coercion term only once (Lemma 1) has been used.

Now, return to the main derivation with cut and proceed by case analysis according to the three subcases above for the right derivation.

Subcase 1: Apply Lemma 8, case 2, to the right derivation, permuting the (∀_{m−j} right) downwards with (→) j times, so that it becomes (∀_{m} right) just before the (cut). By this same lemma, the terms labelling the end sequents in the two derivations are identical, i.e., Q. The modified derivation is then a case (S_{R} derived by (∀ right)) that has been treated before: just permute the (∀_{m} right) with (cut) by Lemma 9, case 1 then apply the induction hypothesis to the upper derivation ending with (cut).

Subcase 2: In this case, we will transform both the left and right derivations α_{l} and α_{r} of the main derivation so as to apply (cut) in a derivation of lesser size. First, in the right derivation α_{r}, replace the axiom:

z_{j}:τ_{j+1} → … τ_{n} → ∀X.τ ⊢_{co} z_{j}:τ_{j+1} → … τ_{n} → ∀X.τ

by:

z′_{j}:τ_{j+1} → … τ_{n} → τ ⊢_{co} z′_{j}:τ_{j+1} → … τ_{n} → τ

Keeping all other derivations the same, apply the same rules in the same order so that all occurrences of ∀X.τ are ultimately replaced by τ. The result is the derivation:

{α′_{r} \atop z′:τ_{1} → … τ_{n} → τ ⊢_{co} Q′:ρ_{1} → … ρ_{j} → τ_{j+1} → … τ_{n} → τ}

where Q′ ≡ λy_{1} :ρ_{1} … λy_{j}:ρ_{j} . z′ M_{1} … M_{j}. Second, in the left derivation α_{l}, omit the last (∀_{n} right) thus obtaining the subderivation:

{α_{l} \atop x:σ ⊢_{co} P′ : τ_{1} → … τ_{n} → τ}

where P′ ≡ λx_{1} :τ_{1} … λx_{k}:τ_{k} . M for some M not starting with λy.

Now, apply (cut) to these two derivations followed by (∀_{n} right):

{α_{l} \atop x:σ ⊢_{co} P′:τ_{1} → … τ_{n} → τ}  α′_{r} ; \begin{matrix}z′:τ_{1} → … τ_{n} → τ \\ ⊢_{co} Q′:ρ_{1} → … ρ_{j} → τ_{j+1} → … τ_{n} → τ \end{matrix}

(cut)

x:σ ⊢_{co+cut} R′:ρ_{1} → … ρ_{j} → τ_{j+1} → … τ_{n} → τ

(∀_{n} right)
x:σ ⊢_{co+cut} R′′:ρ_{1} → … ρ_{j} → τ_{j+1} → … τ_{n} → ∀X.τ

where R′ ≡ nf([P′/z′]Q′). Note that the side-conditions on applying (∀_{n} right) are satisfied since X is not free in σ nor in τ_{j+1}, …, τ_{n} by the application of (∀_{n} right) in the original derivation with cut, and X is not free in ρ ≡ ρ_{1} → … ρ_{j} → … ρ_{n} → ∀X.τ since the original derivation is a pure variable one. Observe that the (cut) above occurs in a derivation of lesser size than in the original derivation. Hence, we can eliminate the cut by induction, obtaining a cut-free derivation with the same label R′, which is thus a coercion. Since (∀_{n} right) preserves coercions, R′′ is likewise a coercion. We must now show that R′′ ≡ R where R is the term labelling the original derivation with (cut). Recall that R is given by:

R ≡ nf([P/z]Q)
P ≡ \begin{cases}λx_{1} :τ_{1} … λx_{k}:τ_{k} … λx_{n}:τ_{n}.λX . Mx_{k+1} … x_{n} & for k ≤ n \\ λx_{1} :τ_{1} … λx_{n}:τ_{n}.λX.λx_{n+1} :τ_{n+1} … λx_{k}:τ_{k} . M & for n < k \end{cases}

and that Q is given by:

Q ≡ λy_{1} :ρ_{1} … λy_{j}:ρ_{j} . z M_{1} … M_{j}

Recall also that, for i = 1 … j,

y_{i}:ρ_{i} ⊢_{co} M_{i}:τ_{i}

Taking into account that j ≤ n, we proceed now by the three cases j ≤ k ≤ n, k < j ≤ n and j ≤ n < k. To save on space, we will not write the types of bound term variables, nor multiple term λs (thus writing, for example, just λx_{1} … x_{n}.M instead of λx_{1} :τ_{1} … λx_{n}:τ_{n}.M).

• For j ≤ k ≤ n

R ≡ nf([P/z]Q)
≡ nf(λy_{1} … y_{j} . ((λx_{1} … x_{k} … x_{n}.λX.Mx_{k+1} … x_{n}) M_{1} … M_{j}))

definition of Q, P

≡ nf(λy_{1} … y_{j} . ([M_{j}/x_{j}] … [M_{1}/x_{1}](λx_{j+1} … x_{n}.λX.M x_{k+1} … x_{n})))

β-reduction inside nf

≡ nf(λy_{1} … y_{j}.x_{j+1} … x_{n} . λX.[M_{j}/x_{j}] … [M_{1}/x_{1}](M x_{k+1} … x_{n}))
≡ nf(λy_{1} … y_{j}.x_{j+1} … x_{n} . λX.([M_{j}/x_{j}] … [M_{1}/x_{1}]M) x_{k+1} … x_{n})
term substitution where x_{k+1}, …, x_{n} were fresh
≡ λy_{1} … y_{j}.x_{j+1} … x_{n} . λX.nf(([M_{j}/x_{j}] … [M_{1}/x_{1}]M) x_{k+1} … x_{n})

and

R′ ≡ nf([P′/z′]Q′)
≡ nf(λy_{1} … y_{j} . ((λx_{1} … x_{k} . M) M_{1} … M_{j})) definition of Q′, P′
≡ nf(λy_{1} … y_{j} . x_{j+1} … x_{k} . [M_{j}/x_{j}] … [M_{1}/x_{1}]M)

β-reduction inside nf

≡ λy_{1} … y_{j} . x_{j+1} … x_{k} . nf([M_{j}/x_{j}] … [M_{1}/x_{1}]M)

Recall that M does not begin with λy and, by Lemma 1, the free variable x is its leftmost variable. Thus, the inner nf term of R′ does not begin with a λy. The application of (∀_{n} right) to R′ is thus allowed and yields R′′ as follows, which is equal to R:

R′′ ≡ λy_{1} … y_{j} . x_{j+1} … x_{k} … x_{n}.λX.
(nf([M_{j}/x_{j}] … [M_{1}/x_{1}]M)) x_{k+1} … x_{n}

(∀_{n} right) applied to R′

≡ λy_{1} … y_{j} . x_{j+1} … x_{k} … x_{n}.λX.
nf(([M_{j}/x_{j}] … [M_{1}/x_{1}]M) x_{k+1} … x_{n})

nf does not begin with λy

≡ R

• For k < j ≤ n

R ≡ nf([P/z]Q)
≡ nf(λy_{1} … y_{j} . ((λx_{1} … x_{k} … x_{n}.λX.Mx_{k+1} … x_{n}) M_{1} … M_{j}))

definition of Q, P

≡ nf(λy_{1} … y_{j} . ([M_{j}/x_{j}] … [M_{1}/x_{1}](λx_{j+1} … x_{n}.λX.M x_{k+1} … x_{n})))

β-reduction inside nf

≡ nf(λy_{1} … y_{j}.x_{j+1} … x_{n} . λX.[M_{j}/x_{j}] … [M_{1}/x_{1}](M x_{k+1} … x_{n}))
≡ nf(λy_{1} … y_{j}.x_{j+1} … x_{n} . λX.([M_{j}/x_{j}] … [M_{1}/x_{1}]M) M_{k+1} … M_{j} x_{j+1} … x_{n})

term substitution and by Lemma 1, y_{i} is only free term variable in M_{i}, i = 1 … j

≡ nf(λy_{1} … y_{j}.x_{j+1} … x_{n} . λX.([M_{k}/x_{k}] … [M_{1}/x_{1}]M) M_{k+1} … M_{j} x_{j+1} … x_{n})
F V (M) = x, x_{1} …, x_{k}
≡ λy_{1} … y_{j}.x_{j+1} … x_{n} . λX.nf(([M_{k}/x_{k}] … [M_{1}/x_{1}]M) M_{k+1} … M_{j} x_{j+1} … x_{n})

and

R′ ≡ nf([P′/z′]Q′)
≡ nf(λy_{1} … y_{j} . ((λx_{1} … x_{k} . M) M_{1} … M_{j})) definition of Q′, P′
≡ nf(λy_{1} … y_{j} . ([M_{k}/x_{k}] … [M_{1}/x_{1}]M) M_{k+1} … M_{j})

β-reduction inside nf

≡ λy_{1} … y_{j} . nf(([M_{k}/x_{k}] … [M_{1}/x_{1}]M) M_{k+1} … M_{j})

As before, the inner nf term of R′ does not begin with a λy. The application of (∀_{n} right) to R′ is thus possible yielding R′′, which is equal to R:

R′′ ≡ λy_{1} … y_{j} . x_{j+1} … x_{n}.λX.

nf(([M_{k}/x_{k}] … [M_{1}/x_{1}]M) M_{k+1} … M_{j}) x_{j+1} … x_{n}

≡ R

• For 0 ≤ j ≤ n < k

R ≡ nf([P/z]Q)
≡ nf(λy_{1} … y_{j} . ((λx_{1} … x_{n}.λX.λx_{n+1} … x_{k} . M) M_{1} … M_{j}))

definition of Q, P

≡ nf(λy_{1} … y_{j} . ([M_{j}/x_{j}] … [M_{1}/x_{1}](λx_{j+1} … x_{n}.λX.λx_{n+1} … x_{k} . M)))

β-reduction inside nf

≡ nf(λy_{1} … y_{j}.x_{j+1} … x_{n}.λX.λx_{n+1} … x_{k} . [M_{j}/x_{j}] … [M_{1}/x_{1}]M)
≡ λy_{1} … y_{j}.x_{j+1} … x_{n}.λX.λx_{n+1} … x_{k} . nf([M_{j}/x_{j}] … [M_{1}/x_{1}]M)

and

R′ ≡ nf(λy_{1} … y_{j} . P′ M_{1} … M_{j})
≡ nf(λy_{1} … y_{j} . ((λx_{1} … x_{k} . M) M_{1} … M_{j}))  definition of P′
≡ nf(λy_{1} … y_{j} . ([M_{j}/x_{j}] … [M_{1}/x_{1}](λx_{j+1} … x_{k}.M)))

β-reduction inside nf

≡ nf(λy_{1} … y_{j}.x_{j+1} … x_{k} . ([M_{j}/x_{j}] … [M_{1}/x_{1}]M))
≡ λy_{1} … y_{j}.x_{j+1} … x_{k} . nf([M_{j}/x_{j}] … [M_{1}/x_{1}]M)

As before, the inner nf term in R′ does not begin with a λy. The application of (∀_{n} right) to R′ is thus possible, and yields R′′ as follows which is equal to R:

R′′ ≡ λy_{1} … y_{j}.x_{j+1} … x_{n}.λX.λx_{n+1} … x_{k} . nf([M_{j}/x_{j}] … [M_{1}/x_{1}]M)

(∀_{n} right) applied to R′

≡ R

Subcase 3: As in the previous case, we will transform both the left and the right derivations of the main derivation so as to apply (cut) in a derivation of lesser size. First, in the right derivation α_{r}, omit (∀ left) but keep all subsequent rule applications the same. This results in the derivation:

{α′_{r} \atop z′:τ_{1} → … τ_{n} → [μ/X]τ ⊢_{co} Q′:ρ}

where Q′ ≡ λy_{1} :ρ_{1} … λy_{n}:ρ_{n} . [(z′ M_{1} … M_{n})/z′_{n}]Q′_{n}. Second, in the left derivation α_{l}, omit the last (∀_{n} right) thus obtaining the subderivation:

{α_{l} \atop x:σ ⊢_{co} P′:τ_{1} → … τ_{n} → τ}

where P′ ≡ λx_{1} : τ_{1} … λx_{k}: τ_{k}.M for some M not starting with λy. In this subderivation, uniformly substitute μ for X to obtain:

{α′_{l} \atop x:σ ⊢_{co} [μ/X]P′:τ_{1} → … τ_{n} → [μ/X]τ}

Remember that X is not free in σ nor in τ_{1}, …, τ_{n}. Now, apply (cut) to these two derivations:

{α′_{l} \atop x:σ ⊢_{co} [μ/X]P′:τ_{1} → … τ_{n} → [μ/X]τ} {α′_{r} \atop z′:τ_{1} → … τ_{n} → [μ/X]τ ⊢_{co} Q′:ρ}

(cut)

x:σ ⊢_{co+cut} R′:ρ

where R′ ≡ nf([([μ/X]P′)/z′]Q′). Observe that the cut occurs in a derivation of lesser size than in the original derivation. Hence, eliminate the (cut) by induction, obtaining a cut-free derivation with the same label R′ which is thus a coercion. We must now show that R′ ≡ R where R is the term labelling the original derivation with (cut). Recall that R is given by:

R ≡ nf([P/z]Q)
P ≡ \begin{cases}λx_{1} :τ_{1} … λx_{k}:τ_{k} … λx_{n}:τ_{n}.λX.Mx_{k+1} … x_{n} & for 0 ≤ k ≤ n \\ λx_{1} :τ_{1} … λx_{n}:τ_{n}.λX.λx_{n+1} :τ_{n+1} … λx_{k}:τ_{k}.M & for 0 ≤ n < k \end{cases}

and that Q is given by:

Q ≡ λy_{1} :ρ_{1} … λy_{n}:ρ_{n} . [(z M_{1} … M_{n} μ)/z′_{n}]Q′_{n}

Recall also that, for i = 1 … n,

y_{i}:ρ_{i} ⊢_{co} M_{i}:τ_{i}

We proceed now by the two cases k ≤ n and n < k. And, as before, we save on space by not writing the types of bound term variables, nor multiple term λs.

• For 0 ≤ k ≤ n

R ≡ nf([P/z]Q)
≡ nf(λy_{1} … y_{n} .

[((λx_{1} … x_{k} … x_{n}.λX.Mx_{k+1} … x_{n}) M_{1} … M_{n} μ)/z′_{n}]Q′_{n})

definition of Q, P

≡ nf(λy_{1} … y_{n} .
[([μ/X][M_{n}/x_{n}] … [M_{k}/x_{k}] … [M_{1}/x_{1}](M x_{k+1} … x_{n}))/z′_{n}]Q′_{n})

β-reduction inside nf

≡ nf(λy_{1} … y_{n} . [([μ/X](([M_{n}/x_{n}] … [M_{1}/x_{1}]M) M_{k+1} … M_{n}))/z′_{n}]Q′_{n})

term substitution and by Lemma 1,

y_{i} is only free term variable in M_{i}, i = 1 … n

≡ nf(λy_{1} … y_{n} . [([μ/X](([M_{k}/x_{k}] … [M_{1}/x_{1}]M) M_{k+1} … M_{n}))/z′_{n}]Q′_{n})
F V (M) = x, x_{1} … x_{k}
≡ nf(λy_{1} … y_{n} . [(([M_{k}/x_{k}] … [M_{1}/x_{1}][μ/X]M) M_{k+1} … M_{n})/z′_{n}]Q′_{n})

X not free in M_{1}, …, M_{n} because ???

and

[μ/X]P′ ≡ [μ/X](λx_{1} :τ_{1} … λx_{k}:τ_{k}.M)
≡ λx_{1} :τ_{1} … λx_{k}:τ_{k} . [μ/X]M  X not free in τ_{1}, …, τ_{n}

and

R′ ≡ nf([([μ/X]P′)/z′]Q′)
≡ nf(λy_{1} … y_{n} . [((λx_{1} … x_{k}.[μ/X]M) M_{1} … M_{n})/z′_{n}]Q′_{n})

definition of Q′, [μ/X]P′

≡ nf(λy_{1} … y_{n} . [(([M_{k}/x_{k}] … [M_{1}/x_{1}][μ/X]M) M_{k+1} … M_{n})/z′_{n}]Q′_{n})

β-reduction inside nf

≡ R

• For 0 ≤ n < k

R ≡ nf([P/z]Q)
≡ nf(λy_{1} … y_{n} .

[((λx_{1} :τ_{1} … λx_{n}:τ_{n}.λX.λx_{n+1} :τ_{n+1} … λx_{k}:τ_{k}.M)

M_{1} … M_{n} μ)/z′_{n}]Q′_{n}) definition of Q, P

≡ nf(λy_{1} … y_{n} .

[([μ/X][M_{n}/x_{n}] … [M_{1}/x_{1}](λx_{n+1} :τ_{n+1} … λx_{k}:τ_{k}.M))/z′_{n}]Q′_{n})

β-reduction inside nf

≡ nf(λy_{1} … y_{n} .
[(λx_{n+1} :[μ/X]τ_{n+1} … λx_{k}:[μ/X]τ_{k} .
[M_{n}/x_{n}] … [M_{1}/x_{1}][μ/X]M)/z′_{n}]Q′_{n})
X not free in M_{1}, … M_{n} because ???

and

[μ/X]P′ ≡ [μ/X](λx_{1} :τ_{1} … λx_{n}:τ_{n} … λx_{k}:τ_{k}.M)
≡ λx_{1} :τ_{1} … λx_{n}:τ_{n}.λx_{n+1} :[μ/X]τ_{n+1} … λx_{k}:[μ/X]τ_{k} . [μ/X]M
X not free in τ_{1}, …, τ_{n}

and

R′ ≡ nf([([μ/X]P′)/z′]Q′)
≡ nf(λy_{1} … y_{n} .
[((λx_{1} :τ_{1} … λx_{n}:τ_{n}.λx_{n+1} :[μ/X]τ_{n+1} … λx_{k}:[μ/X]τ_{k} .
[μ/X]M) M_{1} … M_{n})/z′_{n}]Q′_{n}) definition of Q′, [μ/X]P′′
≡ nf(λy_{1} … y_{n} .
[([M_{n}/x_{n}] … [M_{1}/x_{1}](λx_{n+1} :[μ/X]τ_{n+1} … λx_{k}:[μ/X]τ_{k} .
[μ/X]M))/z′_{n}]Q′_{n}) β-reduction inside nf
≡ nf(λy_{1} … y_{n} .
[(λx_{n+1} :[μ/X]τ_{n+1} … λx_{k}:[μ/X]τ_{k} .
[M_{n}/x_{n}] … [M_{1}/x_{1}][μ/X]M)/z′_{n}]Q′_{n})
≡ R

6.1 Remarks on the proof of cut-elimination

We have thus proven the admissibility of (cut) for the system Co^{⊢} by proving a cut-elimination theorem for the extended system Co^{⊢}+(cut). As pointed out in the introduction, if we had taken (cut) as a primitive of the system, then we would have had to eliminate it in any case in order to prove coherence. Moreover, (cut) as primitive would imply that coercions could “compute on themselves” (even without inputs), whereas the coercions provided by Co^{⊢} are guaranteed to be in β-nf. Thus, they only transform an element of a type to a supertype without any other kind of computation.

The reader may wonder why such a simple inductive proof, on the size of derivations, is possible for a system which contains higher-order types and/or why we couldn’t just derive it from the proofs of more expressive systems. It is known that impredicative second-order logic require powerful tools to yield cut-elimination or normalization proofs ([Gir71, GLT89]). For the reader interested in this issue, let’s analyse closely some analogies and differences with respect to other calculi. We use [GLT89] as a reference.

First, for a first-order system, the proof of cut-elimination considered in Chapter 13 of [GLT89] is divided into two main parts. The first part is the base for an induction on the size of derivations, like ours: ‘cuts” are swapped with other rules (and, when possible, they are moved up). Among the “key cases” there are two crucial ones: cases 6 and 7 (or 8). The first, case 6, is concerned with implication, as cut-formula. The point there is that, if one “swaps” the cut-rule with the two right and left-arrow rules, the cut-rule is NOT moved up, as in all the preceding cases, and a straightforward induction would then fail. This is the reason for introducing, in the second main part (sect. 13.2), the notion of “degree” for a formula and use a combined induction on derivations AND degrees: in case 6, sect. 13.1, the degree of cut-formulae does decrease (not the size of the derivation).

Fortunately, in the first-order case, the notion of degree for a formula doesn’t present any problem (sect. 13.2): it is preserved under instantiation of a variable by a term (e.g., d(A[t/x]) = d(A)). By this, the degree of the cut formulae in case 7 (and 8) of sect. 13.1 does not change, when moving up the cut-rule. And the combined induction goes through.

However, this form of combined induction cannot be used in the presence of higher-order formulae: no degree or measure on formulae is preserved by instantiation, in general. Girard and Tait’s proof by “candidates of reducibility” employs a powerful technique to overcome this crucial difficulty of impredicative systems. The heavy inductive loading used (conditions CR.1-2.3 of chapters 6 and 14) requires the intended set of terms (candidates of reducibility) to be closed under reductions and expansions. In our case, the difficulties of case 6 (sect. 13.1 of [GLT89]) are rather easily handled: that case corresponds to our case of (→) occurring simultaneously on the left and on the right, where an arrow formula is eliminated, by cut. This gives a symmetric situation and allows one to move up the last cut-rule, in contrast to case 6 in [GLT89]. Thus, we do not need to introduce an induction on degrees of formulae, which would, in turn, cause problems in an impredicative system, like ours. Moreover, we couldn’t even refer to nor use the candidates of reducibility, even though Co^{⊢} is a subsystem of System F: the terms of our system with the cut-rule are not closed under β-expansions (CR3), as pointed out before Lemma 5 (cut-rule coercions). Similarly, cut-elimination cannot automatically be applied to subsystems.

6.2 Bi-coercibility

Consider now the term model of | Co^{⊢} | of Co^{⊢}, i.e., the structure whose objects are types and arrows are coercions. | Co^{⊢} | is a category. Indeed, by (ax), it contains all identities. By the admissibility of (cut), arrows compose: just observe that if

x:σ ⊢_{co} M : τ and y:τ ⊢_{co} N : ρ

then there exists P such that x: σ ⊢_{co} P : ρ and P is unique by coherence. As for associativity, this is again given by coherence.

| Co^{⊢} | is even a partial order: by the corollary below, anti-symmetry of ⊢_{co} is a consequence of coherence and cut-elimination. Define first the following relation of bi-coercibility between types:

Definition (Bi-coercibility) Two types σ and τ are defined to be bi-coercible, written

σ ≅ ; b τ, iff σ ⊢_{co} τ and τ ⊢_{co} σ.

For example, τ ≅ ; b ∀X.τ for X not free in τ. Now, recall that, in a category, two objects A and B are isomorphic, A ≅ B, if there are maps f:A → B and g:B → A such that g ∘ f = id and f ∘ g = id. Thus, one can prove the following:

Corollary (Anti-symmetry) If σ ≅ ; b τ then σ ≅ τ in |Co^{⊢} |. Proof: By assumption, x : σ ⊢_{co} M : τ and y : τ ⊢_{co} N : σ. By (cut), we obtain x: σ ⊢_{co} nf([M/y]N) : σ and y: τ ⊢_{co} nf([N/x]M) : τ, then, by coherence, nf([M/y]N) =_{ηco} x and nf([N/x]M) =_{ηco} y.

Note that bi-coercibility is strictly stronger than isomorphism: the type σ → (τ → ρ) is isomorphic to τ → (σ → ρ) (see [Sol83, BDL92] for a characterisation) but it is clearly not a subtype, and so not bi-coercible.

As pointed out, | Co^{⊢} | is a category and a partial order. This allows a preliminary observation on adding base types (int, real, etc.) with axioms introducing ⊢_{co} between these types (e.g., int ⊢_{co} real). In short, one obtains the freely generated partial order, from these base types, by our axioms and rules. A proof-theoretic analysis of this fact will be given in Section 8.

7 Completeness of Co^{⊢}

The standard notion of erasure, defined as follows, will serve to characterize coercions.

Definition (Erasure) The erasure of a polymorphic term to a type-free term is defined by: erase(x) ≡ x

erase(λx:σ.M) ≡ λx.erase(M)  erase(MN) ≡ erase(M)erase(N)
erase(λX.M) ≡ erase(M)  erase(Mτ) ≡ erase(M)

It is simple to show that the erasure of a coercion η-reduces to the identity (in the typefree λ-calculus). This will be a key step in relating our system to that of Mitchell [Mit88] in the next section.

Lemma 15 (Coercions erase to identity) If x:σ ⊢_{co} M:τ then erase(M)⟶_{η} x

Conversely, any linear map in βη-nf whose erasure η-reduces to a term variable is a coercion. This gives a complete characterization of coercions. The proof proceeds by syntactic analysis of the normal form.

Theorem 16 (Completeness) Let M be a term in βη-nf such that x: σ ⊢_{F} M : τ and erase(M) ⟶_{η} x. Then, x:σ ⊢_{co} M : τ.

Proof: By induction on the structure of M and by Lemma 1 on the structure of coercions. The first step consists of identifying those subterms of M satisfying the same assumptions, i.e., linear maps in βη-nf and η-reducing to a term variable.

First, by the assumption that M is in βη-nf, M must have the following structure:

M ≡ λY⃗_{1} . λy_{1} :τ_{1} …. λY⃗_{k} . λy_{k}:τ_{k} . λY⃗_{k+1} . xρ⃗_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1}

with each subterm M_{i}, for 1 ≤ i ≤ n, in βη-nf. Furthermore, the assumption erase(M) ⟶_{η} x implies that k = n and erase(M_{i}) ⟶_{η} y_{i} for 1 ≤ i ≤ n.

Consider now the assumption x : σ ⊢_{F} M : τ. In the body of M, x occurs as xρ⃗_{1}M_{1} … ρ⃗_{n}M_{n} so the type σ of x must have the following structure:

σ = ∀X⃗_{1}.(σ_{1} → … ∀X⃗_{n}.(σ_{n} → ∀X⃗_{n+1}.σ′) …)

where, for 1 ≤ i ≤ n + 1, the vectors X⃗_{i} and ρ⃗_{i} are equal in length (|X⃗_{i}| = |ρ⃗_{i}|). Moreover, the type of each subterm M_{i}, 1 ≤ i ≤ n, must then be given by:

x:σ, y_{1} :τ_{1}, …, y_{n}:τ_{n} ⊢_{F} M_{i} : [ρ⃗_{1}/X⃗_{1}, …, ρ⃗_{i}/X⃗_{i}]σ_{i}

However, the fact that erase(M_{i}) ⟶_{η} y_{i} means that y_{i} is the only free term variable in M_{i}. So, by strengthening of F environments (cf. [CMMS91, section 2.3]), we obtain:

y_{i}:τ_{i} ⊢_{F} M_{i} : [ρ⃗_{1}/X⃗_{1}, …, ρ⃗_{i}/X⃗_{i}]σ_{i}

Thus, we have shown that the subterms M_{i}, 1 ≤ i ≤ n, are in βη-nf with erase(M_{i}) ⟶_{η} y_{i} and y_{i}: τ_{i} ⊢_{F} M_{i} : [ρ⃗_{1}/X⃗_{1}, …, ρ⃗_{i}/X⃗_{i}]σ_{i}. These are therefore the subterms satisfying the same assumptions as M so, by induction:

y_{i}:τ_{i} ⊢_{co} M_{i} : [ρ⃗_{1}/X⃗_{1}, …, ρ⃗_{i}/X⃗_{i}]σ_{i}  (1)

In other words, each subterm M_{i}, 1 ≤ i ≤ n, is a coercion.

To show that M is a coercion requires two further facts derivable from the assumptions and the structure of M:

M ≡ λY⃗_{1} . λy_{1} :τ_{1} …. λY⃗_{n} . λy_{n}:τ_{n} . λY⃗_{n+1} . xρ⃗_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1}

First, since M is well-typed in F by the assumption x : σ ⊢_{F} M : τ, then for 1 ≤ i ≤ n + 1, each Y⃗_{i} is not free in the type of preceding bound term variables y_{1}, …, y_{i−1} nor in the type of x. In other words,

Y⃗_{i} not free in σ nor in τ_{1}, …, τ_{i−1}, for 1 ≤ i ≤ n + 1  (2)

Second, given the structure of M, then the type τ of M must have the following form:

τ = ∀Y⃗_{1}.(τ_{1} → … ∀Y⃗_{n}.(τ_{n} → ∀Y⃗_{n+1}.τ′) …)

where τ′ is the type of the body of M, i.e., the type of xρ⃗_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1}. However, since σ is the type of x, the body of M has the type:

[ρ⃗_{1}/X⃗_{1}, …, ρ⃗_{n+1}/X⃗_{n+1}]σ′

Since a well-typed term has a unique type in F, we thus obtain the following:

τ′ = [ρ⃗_{1}/X⃗_{1}, …, ρ⃗_{n+1}/X⃗_{n+1}]σ′  (3)

We now construct a Co^{⊢} derivation showing that x : σ ⊢_{co} M : τ. To improve readability of complex derivations, we will denote by δ_{i} the substitution

[ρ⃗_{1}/X⃗_{1}, …, ρ⃗_{i}/X⃗_{i}]

Thus, (1) becomes y_{i}:τ_{i} ⊢_{co} M_{i} : δ_{i}σ_{i} and (3) becomes τ′ = δ_{n+1}σ′.

Basically, the leaves of the derivation are the sequents (1) plus an axiom that uses (3). Rules (→) and (∀ left) are then applied alternately to introduce σ on the left and the underlying → structure of τ on the right. Finally, (∀ right) is used repeatedly to introduce ∀Y⃗_{i} on the right. Note that the non-freeness side-conditions for these applications of (∀ right) are satisfied by (2).

(ax) by (3)

\underline{z:δ_{n+1}σ′ ⊢_{co} z:τ′} (∀ left)

(1) \begin{matrix}y_{n}:τ_{n} \\ ⊢_{co} M_{n} : δ_{n}σ_{n} \end{matrix} \begin{matrix}x_{n+1} :δ_{n}(∀X⃗_{n+1}.σ′) \\ ⊢_{co} x_{n+1}ρ⃗_{n+1} : τ′ \end{matrix}

(→)

\underline{\begin{matrix}z_{n}:δ_{n}(σ_{n} → ∀X⃗_{n+1}.σ′) \\ ⊢_{co} λy_{n}:τ_{n} . z_{n}M_{n}ρ⃗_{n+1} : τ_{n} → τ′ \end{matrix}}  (∀ left)
(1) \begin{matrix}y_{n−1} :τ_{n−1} \\ ⊢_{co} M_{n−1} : δ_{n−1}σ_{n−1} \end{matrix}  \begin{matrix}x_{n}:δ_{n−1}(∀X⃗_{n}.(σ_{n} → ∀X⃗_{n+1}.σ′)) \\ ⊢_{co} λy_{n}:τ_{n} . x_{n}ρ⃗_{n}M_{n}ρ⃗_{n+1} : τ_{n} → τ′ \end{matrix}
\overline{⋮}  (→)
⋮  ⋮
⋮  (∀ left)
\overline{\begin{matrix}z_{1} :δ_{1}(σ_{1} → … ∀X⃗_{n}.(σ_{n} → ∀X⃗_{n+1}.σ′) …) \\ ⊢_{co} λy_{1} :τ_{1} … λy_{n}:τ_{n} . z_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1} : τ_{1} → … τ_{n} → τ′ \end{matrix}} (→)

\overline{\begin{matrix}x:∀X⃗_{1}.(σ_{1} → … ∀X⃗_{n}.(σ_{n} → ∀X⃗_{n+1}.σ′) …) \\ ⊢_{co} λy_{1} :τ_{1} … λy_{n}:τ_{n} . xρ⃗_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1} : τ_{1} → … τ_{n} → τ′ \end{matrix}} (∀ left)

\overline{x:σ ⊢_{co} \begin{matrix}λy_{1} :τ_{1} … λy_{n}:τ_{n}λY⃗_{n+1} . xρ⃗_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1} \\ : τ_{1} → … τ_{n} → ∀Y⃗_{n+1}.τ′ \end{matrix}}  (∀_{n+1} right) due to (2)

\overline{⋮}  (∀_{n} right) due to (2)
⋮  ⋮
\overline{x:σ ⊢_{co} \begin{matrix}λY⃗_{1} . λy_{1} :τ_{1} … λY⃗_{n} . λy_{n}:τ_{n} . λY⃗_{n+1} . xρ⃗_{1}M_{1} … ρ⃗_{n}M_{n}ρ⃗_{n+1} \\ : ∀Y⃗_{1}.(τ_{1} → … ∀Y⃗_{n}.(τ_{n} → ∀Y⃗_{n+1}.τ′) …) \end{matrix}}  (∀_{0} right) due to (2)

Thus, x:σ ⊢_{co} M : τ so M is a coercion.

7.1 Mitchell’s System for Subtyping

In [Mit88], a “retyping function” is defined as a typed term in System F whose erasure η-reduces to the identity. In [Mit88, Lemma 9], it is then shown that σ is a subtype of τ in all “simple inference models” (as defined in [Mit88, section 4.2]) if and only if there is a retyping function from σ to τ. Thus, our Theorems 13 and 14 also give a semantic completeness theorem, in the sense of Mitchell, for Co^{⊢}. We conclude this section with a direct comparison of Co^{⊢} to Mitchell’s axiomatic approach to subtyping, which is given here in a revised (but clearly equivalent) way.

Mitchell’s System for Subtyping

(ax)  σ ≤ σ  (trans)  {σ ≤ τ  τ ≤ ρ \atop σ ≤ ρ}

(→)  {σ′ ≤ σ  τ ≤ τ′ \atop (σ → τ) ≤ (σ′ → τ′)}  (∀ subst) {σ ≤ τ \atop ∀X.σ ≤ ∀X.τ}

(∀ intro)  σ ≤ ∀X.σ  (∀ elim) ∀X.σ ≤ [ρ/X]σ
∗ for X not ; free in σ

(∀→ distr) ∀X.(σ → τ) ≤ (∀X.σ) → (∀X.τ)

It is not hard to show that Co^{⊢} and Mitchell’s system are equivalent.

Theorem 17 σ ≤ τ iff σ ⊢_{co} τ.

Proof: Clearly, rules (ax) and (→) are identical in the two systems (with ⊢_{co} for ≤). For the implication from left to right, the rule (trans) above corresponds to (cut), which, by Theorem 14, is admissible for Co^{⊢}; the other cases in this direction are proven as follows:

Case: (∀ intro) is derivable in Co^{⊢} since X is not free in σ

\frac{σ ⊢_{co} σ}{σ ⊢_{co} ∀X.σ} (∀_{0} right)

Case: (∀ elim) is derivable in Co^{⊢}

\frac{[ρ/X]σ ⊢_{co} [ρ/X]σ}{∀X.σ ⊢_{co} [ρ/X]σ} (∀ left)

Case: (∀ subst) is derivable in Co^{⊢}

\frac{[X/X]σ ⊢_{co} τ}{∀X.σ ⊢_{co} τ} (∀ left)
\overline{∀X.σ ⊢_{co} ∀X.τ} (∀_{0} right)

Case: (∀→ distr) is derivable in Co^{⊢}+(cut)

\underline{∀X.σ ⊢_{co} σ  τ ⊢_{co} τ} (→) ∀X.(σ → τ) ⊢_{co} σ → τ  σ → τ ⊢_{co} (∀X.σ) → τ
\overline{∀X.(σ → τ) ⊢_{co+cut} (∀X.σ) → τ}  (cut)
\overline{∀X.(σ → τ) ⊢_{co+cut} (∀X.σ) → (∀X.τ)}  (∀_{1} right)

Conversely, the remaining cases of the implication from right to left are proven as follows:

Case: (∀ left) is derivable in Mitchell’s system by

∀X.σ ≤ [ρ/X]σ ≤ τ

using (trans) on (∀ elim) and the premise of (∀ left), i.e., [ρ/X]σ ≤ τ.

Case: (∀_{n} right) is derivable in Mitchell’s system as follows:

σ ≤ ∀X.σ  by (∀ intro) and (∀_{n} right) side-condition X not free in σ
≤ ∀X.(τ_{1} → … (τ_{n} → τ) …)  by (∀ subst) on (∀_{n} right) premise
≤ (∀X.τ_{1}) → ∀X.(τ_{2} → … (τ_{n} → τ) …)  by (∀→ distr)
≤ (∀X.τ_{1}) → ((∀X.τ_{2}) → ∀X.(τ_{3} → … (τ_{n} → τ) …)by (∀→ distr) and (→)
⋮  ⋮
≤ (∀X.τ_{1}) → ((∀X.τ_{2}) → … ((∀X.τ_{n}) → (∀X.τ) …)

by (∀→ distr) and (→)

≤ τ_{1} → (∀X.τ_{2}) → … (∀X.τ_{n}) → (∀X.τ) …)

by (→), (∀ intro) and (∀_{n} right) side-condition X not free in τ_{1}

⋮  ⋮
≤ τ_{1} → (τ_{2} → … (τ_{n} → ∀X.τ) …)

by (→), (∀ intro) and (∀_{n} right) side-condition X not free in τ_{n}

8 Adding base types to Co^{⊢}

Consider now extending the language of Co^{⊢} with fresh type constants κ_{1}, κ_{2}, κ_{3}, … For example, these could be base types such as bool, int, real. To assert that a subtyping relation holds between some of these base types, between κ_{i} and κ_{j} say, add a fresh term constant c to the language and add the following Gentzen-style rule formalizing that κ_{i} is a subtype of κ_{j} via coercion c:

(κ_{i} ≤ κ_{j}) {x:σ ⊢ M : κ_{i} \atop x:σ ⊢ c M : κ_{j}}

Let Co^{⊢}+B denote the system Co^{⊢} extended with such base constants and rules, and let ⊢_{co+B} denote entailment in the extended system. What happens then to the subtyping partial order and the coherence and cut-elimination properties of the “pure” calculus Co^{⊢}?

First, observe that the expected subtyping judgment x : κ_{i} ⊢_{co} c x : κ_{j} is easy to derive: just take σ = κ_{i} and M ≡ x in the above rule. Indeed, as we now show, the new constants and rules introduce no new subtyping judgments beyond those expected. In a sense, constant coercions act like variables; they do not compute.

Lemma 18 (Conservativity of Co^{⊢}+B) Assume that types σ and τ do not contain occurrences of base types. If σ ⊢_{co+B} τ then σ ⊢_{co} τ.

Proof: First, let α be a Co^{⊢}+B derivation of a sequent S, where S may contain base types. Observe that by uniformly substituting a fresh variable X for all base types κ_{1}, … κ_{n} in α, we obtain a Co^{⊢} derivation of [X/κ_{1}, …, X/κ_{n}]S. This is easily shown by induction on Co^{⊢}+B derivations. Then, the fact follows as a corollary of this observation, for the case when S does not contain base types.

We now prove some properties of ⊢_{co+B} derivations. For this, we require notions of equality on Co^{⊢}+B derivations, defined similarly to the equalities on Co^{⊢} derivations (see section 5), and for which we will use the same symbols: =, =_{η}, =_{ηco}. As a particular reminder, two derivations are = when the proof terms labelling their end-sequents are syntactically identical.

Lemma 19 A (κ_{i} ≤ κ_{j}) rule cannot be applied at any point after an application of either (∀_{n} right) or (→).

Lemma 20 (Rule permutations III) A (κ_{i} ≤ κ_{j}) rule can be permuted with (∀ left) in both directions:

\begin{matrix}\frac{S_{1}}{S_{2}} & (κ_{i} ≤ κ_{j}) \\ \overline{S_{3}} & (∀ left) \end{matrix}  =  \begin{matrix}\frac{S_{1}}{S′_{2}} & (∀ left) \\ \overline{S_{3}} & (κ_{i} ≤ κ_{j}) \end{matrix}

Proof: Easy. Note that the coercions are identical in the final sequents.

Lemma 21 Assume σ ⊢_{co+B} τ with derivation α.

1. If τ does not contain either “→” or “∀”, then α contains applications of only (ax), (κ_{i} ≤ κ_{j}), and (∀ left).

2. If σ does not contain either “→” or “∀”, then α contains applications of only (ax), (κ_{i} ≤ κ_{j}), and (∀_{0} right).

Proof: By induction on the size of α in both cases. Note that, in both cases, the derivations are linear, not trees.

Theorem 22

1. Let σ ⊢_{co+B} κ. Then, σ = ∀X_{l} … ∀X_{1}.σ′, for some l ≥ 0 and where σ′ is either a base type κ′ or a variable X_{i} for i ∈ 1 … l.

2. Let κ ⊢_{co+B} τ. Then, τ = ∀X_{m} … ∀X_{1}.κ′ for some base type κ′ and some m ≥ 0.

Proof of 1. By Lemma 21 case 1, the derivation of σ ⊢_{co+B} κ consists of applications of only (ax), (κ_{i} ≤ κ_{j}), and (∀ left). The derivation is linear, not a tree. The applications of (κ_{i} ≤ κ_{j}) can be permuted by Lemma 20 with the applications of (∀ left), if any. Furthermore, (ax) must be instantiated with κ′. Thus, an equal derivation of σ ⊢_{co+B} κ may be constructed with the following structure:

κ′ ⊢_{co+B} κ′  (ax)
(∀ left)
⋮ ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ′} (∀ left)
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ_{p}} (κ′ ≤ κ_{p})
\overline{⋮}  ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ_{q}}  ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ} (κ_{q} ≤ κ)

where k ≥ 0 is the number of applications of (κ_{i} ≤ κ_{j}) rules, i.e., (κ′ ≤ κ_{p}), …, (κ_{q} ≤ κ), and l′ ≥ 0 is the number of applications of (∀ left). Note that l ≤ l′.

Proof of 2. By Lemma 21 case 2, the derivation of κ ⊢_{co+B} τ can contain applications of only (ax), (κ_{i} ≤ κ_{j}), and (∀_{0} right). By Lemma 19, all the applications of the (κ_{i} ≤ κ_{j}) rules must appear before those of (∀_{0} right). Furthermore, (ax) must be instantiated with the base type κ. Hence, the derivation has the following structure:

κ ⊢_{co+B} κ  (ax)
\overline{κ ⊢_{co+B} κ_{p}}  (κ ≤ κ_{p})
⋮
⋮  ⋮ \overline{κ ⊢_{co+B} κ_{q}}  ⋮
\overline{κ ⊢_{co+B} κ′}  (κ_{q} ≤ κ′)
\overline{κ ⊢_{co+B} ∀X_{1}.κ′}  (∀_{0} right)
⋮
⋮ ⋮
\overline{κ ⊢_{co+B} ∀X_{m} … ∀X_{1}.κ′} (∀_{0} right)

where k ≥ 0 is the number of applications of (κ_{i} ≤ κ_{j}) rules, i.e., (κ ≤ κ_{p}), …, (κ_{q} ≤ κ′), and m ≥ 0 is the number of applications of (∀_{0} right).

Corollary 1. Let x:σ ⊢_{co+B} M:κ. Then, M ≡ c_{k}(… c_{1}(xρ_{l′} … ρ_{1}) …)

2. Let x:κ ⊢_{co+B} M:τ. Then, M ≡ λX_{m} … λX_{1} . c_{k}(… c_{1}x) …)

Theorem 22 shows that adding extra base types and base coercions changes the subtyping partial order in a reasonable way: each base type has only itself, the empty type, or other base types, given by the extra subtyping rules, as subtypes of it (up to bi-coercibility, of course). Indeed, for case 1 of Theorem 22, σ ≅ ; b κ′ or σ ≅ ; b ∀X.X, while for case 2, τ ≅ ; b κ′.

8.1 Admissibility of Cut for Co^{⊢}+B

Let Co^{⊢}+B + (cut) denote Co^{⊢}+B extended with (cut). Following the paradigm used for the pure system Co^{⊢}, we will show that (cut) is admissible for the extended system Co^{⊢}+B by proving cut-elimination for Co^{⊢}+B + (cut).

Lemma 23 (Rule permutations IV) A (κ_{i} ≤ κ_{j}) rule can be permuted on the right with (cut). That is, the following derivation:

\begin{matrix}\underline{y:τ ⊢_{co+B} N : κ_{i}} & (κ_{i} ≤ κ_{j}) \\ x:σ ⊢_{co+B} M : τ & y:τ ⊢_{co+B} c N : κ_{j} \\ \overline{x:σ ⊢_{co+B} P : κ_{j}} & (cut) \end{matrix}

where P is the β-nf of [M/y](c N), is = to:

\begin{matrix}\frac{x:σ ⊢_{co+B} M : τ y:τ ⊢_{co+B} N : κ_{i}}{x:σ ⊢_{co+B} Q : κ_{i}} & (cut) \\ \overline{x:σ ⊢_{co+B} c Q : κ_{j}} & (κ_{i} ≤ κ_{j}) \end{matrix}

where Q is the β-nf of [M/y]N.

Proof: Easy. Observe that P ≡ c Q.

Theorem 24 (Cut-elimination for Co^{⊢}+B + (cut)) Every derivation in Co^{⊢}+B + (cut) is = to a derivation in Co^{⊢}+B.

Proof: By induction on the size of cut-free derivations (i.e., Co^{⊢}+B derivations). The proof is identical to the proof of Theorem 14 but with two extra cases. Consider thus the first application of (cut) in a derivation:

\frac{S_{L} S_{R}}{S} (cut)

where the derivations of S_{L} and S_{R} are cut-free. The two extra cases to consider are as follows:

\underline{Case:} S_{R} derived by a (κ_{i} ≤ κ_{j}) rule. Apply Lemma 23 to permute (κ_{i} ≤ κ_{j}) on the right with (cut) so that the (cut) moves upwards. Then, by induction, there exists an equal cut-free derivation, replacing the one with (cut).

\underline{Case:} S_{L} derived by a (κ_{i} ≤ κ_{j}) rule. The derivation looks like:

\frac{⋮}{σ ⊢_{co+B} κ_{q}}

(κ_{q} ≤ κ) \overline{σ ⊢_{co+B} κ}  \frac{⋮}{κ ⊢_{co+B} τ}
(cut)  \overline{σ ⊢_{co+B} τ}

Apply Theorem 22, case 1 to S_{L} ≡ σ ⊢_{co+B} κ, and case 2 to S_{R} ≡ κ ⊢_{co+B} τ. This yields the following equal derivation, still with (cut).

(ax)  κ′ ⊢_{co+B} κ′

(∀ left)

⋮ ⋮
(∀ left) \overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ′}
(κ′ ≤ κ_{p}) \overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ_{p}}
⋮  \overline{⋮}
⋮  \overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ_{q}}
(κ_{q} ≤ κ) \overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ}

κ ⊢_{co+B} κ  (ax)
\overline{κ ⊢_{co+B} κ_{p′}}  (κ ≤ κ_{p′})
⋮
⋮  ⋮ \overline{κ ⊢_{co+B} κ_{q′}}  ⋮
\overline{κ ⊢_{co+B} κ′′}  (κ_{q′} ≤ κ′′)
\overline{κ ⊢_{co+B} ∀X_{1}.κ′′}  (∀_{0} right)
⋮
⋮ ⋮
\overline{κ ⊢_{co+B} ∀X_{m} … ∀X_{1}.κ′′} (∀_{0} right)
(cut)  \overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} ∀X_{m} … ∀X_{1}.κ′′}

Thus, τ = ∀X_{m} … ∀X_{1}.κ′′ for m the number of applications of (∀_{0} right), and σ = ∀X_{l} … ∀X_{1}.σ′ where σ′ is either the base type κ′ or a variable X_{i} for i ∈ 1 … l, with l ≤ l′ for l′ the number of applications of (∀ left). Obtain now the following equal cut-free derivation by applying the rules in the derivation of S_{R} immediately after those of S_{L}:

κ′ ⊢_{co+B} κ′  (ax)
(∀ left)
⋮ ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ′}  (∀ left)
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ_{p}}  (κ′ ≤ κ_{p})
\overline{⋮}  ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ_{q}}  ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ}  (κ_{q} ≤ κ)
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ_{p′}}  (κ ≤ κ_{p′})
⋮
⋮  ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ_{q′}}  ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ′′}  (κ_{q′} ≤ κ′′)
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} ∀X_{1}.κ′′}  (∀_{0} right)
⋮
⋮ ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} ∀X_{m} … ∀X_{1}.κ′′} (∀_{0} right)

We have thus shown that, in the extended system Co^{⊢}+B, (cut) is admissible. In other words, adding extra base types and coercions preserves the transitivity of entailment, i.e., of subtyping.

Note that, if we had used axioms of the form κ_{i} ⊢_{co+B} κ_{j} to assert subtyping relations between base types instead of Gentzen-style rules (κ_{i} ≤ κ_{j}), it would have been impossible to eliminate cuts. Remark also that, usually, in Gentzen-style systems such as ours, “right” rules are balanced by symmetric “left” rules. In the system Co^{⊢}+B, though, only the rules

(κ_{i} ≤ κ_{j}) {x:σ ⊢_{co+B} M : κ_{i} \atop x:σ ⊢_{co+B} c M : κ_{j}}

are added to assert subtyping between base types. However, from the admissibility of (cut) (Theorem 24), we can deduce the admissibility of the “left” analogue of the (κ_{i} ≤ κ_{j}) rules, although only up to β-convertibility in the labelled system:

(κ_{i} ≤ κ_{j} left) {x:κ_{j} ⊢_{co+B} M : σ \atop y:κ_{i} ⊢_{co+B} P : σ}

∗

for P the β-nf of [c y/x]M

To see this, assume that x:κ_{j} ⊢_{co+B} M : σ has been proved. Construct the following derivation with (cut):

\begin{matrix}(κ_{i} ≤ κ_{j}) & \underline{y:κ_{i} ⊢_{co+B} y : κ_{i}} \\ y:κ_{i} ⊢_{co+B} c y : κ_{j} & x:κ_{j} ⊢_{co+B} M : σ \\ (cut) & \overline{y:κ_{i} ⊢_{co+B} P : σ} \end{matrix}

where P is the β-nf of [c y/x]M. Since (cut) is admissible, we are done.

What happens now to coherence of the system in the presence of base types?

8.2 Coherence of Co^{⊢}+B

Suppose that base types κ_{1}, κ_{2}, κ_{3}, … are given together with some (κ_{i} ≤ κ_{j}) rules, as described previously, but that no other conditions are added; for example, no compositionality, no unicity (coherence), no associativity of these base coercions.

Yet, we know, by Lemma 18 (conservativity), that extending the pure calculus Co^{⊢} with new base types and rules yields no new coercions between “pure” types (i.e., types not containing base types). As regards compositionality, Theorem 24 guarantees that, once embedded in our Gentzen-style system, base coercions compose. Moreover, as pointed out previously, only types bi-coercible to ∀X.X and to the new base types may be freshly related to the base types by subtyping in the extended system Co^{⊢}+B.

Thus, the questions of unicity (coherence) and associativity remain unsettled for the new base types (and their bi-coercible images) in the extended system.

As a weak form of coherence, here is what (eq appl2 co) allows us to prove, without any further conditions or assumptions on base types and rules:

Theorem 25 Assume that both c and d are constant coercions between base types κ_{i} and κ_{j}. If y:σ ⊢_{co+B} M:κ_{i}, then x:∀X.σ ⊢_{co+B} c ([xX/y]M) =_{ηco} d ([xX/y]M) : κ_{j}

Proof: The assumption means that the following two rules have been added:

{x:σ ⊢_{co+B} M : κ_{i} \atop x:σ ⊢_{co+B} c M : κ_{j}}  {x:σ ⊢_{co+B} M : κ_{i} \atop x:σ ⊢_{co+B} d M : κ_{j}}

Construct then the following derivation:

\frac{y:σ ⊢_{co+B} M : κ_{i}}{y:σ ⊢_{co+B} c M : κ_{j}}  \frac{y:σ ⊢_{co+B} M : κ_{i}}{y:σ ⊢_{co+B} d M : κ_{j}}
\overline{x:∀X.σ ⊢_{co+B} c ([xX/y]M) =_{ηco} d ([xX/y]M) : κ_{j}} (eq appl2 co)

In particular, since x:∀X.κ_{i} ⊢_{co+B} xX:κ_{i}, Theorem 25 implies equality of the composition of c and d with the coercion xX: just take σ = κ_{i} and M ≡ y. Clearly though, the Theorem does not imply the equality of c and d.

In order to prove full coherence for Co^{⊢}+B, we need to force unicity of coercions (coherence) on base types. This may be done by adding a rule for equality on base types as follows.

Definition =_{ηcoB} is the least equivalence relation generated by =_{ηco} plus the following rule:

(eq base co) {x:κ_{i} ⊢_{co+B} c_{i}(… (c_{1}x) …) : κ_{j}  x:κ_{i} ⊢_{co+B} c′_{j}(… (c′_{1}x) …) : κ_{j} \atop x:κ_{i} ⊢_{co+B} c_{i}(… (c_{1}x) …) =_{ηcoB} c′_{j}(… (c′_{1}x) …) : κ_{j}}

Note that, by the corollary to Theorem 22, the terms c_{i}(… (c_{1}x) …) and c′_{j}(… (c′_{1}x) …) are the only ones possible.

Theorem 26 (Coherence of Co^{⊢}+B derivations) Let α_{1} and α_{2} be two derivations of x:σ ⊢_{co+B} M:τ and x:σ ⊢_{co+B} N:τ respectively. Then, M =_{ηcoB} N.

Proof: The proof is similar to the proof of coherence for the pure system Co^{⊢} (Theorem 13) but with an extra case. Assume that one of α_{1}, α_{2} ends with a (κ_{i} ≤ κ_{j}) rule. Then, τ = κ for some base type κ. By Lemma 21 case 1, both α_{1} and α_{2} may contain applications of only (ax), (κ_{i} ≤ κ_{j}), and (∀ left) rules. Apply Lemma 20 to both derivations, permuting all applications of (κ_{i} ≤ κ_{j}) rules before those of (∀ left), thus obtaining the following two derivations:

κ′ ⊢_{co+B} κ′  (ax)
\overline{κ′ ⊢_{co+B} κ_{p}}  (κ′ ≤ κ_{p})
\overline{⋮}  ⋮ \overline{κ′ ⊢_{co+B} κ_{q}}  ⋮
\overline{x:κ′ ⊢_{co+B} M : κ} (κ_{q} ≤ κ)
(∀ left)
⋮ ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ} (∀ left)

κ′ ⊢_{co+B} κ′  (ax)
\overline{κ′ ⊢_{co+B} κ_{p′}}  (κ′ ≤ κ_{p′})
\overline{⋮}  ⋮ \overline{κ′ ⊢_{co+B} κ_{q′}}  ⋮
\overline{x:κ′ ⊢_{co+B} N : κ} (κ_{q′} ≤ κ)
(∀ left)
⋮ ⋮
\overline{∀X_{l} … ∀X_{1}.σ′ ⊢_{co+B} κ} (∀ left)

Note that the applications of (∀ left) are the same in both derivations, but the applications of (κ_{i} ≤ κ_{j}) rules, and their number, may differ. Ignore now the applications of (∀ left) and consider the (sub)derivations of x : κ′ ⊢_{co+B} M : κ and x: κ′ ⊢_{co+B} N : κ in each derivation. By simple application of the equality rule (eq base co) above, obtain x: κ′ ⊢_{co+B} M =_{ηcoB} N : κ. Then, since (∀ left) preserves equality of coercions (implied by (eq appl2 co); see remark section 3.3), we are done.

Corollary Each (κ_{i} ≤ κ_{j}) rule preserves equality of coercions. Proof: Assume that a rule (κ ≤ κ′) has been added to the system, and assume that the equality x:σ ⊢_{co+B} M =_{ηcoB} N : κ has been derived. The equality implies that x:σ ⊢_{co+B} M : κ and x:σ ⊢_{co+B} N : κ. By application of the rule (κ ≤ κ′), we obtain both x:σ ⊢_{co+B} c M : κ′ and x:σ ⊢_{co+B} c N : κ′ where c is the base coercion given by the rule. Use now the same proof technique as in Theorem 26 to derive x:σ ⊢_{co+B} c M =_{ηcoB} c N : κ′.

Coherence guarantees unicity of coercions on all types. As in the pure system Co^{⊢}, it implies that bi-coercible types are isomorphic. And, as in Co^{⊢}, coherence implies the associativity of coercion composition, as given by cut-elimination.

9 Conclusions

The purpose of the calculus Co^{⊢} presented in this paper is to give a coherent logical meaning to the notion of subtyping. The main advantage of our approach is that Co^{⊢} has a sound logical “status”, independently of its intended meaning for subtyping. This allowed us to (state and) prove relevant properties such as coherence and the admissibility of (cut), which is equivalent to a cut-elimination theorem. And, since Gentzen, cut-elimination theorems are at the core of (constructive) Proof Theory.

It should be clear why we do not take the (cut) rule as part of the definition of our “Logic of Subtyping”, in spite of it being as fundamental as transitivity and it being required to prove completeness. In order to obtain coherence, we would need to eliminate it, anyway. And coherence is used to prove anti-symmetry. Moreover, without (cut), all our proof-terms (definable coercions) are in normal form, as only (cut) introduces redexes, exactly as in the lambda-calculus.

In view of its formal relation to (cut), it may be fair to say that this “Logic for Subtyping” is the least meaningful system for implication that also handles second order universal quantification. Indeed, what weaker but still meaningful computation is there than “take an input and transform it into an element of a larger type”? And, intuitionistically, logical implications are computations. By our system, we characterized the logical implications which are coercions and explicitly used this characterization in the main results.

Acknowledgments

We would like to thank Jerzy Tiuryn for his close analysis and critical insight into our work.

Sergei Soloviev’s work was carried out while employed at BRICS, the Danish National Research Council’s center for computer science (Århus, Denmark), and was funded by two European Community Human Capital and Mobility grants “Typed Lambda Calculus” (while visiting ENS, Paris) and “CLICS II”.

Appendix

The following rules complete the definition of =_{ηco} (Definition 3.3); they just say that rules (→) and (∀_{n} right) preserve equality of coercions:

(eq →)  {x′:σ′ ⊢_{co} M =_{ηco} M′ : σ  y:τ ⊢_{co} N =_{ηco} N′ : τ′ \atop x:σ → τ ⊢_{co} λx′:σ′ . [xM/y]N =_{ηco} λx′:σ′ . [xM′/y]N′ : σ′ → τ′}

(eq ∀_{0≤k≤n} right)  {x:σ ⊢_{co} \begin{matrix}λx_{1} :τ_{1} … λx_{k}:τ_{k}.M =_{ηco} λx_{1} :τ_{1} … λx_{k}:τ_{k}.N \\ : τ_{1} → … (τ_{n} → τ) …) \end{matrix} \atop x:σ ⊢_{co} \begin{matrix}λx_{1} :τ_{1} … λx_{k}:τ_{k} … λx_{n}:τ_{n}.λX.Mx_{k+1} … x_{n} \\ =_{ηco} λx_{1} :τ_{1} … λx_{k}:τ_{k} … λx_{n}:τ_{n}.λX.Nx_{k+1} … x_{n} \\ : τ_{1} → … (τ_{n} → ∀X.τ) …) \end{matrix}} ∗ for X not free in σ

nor in τ_{1}, …, τ_{n}, for M not of the form λy.M′, for x_{k+1}, …, x_{n} fresh

(eq ∀_{0≤n<k} right)  {x:σ ⊢_{co} \begin{matrix}λx_{1} :τ_{1} … λx_{k}:τ_{k}.M =_{ηco} λx_{1} :τ_{1} … λx_{k}:τ_{k}.N \\ : τ_{1} → … (τ_{n} → τ) …) \end{matrix} \atop x:σ ⊢_{co} \begin{matrix}λx_{1} :τ_{1} … λx_{n}:τ_{n}.λX.λx_{n+1} :τ_{n+1} … λx_{k}:τ_{k}.M \\ =_{ηco} λx_{1} :τ_{1} … λx_{n}:τ_{n}λX.λx_{n+1} :τ_{n+1} … λx_{k}:τ_{k}.N \\ : τ_{1} → … (τ_{n} → ∀X.τ) …) \end{matrix}} ∗ for X not free in σ

nor in τ_{1}, …, τ_{n}, for M not of the form λy.M′ for τ ≡ τ_{n+1} → … (τ_{k} → τ′) …)

References

[ACC93] M. Abadi, L. Cardelli and P.-L. Curien. Formal parametric polymorphism. Theoretical Computer Science 121, pages 9–58, 1993.

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

[BDL92] K. Bruce, R. Di Cosmo, and G. Longo. Provable isomorphisms of types. Mathematical Structures in Computer Science 2:2, pages 231–247, 1992.

[BL90] K. Bruce and G. Longo. A modest model of records, inheritance, and bounded quantification. Information and Computation 87, pages 196–240, 1990.

[CG92] P.-L. Curien and Giorgio Ghelli. Coherence of subsumption, minimum typing and type-checking in F_{≤}. Mathematical Structures in Computer Science 2, pages 55–92, 1992.

[CL91] L. Cardelli and G. Longo. A semantic basis for Quest. Journal of Functional Programming 1, pages 417–458, 1991.

[CMMS91] L. Cardelli, S. Martini, J.C. Mitchell, and A. Scedrov. An extension of system F with subtyping. Information and Computation 94, pages 4–56, 1994. First appeared in the proceedings of the Conference on Theoretical Aspects of Computer Software (Sendai, Japan), T. Ito and R. Meyer, eds., Lecture Notes in Computer Science 526, pages 750–770, Springer-Verlag, 1991.

[CW85] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. ACM Computing Surveys 17:4, pages 471–522, 1985.

[Gir71] J.-Y. Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. Proceedings of the 2nd Scandinavian Logic Symposium, J.E. Fenstad, ed., pages 63–92, North-Holland, 1971.

[GLT89] J.-Y. Girard, Y. Lafont and P. Taylor. Proofs and types. Cambridge Tracts in Theoretical Computer Science 7, Cambridge University Press, 1989.

[Hyl82] J.M.E. Hyland. The effective topos. Proceedings of The L.E.J. Brouwer Centenary Symposium, A.S. Troelstra and D.S. van Dalen, eds., pages 165–216, North-Holland, 1982.

[Hyl88] J.M.E. Hyland. A small complete category. Annals of Pure and Applied Logic 40, pages 135–165, 1988.

[Jac95] B. Jacobs. Subtyping and bounded quantification from a fibred perspective. Proceedings of the Conference on Mathematical Foundations of Programming Semantics (New Orleans, U.S.A), 1995.

[Kle67] S.C. Kleene. Mathematical logic, Wiley, 1967.

[LM91] G. Longo and E. Moggi. Constructive natural deduction and its ω-set interpretation. Mathematical Structures in Computer Science 1:2, pages 215–253, 1991.

[LMS93] G. Longo, K. Milsted, and S. Soloviev. The genericity theorem and the notion of parametricity in the polymorphic λ-calculus. Theoretical Computer Science 121, pages 323–349, 1993.

[MR92] Q. Ma and J.C. Reynolds. Types, abstraction, and parametric polymorphism, part 2. Proceedings of the Conference on Mathematical Foundations of Programming Semantics, S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt, eds., Lecture Notes in Computer Science 598, pages 1–40, Springer-Verlag, 1992.

[Mit88] J.C. Mitchell. Polymorphic type inference and containment. Information and Computation 76:2-3, pages 211–249, 1988. Also appeared in Logical Foundations of Functional Programming, G. Huet, ed., pages 153–193, Addison-Wesley, 1990.

[PS94] B. Pierce and M. Steffen. Higher-Order Subtyping. To appear in: Theoretical Computer Science, 1996. A preliminary version appeared in the proceedings of the IFIP Working Conference on Programming Concepts, Methods and Calculi (PRO-COMET), June 1994, and as University of Edinburgh technical report ECS-LFCS-94-280 and Universität Erlangen-Nürnberg Interner Bericht IMMD7-01/94, January 1994.

[Sol83] S. Soloviev. The category of finite sets and Cartesian Closed Categories. Journal of Soviet Mathematics 22:3, pages 1387–1400, 1983.

[Tiu95] J. Tiuryn. Equational axiomatization of bicoercibility for polymorphic types. Proceedings of the 15th Conference on the Foundations of Software Technology and Theoretical Computer Science, P.S. Thiagarajan, ed., Lecture Notes in Computer Science 1026, pages 166–179, Springer-Verlag, 1995.

[Tiu96] J. Tiuryn. A sequent calculus for subtyping polymorphic types. To appear in the proceedings of the Conference on Mathematical Foundations of Computer Science, Springer-Verlag, 1996.

[TU96] J. Tiuryn and P. Urzyczyn. The subtyping problem for second-order types is undecidable. To appear in the proceedings of the 11th IEEE Symposium on Logic in Computer Science (LICS), 1996.