The Genericity Theorem and the Notion of Parametricity in the Polymorphic

λ-calculus

Giuseppe LONGO  Kathleen MILSTED^{∗}

Sergei SOLOVIEV^{∗∗}

Laboratoire d’Informatique, URA 1327 du CNRS Département de Mathématiques et d’Informatique

Ecole Normale Supérieure ∗Digital Equipment Corporation, Paris

∗∗Russian Academy of Sciences, St. Petersburg

LIENS - 92 - 25

December 1992

The Genericity Theorem and the Notion of Parametricity in the Polymorphic λ-calculus

Giuseppe Longo^{1}  Kathleen Milsted^{2}  Sergei Soloviev^{3}

December 1992

Abstract

This paper focuses on how terms of second order λ-calculus, which may take types as inputs, depend on types. These terms are generally understood to have an “essentially” constant meaning, in all models, on input types. We show how the proof theory of second order λ-calculus suggests a clear syntactic description of this phenomenon. Namely, under a reasonable condition, we show that identity of two polymorphic functions on a single type implies identity of the functions (equivalently, every type is a generic input).

1 Introduction

The use of types as explicit parameters, or variable types, is at the core of polymorphic (functional) languages and was introduced, in Logic, by Girard [Gir71] and, in Computer Science, by Reynolds [Rey74]. The idea is that one may define formal functions that “explicitly depend” on input types. In λ-calculus notation, where capital X, Y, ... stand for type variables, one is allowed to consider terms such as λX.M which may be fed a type as input and give a term as output (in the logical jargon, λX.M is a second order term in impredicative Type Theory).

Since early remarks of Strachey [Str67], a distinction was introduced on how these explicitly polymorphic functions had to behave. Indeed, in computing, programs may depend on types: overloaded functions, for example, may call different code according to the input type (or to the type of the input): + uses different code according to whether the addition is performed on (the type of) reals or integers, say. This sort of dependency of terms on types, known as “ad hoc” polymorphism, is an expressive feature of some programming languages, in particular when handled at run-time, and may suggest interesting and general formal systems (see [CGL92], say).

1LIENS(CNRS)-DMI, Ecole Normale Supérieure, 45 rue d’Ulm, 75005 Paris, France.

longo@dmi.ens.fr

2Digital Equipment Corporation, Paris Research Laboratory (PRL), 85 avenue Victor Hugo, 92563 Rueil-Malmaison, France. milsted@prl.dec.com

3Currently at: Computer Science Department, Aarhus University, Ny Munkegade, Bd. 540, DK 8000, Aarhus C, Denmark. soloviev@daimi.aau.dk

Following Strachey (and Reynolds) then, “proper” polymorphism, as opposed to the “ad hoc” variety, was understood as a property of second order terms to define functions that have a “uniform” dependency on input types, or whose output terms do not “essentially” depend on input types. Note, though, that the output terms of, say, λX.M applied to types σ and τ, i.e., (λX.M)σ and (λX.M)τ, need not live in the same type. The point then is to understand how core systems, such as Girard-Reynolds system F [Gir71, Rey74] (also known as second order λ-calculus), satisfy this uniformity property or essential independence from input types and compare terms possibly living in different types; more generally, to understand the functional behavior of formal functions such as λX.M.

A semantic criterion for parametricity was proposed by Reynolds [Rey83, MR91] as an invariance property under relations between type values. In short, if a relation is given on type parameters σ and τ, then (the interpretation of) λX.M, applied to (the meaning of) σ and τ, should send related elements of σ and τ to related elements in the types of the outputs.

Another meaning of the proper polymorphism of system F was given by Bainbridge et al. [BFSS90]. Consider λx: X.N. Is it the case that λx: X.N depends “naturally” on X, in the sense of natural transformations of Category Theory? Indeed, natural transformations provide the core way to express uniformity on objects (as interpretation of types) in categories. Unfortunately, natural transformations act on functors and, in general categories, variable types are not functors. The counterexample is straightforward: the map from X to X → X (the arrow type) should be at once a covariant and contravariant functor. A partial solution, in the context of the typed λ-calculus, may be given by considering categories where maps are only retractions (as in [Sco72, SP82, Gir86]) or isomorphisms (as in [DL89]). This is fine for specific purposes, as in those papers, but does not describe the situation in the full generality of a model theoretic approach. On the other hand, this issue of contra/covariant functors was partly at the origin of relevant generalizations of the notion of functor in mathematics, for example [EK66]; see also [Mac71]. In this line of work, Bainbridge et al. propose to interpret terms as “dinatural” transformations, yet another elegant categorical notion derived from tensor algebra and algebraic topology. The rub is that, in general, dinatural transformations do not compose, while terms do; however, the interpretation works fine (i.e., it is compositional) on relevant models (see [BFSS90, FGSS88, GSS]). On essentially similar lines, Freyd suggested the novel notion of “structor” in order to understand, categorically, the notion of uniformity inherent in second order λ-terms.

These attempts suggested brand new constructions and relevant mathematics, but seem still insufficient to fill the essential gap between the so-called parametricity or uniformity of second order λ-calculus and the core uniformity with respect to objects (and functors) as expressed by natural transformations in Category Theory. This is probably one of the few mismatches (together with subtyping versus subobjects) out of many deep connections between types and objects, terms and morphisms, as summarized, say, in [AL91] and [LS86].

We propose in this work a simple “syntactic” understanding of the so-called parametricity property, or “uniform dependency” on input types, of polymorphic calculi. First, we present an extension of system F, suggested by a simple result of Girard. In [Gir71], given a type σ and a term J_{σ} such that, for any type τ, J_{σ}τ reduces to 1 if σ = τ, and reduces to 0 if σ ≠ τ, then F + J_{σ} does not normalize. Since system F normalizes, J_{σ} is not definable in F. The point here is that the polymorphic term J_{σ} gives essentially different output terms living in the same type, according to the (values of the) input types. Then, the starting point for our understanding of parametricity is that a polymorphic term that gives outputs in the same type for all input types, must be constant. This is expressed by the following axiom:

(Axiom C) Mτ = Mτ′ for Γ ⊢ M : ∀X.σ and X ∉ F V (σ)

That is, if the outputs of a polymorphic term M, applied to any type, all live in the same type σ, then these outputs are simply equal. Axiom C is not provable in F, but it is compatible with F, i.e., F may be consistently extended with it. Indeed, a generalization of Axiom C appears in the system F_{<:} [CMMS91] which extends system F with subtyping; see rule Eq appl2. Moreover, in section 10, we point out that both the PER models in realizability topoi and Girard’s models over dI-domains and stable maps satisfy Axiom C. A categorical characterization of models realizing Axiom C will also be outlined. In our view, this obvious remark, the compatibility of Axiom C with system F, is one thing to be noted in order to understand parametricity. From ongoing work [ACC92], it also turns out that Axiom C is realized by all models that satisfy Reynolds’s parametricity condition [MR91].

Consider now Fc, the extension of system F with Axiom C. What we propose for a syntactic understanding of parametricity is the following theorem:

(Genericity Theorem)

Assume M and N live in the same type ∀X.σ If Mτ =_{F c} Nτ for some type τ, then M =_{F c} N

The reader should notice where intended parentheses and existential quantification are located, and also, that there is no restriction on σ. The Genericity Theorem says that, in Fc, if two second order terms coincide on one type, they coincide everywhere. Or, equivalently, that each single type acts as a “generic” input, as a variable.

As second order terms are functions from types to terms, the following intuitive geometric description of our understanding of parametricity may further help the reader:

[figure: types; terms; ⇒; types; terms]

This illustrates that if two polymorphic functions coincide on an input type, then they are, in fact, the same function. In a sense, there are “very few” polymorphic functions.

Of course, more things must be settled, due to the fact that the Genericity Theorem is stated in Fc, not in F. However, Axiom C is a very natural request, directly derived from the old and simple result J_{σ}τ in [Gir71]. Its relevance is also confirmed by the use made of it in [CMMS91]. We will discuss the model theoretic problems raised by the Genericity Theorem in section 10. The next sections recall system F, introduce system Fc, and prove the Genericity Theorem.

2 System F

The language of system F consists of types and terms. A type is either a type variable, a function type, or a polymorphic type, while a term is either a variable, an abstraction, an application, a type abstraction, or a type application. Types and terms have the following syntax:

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

We will use σ, τ, ρ, μ, ν for types and M, N for terms, while for variables, we will use X, Y, Z for type variables and x, y, z for term variables. Following the usual conventions for minimizing parentheses, applications associate to the left, → associates to the right, and the scope of ∀ and λ extends as far to the right as possible. For any type or term P, the set of its free (type and term) variables is defined as usual, and written F V (P). Capture-avoiding substitution of a free (type or term) variable is also defined as usual, and written [τ/X]P or [M/x]P.

Assignment of types to terms takes place relative to a set of variable declarations, where each declaration assigns a unique type to a term variable. In general, we will use Γ to denote a set of declarations, and we write Γ, x : σ to extend Γ with a new declaration x : σ, where x must not occur in Γ. A type assignment is a meta-expression of the form Γ ⊢ M : σ, which asserts that term M has, or lives in, type σ, relative to the declarations in Γ. The following rules define valid type assignments.

Type Assignment Rules

(declaration)  Γ, x:σ ⊢ x : σ

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

∗(∀-intro)  \frac{Γ ⊢ M : σ}{Γ ⊢ λX.M : ∀X.σ}  (∀-elim)  \frac{Γ ⊢ M : ∀X.σ}{Γ ⊢ Mτ : [τ/X]σ}

∗

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

Note the restriction on the ∀-intro rule: without it, it would be possible to prove inconsistencies such as x:Y ⊢ x : Z. This restriction will show up frequently later.

Equal terms are defined by the following schemes and rules:

Equational Schemes and Rules

(β_{1}) (λx:σ.M)N = [N/x]M  (β_{2}) (λX.M)τ = [τ/X]M
(η_{1}) λx:σ.Mx = M for x ∉ F V (M)  (η_{2}) λX.MX = M for X ∉ F V (M)

(ξ_{1}) \frac{M = N}{λx:σ.M = λx:σ.N}  (ξ_{2}) \frac{M = N}{λX.M = λX.N}

(app_{1}) \frac{M_{1} = M_{2} N_{1} = N_{2}}{M_{1}N_{1} = M_{2}N_{2}}  (app_{2}) \frac{M = N}{Mτ = Nτ}

(refl) M = M  (sym) \frac{M_{1} = M_{2}}{M_{2} = M_{1}}  (trans) \frac{M_{1} = M_{2} M_{2} = M_{3}}{M_{1} = M_{3}}

We will use the symbol ≡ for syntactic identity. For types, σ = τ is the same as σ ≡ τ while, for terms, M ≡ N implies M = N but not vice-versa.

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}) & λx:σ.Mx ⟶_{η_{1}} M for x ∉ F V (M) & (η_{2}) & λX.MX ⟶_{η_{2}} M for X ∉ F V (M) \end{matrix}

We will write ⟶_{F} for the union of these reductions.

The following important properties hold for system F.

Unique Typing A well-typed term lives in a unique type: if Γ ⊢ M : σ and Γ ⊢ M : τ then σ = τ.

Strong Normalization There are no infinite reduction sequences from well-typed terms.

Church-Rosser If M ⟶_{F} M_{1} and M ⟶_{F} M_{2} then there exists an M_{0} such that M_{1} ⟶_{F} M_{0} and M_{2} ⟶_{F} M_{0}.

Equational Church-Rosser If M_{1} = M_{2} then there exists an M_{0} such that M_{1} ⟶_{F} M_{0} and M_{2} ⟶_{F} M_{0}.

3 System Fc

System Fc is formed by adding the following equational scheme to system F:

(Axiom C) Mτ = Mτ′ for Γ ⊢ M : ∀X.σ and X ∉ F V (σ)

If the outputs of polymorphic function M live in a type σ that does not depend on M’s input type, then the outputs are equal, regardless of the input type. Or, equivalently, M is constant.

Axiom C authorizes more equations than in system F. We will write M =_{F} N for F equations, and M =_{F c} N for Fc equations. Clearly, Axiom C is not provable in system F. Take x : ∀X.σ with X ∉ F V (σ) and apply Axiom C to x. This gives

xτ =_{F c} xρ

These two terms would be equated in system F only if τ = ρ.

Since system Fc adds no new terms, types, typing rules, or reductions, it enjoys the same non-equational properties as system F, such as unique typing of terms, strong normalization, and the Church-Rosser property. However, a number of equational properties fail for Fc, in particular, the equational Church-Rosser property: for example, even though xτ =_{F c} xρ above, there is no common term to which both xτ and xρ reduce.

In the proof of the Genericity Theorem, it will generally be more convenient to use a term with a “type substitution structure” such as [τ/X]M instead of a polymorphic application Mτ. Thus, we may use the following formulation of Axiom C:

(Axiom C^{∗}) [τ/X]M = [τ′/X]M  for Γ ⊢ M : σ and X ∉ F V (Γ) ∪ F V (σ)

It is simple to prove that Axiom C and Axiom C^{∗} are equivalent. We give the proof to stress the extra side-condition X ∉ F V (Γ) on Axiom C^{∗} and its relation to the side-condition on ∀-introduction. These conditions will appear frequently in the later proofs. We will write M =_{c} N and M =_{c^{∗}} N if M and N are equal by only applications of Axiom C and Axiom C^{∗} respectively.

Remark: Axiom C^{∗} is equivalent to Axiom C.

\underline{Case:} Axiom C implies Axiom C^{∗}.

Assume that Γ ⊢ M : σ and X ∉ F V (Γ) ∪ F V (σ).

Since X ∉ F V (Γ), then X is not free in the type of any free term variable in M. So, by ∀-intro, Γ ⊢ λX.M : ∀X.σ. Also, X ∉ F V (σ). Thus, by Axiom C and β_{2}, [τ/X]M =_{β_{2}} (λX.M)τ =_{c} (λX.M)τ′ =_{β_{2}} [τ′/X]M.

\underline{Case:} Axiom C^{∗} implies Axiom C.

Assume that Γ ⊢ M : ∀X.σ and X ∉ F V (σ).

Let Z be a fresh type variable. Then, Γ ⊢ MZ : σ, and Z not free in any of Γ, M, σ. Thus, by Axiom C^{∗}, Mτ ≡ [τ/Z](MZ) =_{c^{∗}} [τ′/Z](MZ) ≡ Mτ′.

4 Roadmap to the Proof of Genericity

In this section, we outline the route to the proof of the Genericity Theorem:

Assume M and N live in the same type ∀X.σ If Mτ =_{F c} Nτ for some type τ, then M =_{F c} N

The hard part consists of proving the following Main Lemma, which is a substitution formulation of the Theorem:

Assume M and N live in the same type σ

If [τ/X]M =_{F c} [τ/X]N for some type τ, then M =_{F c} N

The first remark to be made about the proof is that it is not an induction. The point is that corresponding subterms of Fc-equal terms do not need to live in the same type. The following example illustrates this.

Example: Assume x : ∀Y.Y and z : ∀Y_{1}.∀Y_{2}.Y_{1} → Y_{2}.

Let X and Z be fresh type variables.

Then, apply Axiom C^{∗} to zZX(xZ) : X to obtain

zτX(xτ) =_{F c} zρX(xρ)

Note, though, that subterms zτX and zρX live in different types.

However, this example also provides a hint to the proof of the Genericity Theorem. Observe that the Fc-equality zτX(xτ) =_{F c} zρX(xρ) is obtained via the intermediate term zZX(xZ) to which Axiom C^{∗} is applied. Furthermore, zτX(xτ) and zρX(xρ) are both instances of this term, using type substitutions [τ/Z] and [ρ/Z] respectively. Approximately then, the hint is this: given two Fc-equal terms, construct a common term that can be instantiated to the two terms by type substitutions, and to which Axiom C^{∗} can be applied.

The proof thus begins in section 5 by developing the notion of a generalizer for second order terms. This is a novel idea for the polymorphic λ-calculus, although it is, of course, related to generalizers and anti-unifiers of first-order calculi. Given two second order terms that are identified by type substitutions, we construct a common term that can be instantiated, by type substitutions, to the original terms. Similarly, we can construct a common type that can be instantiated, by type substitutions, to two given types. Furthermore, if the two terms live in two different types, then the generalizer of the terms lives in the generalizer of the types. Note that this notion of generalizer uses type substitutions, not term substitutions (as is usual for first-order terms).

The proof proceeds next with a property of C^{∗}-equality that we call Quasi-Genericity: if a term has a type substitution structure, i.e., is of the form [τ/X]M, and Axiom C^{∗} is applied to it, then that exact type substitution structure is preserved, i.e., the result is of the form [τ/X]N, and, moreover, M =_{c^{∗}} N. This is shown in section 6, where we also give a counter-example to show that F-equality does not satisfy this property.

One of the consequences of Quasi-Genericity of C^{∗}-equality is that if the result of applying Axiom C^{∗} to [τ/X]M is already known to be of the form [τ/X]N, then M =_{c^{∗}} N. Observe that this is a weak form of Genericity, in that it uses C^{∗}-equality instead of Fc-equality in the premise of the Genericity Theorem. Another weak form, with F-equality in the premise, can also be proven. Thus, in section 7, we have the following two Weak Genericity Theorems:

Assume M and N live in the same type σ

If [τ/X]M =_{F} [τ/X]N for some type τ, then M =_{F c} N

Assume M and N live in the same type σ

If [τ/X]M =_{c^{∗}} [τ/X]N for some type τ, then M =_{F c} N

Putting these two together to obtain Fc-equality in the premise depends on how C^{∗}- equality interacts with F-equality. Unfortunately, F and C^{∗}-equalities cannot be arbitrarily reordered. In section 8, we show that C^{∗}-equality and forward β_{1}β_{2}η_{1} reduction (but not η_{2} reduction) do indeed commute. In section 9, we draw all the pieces together to prove the main result. This involves examining the chain of Fc-equalities between [τ/X]M =_{F c} [τ/X]N. Using the Church-Rosser property, commutativity of C^{∗}-equality with β_{1}β_{2}η_{1} reduction, and Quasi-Genericity of C^{∗}-equality, we push the [τ/X] substitution structure from [τ/X]M through the chain so that each node in the chain has the form [τ/X]M_{i} for some M_{i} with M =_{F c} M_{i}. Finally, we use Weak Genericity of F and C^{∗}-equality to show that the final node [τ/X]N in the chain ends up with M =_{F c} N. This gives the result.

5 Type and Term Generalizers

In this section, we give a notion of “generalizer” and construct some critical ones for types and terms. In short, a generalizer of two types or terms may be instantiated to those types or terms, under suitable conditions.

For example, given two terms M_{1} and M_{2}, if one has [τ/X]M_{1} ≡ [ρ/Y]M_{2}, then an abstract notion of a generalizer, with respect to a fresh type variable Z, will be a term M_{0} such that, for suitable types μ_{1}, μ_{2}, one has

\begin{matrix}[μ_{1}/Z]M_{0} ≡ M_{1} \\ [μ_{2}/Z]M_{0} ≡ M_{2} \end{matrix}

That is, if two terms are unified as above, then we will construct a common “term schema” which is instantiated, by type substitutions, to both of them. We use generalizers in later sections, where we show that the typing of M_{0} permits Axiom C^{∗} to be applied, thus allowing us to deduce that M_{1} =_{F c} M_{2}.

The generalizers, though, that we construct here require more details, starting with an analysis of mutual occurrences of τ in ρ or ρ in τ.

Definition: in_{k} If there are k ≥ 0 occurrences of type τ in type ρ, we will write τ in_{k} ρ.

Definition: Context Let τ, ρ, ρ′ be types and let X be a type variable. We say that ρ′ is an X-context for τ in ρ if [τ/X] ρ′ = ρ.

If τ in_{k} ρ with k ≥ 0, then, given fresh X, there are 2^{k} different X-contexts for τ in ρ. We will assume given an enumeration of these contexts, which we will write as ρ_{1}^{X}, …, ρ_{h}^{X} where h = 2^{k}. By convention, we take ρ_{1}^{X} to be ρ. For example, if τ = ρ, then there are two X-contexts for τ in ρ, i.e., ρ_{1}^{X} = ρ and ρ_{2}^{X} = X.

Substitution Convention Let P_{1}, P_{2} be either two terms, or two types, or two sets of variable declarations. If [τ/X]P_{1} ≡ [ρ/Y]P_{2} for some types τ and ρ, then we will assume that X and Y are not free in τ and ρ.

Definition: Generalizer Let P_{1}, P_{2} be either two terms, or two types, or two sets of variable declarations, such that [τ/X]P_{1} ≡ [ρ/Y]P_{2} for some types τ and ρ.

• Case: τ in_{k} ρ for k > 0. Let h = 2^{k}. Given fresh type variables Z_{0}, …, Z_{h}, we say that P_{0} is a Z_{0}, …, Z_{h}- generalizer of P_{1} and P_{2} iff X and Y are not free in P_{0} and

\begin{aligned}[ & X & /Z_{0}, & ρ_{1}^{X} & /Z_{1}, & …, & ρ_{h}^{X} & /Z_{h} & ] P_{0} & ≡ & P_{1} \\ [ & τ & /Z_{0}, & Y & /Z_{1}, & …, & Y & /Z_{h} & ] P_{0} & ≡ & P_{2} \end{aligned}

where ρ_{1}^{X}, …, ρ_{h}^{X} are the X-contexts for τ in ρ.

• Case: ρ in_{k} τ for k ≥ 0 and the previous case does not apply. Let h = 2^{k}. Given fresh type variables Z_{0}, …, Z_{h}, we say that P_{0} is a Z_{0}, …, Z_{h}- generalizer of P_{1} and P_{2} iff X and Y are not free in P_{0} and

\begin{aligned}[ & ρ & /Z_{0}, & X & /Z_{1}, & …, & X & /Z_{h} & ] P_{0} & ≡ & P_{1} \\ [ & Y & /Z_{0}, & τ_{1}^{Y} & /Z_{1}, & …, & τ_{h}^{Y} & /Z_{h} & ] P_{0} & ≡ & P_{2} \end{aligned}

where τ_{1}^{Y} , …, τ_{h}^{Y} are the Y -contexts for ρ in τ.

Remark that, if τ = ρ, then the first case of the definition applies, by τ in_{1} ρ, giving

\begin{aligned}[ & X & /Z_{0}, & ρ & /Z_{1}, & X & /Z_{2} & ] P_{0} & ≡ & P_{1} \\ [ & τ & /Z_{0}, & Y & /Z_{1}, & Y & /Z_{2} & ] P_{0} & ≡ & P_{2} \end{aligned}

If τ and ρ are unrelated (i.e., they do not occur in each other), then the second case applies, by ρ in_{0} τ:

\begin{aligned}[ & ρ & /Z_{0}, & X & /Z_{1} & ] P_{0} & ≡ & P_{1} \\ [ & Y & /Z_{0}, & τ & /Z_{1} & ] P_{0} & ≡ & P_{2} \end{aligned}

As written, the cases are exclusive, for example, one cannot have both τ in_{0} ρ and ρ in_{0} τ, nor both ρ in_{0} τ and τ in_{k} ρ, which would otherwise be possible.

Lemma 5.1 (Type Generalization) Let σ_{1}, σ_{2} be two types such that [τ/X]σ_{1} = [ρ/Y]σ_{2} for some types τ and ρ. Assume that k is given either by τ in_{k} ρ for k > 0, or ρ in_{k} τ for k ≥ 0 and the previous case does not apply. Let h = 2^{k}. Given fresh type variables Z_{0}, …, Z_{h}, there exists a type σ_{0} that is a Z_{0}, …, Z_{h}-generalizer of σ_{1} and σ_{2}.

Proof: Assume first that τ in_{k} ρ for k > 0, and let σ = [τ/X]σ_{1} = [ρ/Y]σ_{2}.

\underline{τ-marking:} Mark in σ those occurrences of τ which derive from σ_{1} by a [τ/X] substitution. \underline{σ-marking:} Mark in σ those occurrences of ρ which derive from σ_{2} by a [ρ/Y] substitution. Observe that some of the marked τs may appear in a marked ρ. Construct then σ_{0} from σ by the following procedure:

1) Replace by Z_{0} all marked τs that do not occur in a marked ρ.

2) Consider now a marked ρ, possibly containing marked τs. Let ρ_{i}^{X} be the corresponding X-context in ρ for the marked τs. (If there are no marked τs, this will be ρ_{1}^{X} ≡ ρ). Replace the marked ρ by Z_{i}.

In case ρ in_{k} τ for k ≥ 0 and the previous case does not apply, perform the τ and σ-markings as above and observe that some of the marked ρs may appear in a marked τ. Then, apply the dual procedure, where the roles of ρ and τ in steps 1) and 2) are interchanged (and τ_{i}^{Y}, the Y -contexts for ρ in τ, are used instead of ρ_{i}^{X}, the X-contexts for τ in ρ). By construction, σ_{0} satisfies the definition of a generalizer.

In the following lemma, we show that, once fresh variables Z_{0}, …, Z_{h} are fixed, then the generalizer of two types is unique. This lemma makes explicit use of the substitution convention, i.e., that X, Y ∉ F V (τ) ∪ F V (ρ), without which it would fail.

Lemma 5.2 (Uniqueness of Type Generalizer) Let σ_{1}, σ_{2} be two types such that [τ/X]σ_{1} = [ρ/Y]σ_{2} for some types τ and ρ. Assume that k is given either by τ in_{k} ρ for k > 0, or ρ in_{k} τ for k ≥ 0 and the previous case does not apply. Let h = 2^{k}. Given fresh type variables Z_{0}, …, Z_{h}, the Z_{0}, …, Z_{h}- generalizer of σ_{1} and σ_{2} is unique.

Proof: Assume first that τ in_{k} ρ for k > 0.

Let σ_{0} and σ′_{0} be two Z_{0}, …, Z_{h}-generalizers of σ_{1}, σ_{2}. Then, by definition,

\begin{aligned}[ & X & /Z_{0}, & ρ_{1}^{X} & /Z_{1}, & …, & ρ_{h}^{X} & /Z_{h} & ] σ_{0} & = & σ_{1} & = & [ & X & /Z_{0}, & ρ_{1}^{X} & /Z_{1}, & …, & ρ_{h}^{X} & /Z_{h} & ] σ′_{0} & (1) \\ [ & τ & /Z_{0}, & Y & /Z_{1}, & …, & Y & /Z_{h} & ] σ_{0} & = & σ_{2} & = & [ & τ & /Z_{0}, & Y & /Z_{1}, & …, & Y & /Z_{h} & ] σ′_{0} & (2) \end{aligned}

with X and Y not free in σ_{0} or σ′_{0}. We will show that σ_{0} = σ′_{0} by induction on σ_{0}.

\underline{Subcase:} Assume that σ_{0} ≡ Z_{0}. Then, (1) and (2) become

\begin{aligned}X & = & σ_{1} & = & [ & X & /Z_{0}, & ρ_{1}^{X} & /Z_{1}, & …, & ρ_{h}^{X} & /Z_{h} & ] σ′_{0} \\ τ & = & σ_{2} & = & [ & τ & /Z_{0}, & Y & /Z_{1}, & …, & Y & /Z_{h} & ] σ′_{0} \end{aligned}

We now consider the possible choices for σ′_{0}. Clearly, σ′_{0} cannot be X since X ∉ F V (σ′_{0}). Nor can σ′_{0} be τ since then, (1) becomes X = σ_{1} = τ but, by the substitution convention, X ∉ F V (τ). Further, σ′_{0} cannot be Z_{i} for some i = 1 … h, because then (2) becomes τ = σ_{2} = Y but, by the substitution convention again, Y ∉ F V (τ). The only choice is σ′_{0} ≡ Z_{0} = σ_{0}.

\underline{Subcase:} Assume that σ_{0} ≡ Z_{i} for some i = 1 … h. Then, (1) and (2) become

\begin{aligned}ρ_{i}^{X} & = & σ_{1} & = & [ & X & /Z_{0}, & ρ_{1}^{X} & /Z_{1}, & …, & ρ_{h}^{X} & /Z_{h} & ] σ′_{0} \\ Y & = & σ_{2} & = & [ & τ & /Z_{0}, & Y & /Z_{1}, & …, & Y & /Z_{h} & ] σ′_{0} \end{aligned}

First, σ′_{0} cannot be Y since Y ∉ F V (σ′_{0}). Furthermore, σ′_{0} cannot be ρ_{i}^{X} since, for i = 1, (2) becomes Y = σ_{2} = ρ_{1}^{X} = ρ but, by the substitution convention, Y ∉ F V (ρ), and, for i = 2 … h, X ∈ F V (ρ_{i}^{X}) but X ∉ F V (σ′_{0}). Also, σ′_{0} cannot be Z_{0} since then, (2) becomes Y = σ_{2} = τ but, by the substitution convention again, Y ∉ F V (τ). Similarly, σ′_{0} cannot be Z_{j} for some j = 1 … h and j ≠ i since then,

(1) becomes ρ_{i}^{X} = σ_{1} = ρ_{j}^{X} but ρ_{i}^{X} ≠ ρ_{j}^{X} for i ≠ j. The only choice is σ′_{0} ≡ Z_{i} = σ_{0}. \underline{Subcase:} Assume that σ_{0} ≡ Z ≠ Z_{i} for i = 0 … h. Then, (1) and (2) become

\begin{aligned}Z & = & σ_{1} & = & [ & X & /Z_{0}, & ρ_{1}^{X} & /Z_{1}, & …, & ρ_{h}^{X} & /Z_{h} & ] σ′_{0} \\ Z & = & σ_{2} & = & [ & τ & /Z_{0}, & Y & /Z_{1}, & …, & Y & /Z_{h} & ] σ′_{0} \end{aligned}

Since X and Y are not free in σ_{0}, then Z ≠ X and Z ≠ Y and, moreover, σ′_{0} cannot be Z_{i} for any i = 0 … h. The only choice is σ′_{0} ≡ Z = σ_{0}.

\underline{Subcase:} Assume that σ_{0} ≡ σ → μ. Then, (1) and (2) become

\begin{aligned}[ & X & /Z_{0}, & ρ_{1}^{X} & /Z_{1}, & …, & ρ_{h}^{X} & /Z_{h} & ] (σ → μ) & = & σ_{1} & = & [ & X & /Z_{0}, & ρ_{1}^{X} & /Z_{1}, & …, & ρ_{h}^{X} & /Z_{h} & ] σ′_{0} \\ [ & τ & /Z_{0}, & Y & /Z_{1}, & …, & Y & /Z_{h} & ] (σ → μ) & = & σ_{2} & = & [ & τ & /Z_{0}, & Y & /Z_{1}, & …, & Y & /Z_{h} & ] σ′_{0} \end{aligned}

Remark that σ′_{0} cannot be Z_{i} for any i = 0 … h since, then, a → type would be on the left of (1) and (2) but a type variable would be on the right (X in (1) and Y in (2)). So, σ′_{0} must be of the form σ′ → μ′, with σ, σ′ and μ, μ′ satisfying equations similar to (1) and (2). By induction, σ = σ′ and μ = μ′. Hence, σ′_{0} ≡ σ′ → μ′ = σ → μ = σ_{0}.

\underline{Subcase:} Assume that σ_{0} ≡ ∀Z.σ. Then, (1) and (2) become

\begin{aligned}[ & X & /Z_{0}, & ρ_{1}^{X} & /Z_{1}, & …, & ρ_{h}^{X} & /Z_{h} & ] (∀Z.σ′) & = & σ_{1} & = & [ & X & /Z_{0}, & ρ_{1}^{X} & /Z_{1}, & …, & ρ_{h}^{X} & /Z_{h} & ] σ′_{0} \\ [ & τ & /Z_{0}, & Y & /Z_{1}, & …, & Y & /Z_{h} & ] (∀Z.σ′) & = & σ_{2} & = & [ & τ & /Z_{0}, & Y & /Z_{1}, & …, & Y & /Z_{h} & ] σ′_{0} \end{aligned}

As with the previous case, σ′_{0} cannot be Z_{i} for any i = 0 … h. So, σ′_{0} must be of the form ∀Z.σ′. By induction, σ = σ′. Hence, σ′_{0} ≡ ∀Z.σ′ = ∀Z.σ = σ_{0}.

Treat dually ρ in_{k} τ for k ≥ 0 and not the previous case.

Fact 5.3 Let σ_{1}, σ_{2}, μ_{1}, μ_{2} be types such that [τ/X]σ_{1} = [ρ/Y]σ_{2} and [τ/X]μ_{1} = [ρ/Y]μ_{2}. Assume that k is given either by τ in_{k} ρ for k > 0, or ρ in_{k} τ for k ≥ 0 and the previous case does not apply. Let h = 2^{k}. Given fresh type variables Z_{0}, …, Z_{h}, let σ_{0} and μ_{0} be the Z_{0}, …, Z_{h}-generalizers of σ_{1}, σ_{2} and μ_{1}, μ_{2}, respectively. Then, [μ_{0}/Z]σ_{0} is the Z_{0}, …, Z_{h}-generalizer of [μ_{1}/Z]σ_{1} and [μ_{2}/Z]σ_{2}.

Lemma 5.4 (Generalization of Declarations) Let Γ_{1}, Γ_{2} be two sets of declarations such that [τ/X]Γ_{1} = [ρ/Y]Γ_{2}. Assume that k is given either by τ in_{k} ρ for k > 0, or ρ in_{k} τ for k ≥ 0 and the previous case does not apply. Let h = 2^{k}. Given fresh type variables Z_{0}, …, Z_{h}, there exists a set of declarations Γ_{0} that is a unique Z_{0}, …, Z_{h}-generalizer of Γ_{1} and Γ_{2}.

Proof: Since [τ/X]Γ_{1} = [ρ/Y]Γ_{2}, then Γ_{1} and Γ_{2} must contain declarations of the same term variables. Thus, Γ_{1} ≡ x_{1} :σ_{1}^{1}, …, x_{n}:σ_{n}^{1} and Γ_{2} ≡ x_{1} :σ_{1}^{2}, …, x_{n}:σ_{n}^{2} with [τ/X]σ_{i}^{1} = [ρ/Y]σ_{i}^{2} for i = 1 … n. For i = 1 … n, construct the unique Z_{0}, …, Z_{h}-generalizer σ_{i}^{0} of σ_{i}^{1} and σ_{i}^{2}. Then, Γ_{0} ≡ x_{1} :σ_{1}^{0}, …, x_{n}:σ_{n}^{0} is the unique Z_{0}, …, Z_{h}-generalizer of Γ_{1} and Γ_{2}.

The following theorem is the main result of this section. It constructs a well-typed generalizer of two terms living in two different types. Uniqueness of type generalizers turns out to be essential in the proof (see the →-elim case). The point to note here is not just that we can construct a generalizer for M_{1} and M_{2} but that we can construct one that is well-typed and that lives in the type generalizer of the types of M_{1} and M_{2}.

Theorem 5.5 (Term Generalization) Let Γ_{1} ⊢ M_{1} : σ_{1} and Γ_{2} ⊢ M_{2} : σ_{2} be such that [τ/X]Γ_{1} = [ρ/Y]Γ_{2} and [τ/X]M_{1} ≡ [ρ/Y]M_{2} for some types τ and ρ. Assume that k is given either by τ in_{k} ρ for k > 0, or ρ in_{k} τ for k ≥ 0 and the previous case does not apply. Let h = 2^{k}. Given fresh type variables Z_{0}, …, Z_{h}, there exist a set of declarations Γ_{0}, a term M_{0}, and a type σ_{0} that are unique Z_{0}, …, Z_{h}-generalizers of Γ_{1}, Γ_{2}; M_{1}, M_{2}; and σ_{1}, σ_{2}, respectively, such that Γ_{0} ⊢ M_{0} : σ_{0}.

Proof: We will construct Γ_{0}, M_{0}, σ_{0} by induction on the derivation of Γ_{1} ⊢ M_{1} : σ_{1}. (In

the proof, we will write simply “generalizer” instead of “Z_{0}, …, Z_{h}-generalizer”). \underline{Case:} Assume that Γ_{1} ⊢ M_{1} : σ_{1} by a variable declaration in Γ_{1}.

Then, M_{1} ≡ x and x:σ_{1} ∈ Γ_{1} for some term variable x.

¿From the assumption [τ/X]M_{1} ≡ [ρ/Y]M_{2}, we obtain M_{2} ≡ x.

Furthermore, because Γ_{2} ⊢ M_{2} : σ_{2}, then x:σ_{2} ∈ Γ_{2}.

And, since [τ/X]Γ_{1} = [ρ/Y]Γ_{2} with x:σ_{1} ∈ Γ_{1} and x:σ_{2} ∈ Γ_{2},

then [τ/X]σ_{1} = [ρ/Y]σ_{2}.

Take σ_{0} to be the unique generalizer of σ_{1}, σ_{2} by Type Generalization (Lemma 5.1), and Γ_{0} to be the unique generalizer of Γ_{1}, Γ_{2} by Lemma 5.4. Observe that, by construction, x : σ_{0} ∈ Γ_{0}, from which, by the declaration rule, Γ_{0} ⊢ x : σ_{0}. Since x is clearly the only generalizer of M_{1}, M_{2}, take M_{0} ≡ x.

\underline{Case:} Assume that Γ_{1} ⊢ M_{1} : σ_{1} is derived by →-intro. Then, M_{1} ≡ λx:μ_{1}.M′_{1} and σ_{1} ≡ μ_{1} → ρ_{1} with Γ_{1}, x:μ_{1} ⊢ M′_{1} : ρ_{1}. ¿From [τ/X]M_{1} ≡ [ρ/Y]M_{2}, we obtain M_{2} ≡ λx:μ_{2}.M′_{2} with [τ/X]μ_{1} = [ρ/Y]μ_{2} and [τ/X]M′_{1} ≡ [ρ/Y]M′_{2}. Furthermore, because Γ_{2} ⊢ M_{2} : σ_{2}, then σ_{2} ≡ μ_{2} → ρ_{2} and Γ_{2}, x:μ_{2} ⊢ M′_{2} : ρ_{2}. Consider now Γ_{1}, x:μ_{1} ⊢ M′_{1} : ρ_{1} and Γ_{2}, x:μ_{2} ⊢ M′_{2} : ρ_{2}. By induction, there exist unique generalizers: Γ′_{0} of (Γ_{1}, x:μ_{1}), (Γ_{2}, x:μ_{2}); M′_{0} of M′_{1}, M′_{2}; and ρ_{0} of ρ_{1}, ρ_{2}, such that Γ′_{0} ⊢ M′_{0} : ρ_{0}. But, since generalizers of types and sets of declarations are unique, then Γ′_{0} must be Γ_{0}, x:μ_{0} where Γ_{0} and μ_{0} are unique generalizers of Γ_{1}, Γ_{2} and μ_{1}, μ_{2}, respectively. So, in fact, Γ_{0}, x:μ_{0} ⊢ M′_{0} : ρ_{0}, from which, by →-intro, Γ_{0} ⊢ λx:μ_{0}.M′_{0} : μ_{0} → ρ_{0}. Clearly, λx:μ_{0}.M′_{0} and μ_{0} → ρ_{0} are generalizers of M_{1}, M_{2} and σ_{1}, σ_{2}. Moreover, μ_{0} → ρ_{0} is unique by the uniqueness of type generalizers, and λx:μ_{0}.M′_{0} is unique because any other generalizer of M_{1}, M_{2} would be of the form λx : μ′_{0}.M′′_{0} giving further generalizers, μ′_{0} and M′′_{0}, of μ_{1}, μ_{2} and M′_{1}, M′_{2}, which is impossible. Hence, take M_{0} ≡ λx:μ_{0}.M′_{0} and σ_{0} ≡ μ_{0} → ρ_{0}.

\underline{Case:} Assume that Γ_{1} ⊢ M_{1} : σ_{1} is derived by →-elim. Then, M_{1} ≡ M′_{1}N′_{1} with Γ_{1} ⊢ M′_{1} : ρ_{1} → σ_{1} and Γ_{1} ⊢ N′_{1} : ρ_{1}. ¿From [τ/X]M_{1} ≡ [ρ/Y]M_{2}, we obtain M_{2} ≡ M′_{2}N′_{2} with [τ/X]M′_{1} ≡ [ρ/Y]M′_{2} and [τ/X]N′_{1} ≡ [ρ/Y]N′_{2}. Furthermore, because Γ_{2} ⊢ M_{2} : σ_{2}, then Γ_{2} ⊢ M′_{2} : ρ_{2} → σ_{2} and Γ_{2} ⊢ N′_{2} : ρ_{2}. Consider now Γ_{1} ⊢ N′_{1} : ρ_{1} and Γ_{2} ⊢ N′_{2} : ρ_{2}. By induction, there exist unique generalizers: Γ_{0} of Γ_{1}, Γ_{2}; N′_{0} of N′_{1}, N′_{2}; and ρ_{0} of ρ_{1}, ρ_{2}, such that Γ_{0} ⊢ N′_{0} : ρ_{0}. Consider also Γ_{1} ⊢ M′_{1} : ρ_{1} → σ_{1} and Γ_{2} ⊢ M′_{2} : ρ_{2} → σ_{2}. By induction, there exist unique generalizers: M′_{0} of M′_{1}, M′_{2} and ρ′ of ρ_{1} → σ_{1}, ρ_{2} → σ_{2}, such that Γ_{0} ⊢ M′_{0} : ρ′. But by the uniqueness of type generalizers, ρ′ must be ρ_{0} → σ_{0}, where ρ_{0} and σ_{0} are unique generalizers of ρ_{1}, ρ_{2} and σ_{1}, σ_{2}, respectively. Thus, we have Γ_{0} ⊢ M′_{0} : ρ_{0} → σ_{0} and Γ_{0} ⊢ N′_{0} : ρ_{0}. So, by →-elim, Γ_{0} ⊢ M′_{0}N′_{0} : σ_{0}. Since M′_{0}N′_{0} is clearly a generalizer of M_{1}, M_{2}, with uniqueness proven as in the previous case, take M_{0} ≡ M′_{0}N′_{0}.

\underline{Case:} Assume that Γ_{1} ⊢ M_{1} : σ_{1} is derived by ∀-intro. Then, M_{1} ≡ λZ.M′_{1} and σ_{1} ≡ ∀Z.μ_{1} with Γ_{1} ⊢ M′_{1} : μ_{1} and Z not free in the type of any free term variable in M′_{1}. ¿From [τ/X]M_{1} ≡ [ρ/Y]M_{2}, we obtain M_{2} ≡ λZ.M′_{2} with [τ/X]M′_{1} ≡ [ρ/Y]M′_{2}. Furthermore, because Γ_{2} ⊢ M_{2} : σ_{2}, then σ_{2} ≡ ∀Z.μ_{2} and Γ_{2} ⊢ M′_{2} : μ_{2} with Z not free in the type of any free term variable in M′_{2}. Consider now Γ_{1} ⊢ M′_{1} : μ_{1} and Γ_{2} ⊢ M′_{2} : μ_{2}. By induction, there exist unique generalizers: Γ_{0} of Γ_{1}, Γ_{2}; M′_{0} of M′_{1}, M′_{2}; and μ_{0} of μ_{1}, μ_{2}, such that Γ_{0} ⊢ M′_{0} : μ_{0}. Observe now that Z is not free in the type of any free term variable in M′_{0}, since, by definition of generalizer, M′_{0} contains exactly the free term variables of M′_{1}, M′_{2}. Thus, we can apply ∀-intro to Γ_{0} ⊢ M′_{0} : μ_{0} to obtain Γ_{0} ⊢ λZ.M′_{0} : ∀Z.μ_{0}. Clearly, λZ.M′_{0} and ∀Z.μ_{0} are generalizers of M_{1}, M_{2} and σ_{1}, σ_{2}, respectively. Their uniqueness follows as before. Hence, take M_{0} ≡ λZ.M′_{0} and σ_{0} ≡ ∀Z.μ_{0}.

\underline{Case:} Assume that Γ_{1} ⊢ M_{1} : σ_{1} is derived by ∀-elim.

Then, M_{1} ≡ M′_{1}μ_{1} and σ_{1} ≡ [μ_{1}/Z]ρ_{1} with Γ_{1} ⊢ M′_{1} : ∀Z.ρ_{1}. ¿From [τ/X]M_{1} ≡ [ρ/Y]M_{2}, we obtain M_{2} ≡ M′_{2}μ_{2} with [τ/X]M′_{1} ≡ [ρ/Y]M′_{2} and [τ/X]μ_{1} = [ρ/Y]μ_{2}. Furthermore, since Γ_{2} ⊢ M_{2} : σ_{2}, then Γ_{2} ⊢ M′_{2} : ∀Z.ρ_{2} and σ_{2} ≡ [μ_{2}/Z]ρ_{2}. Consider now Γ_{1} ⊢ M′_{1} : ∀Z.ρ_{1} and Γ_{2} ⊢ M′_{2} : ∀Z.ρ_{2}. By induction, there exist unique generalizers: Γ_{0} of Γ_{1}, Γ_{2}; M′_{0} of M′_{1}, M′_{2}; and ρ′ of ∀Z.ρ_{1}, ∀Z.ρ_{2}, such that Γ_{0} ⊢ M′_{0} : ρ′. Since type generalizers are unique, ρ′ must be ∀Z.ρ_{0}, where ρ_{0} is the generalizer of ρ_{1}, ρ_{2}. Thus, we have Γ_{0} ⊢ M′_{0} : ∀Z.ρ_{0}, from which, by ∀-elim, Γ_{0} ⊢ M′_{0}μ_{0} : [μ_{0}/Z]ρ_{0}, where μ_{0} is the unique generalizer of μ_{1}, μ_{2} by Type Generalization (Lemma 5.1). Clearly, M′_{0}μ_{0} is a generalizer of M_{1}, M_{2}, with uniqueness proven as before. Furthermore, by Fact 5.3, [μ_{0}/Z]ρ_{0} is the unique generalizer of σ_{1} ≡ [μ_{1}/Z]ρ_{1}, σ_{2} ≡ [μ_{2}/Z]ρ_{2}. Hence, take M_{0} ≡ M′_{0}μ_{0} and σ_{0} ≡ [μ_{0}/Z]ρ_{0}.

6 Quasi-Genericity of C^{∗}-equality

This section shows that applications of Axiom C^{∗} preserve the type substitution structure of terms. That is, if Axiom C^{∗} is applied to a term of the form [τ/X]M, then the result is also of the form [τ/X]N, and furthermore, M =_{c^{∗}} N. We call this property Quasi-Genericity of C^{∗}-equality (since it resembles genericity). The proof of this uses generalizers.

We will write M =^{1}_{c^{∗}} N if M and N are made equal by one application of Axiom C^{∗} only, and M =_{c^{∗}} N if Axiom C^{∗} is applied zero or more times. Clearly, if M =^{1}_{c^{∗}} N, then the single application of Axiom C^{∗} may have been made either to a proper subterm of M, or to the entire term M. Note, however, that an application of Axiom C^{∗} to a term cannot always be split into applications to subterms, as the example of section 4 shows.

Theorem 6.1 (Quasi-Genericity of C^{∗}-equality) If [τ/X]M =_{c^{∗}} N′ then there exists a term N such that N′ ≡ [τ/X]N and M =_{c^{∗}} N.

Proof: We will construct N by induction on the number of applications of Axiom C^{∗} in [τ/X]M =_{c^{∗}} N′. If there are 0 applications, i.e., [τ/X]M ≡ N′, then, clearly, take N ≡ M. We prove only the case [τ/X]M =^{1}_{c^{∗}} N′ as the inductive case holds by transitivity. With no loss of generality, by variable renaming, we can assume that X ∉ F V (N′).

Assume then that [τ/X]M =^{1}_{c^{∗}} N′. Then, as previously remarked, Axiom C^{∗} is applied either to a proper subterm of [τ/X]M, or to [τ/X]M itself. If Axiom C^{∗} is applied to a proper subterm, the proof proceeds by straightforward induction on the structure of M. We display here the case when Axiom C^{∗} is applied to [τ/X]M itself (this includes the base case of the previous induction on M). Then, by definition of Axiom C^{∗}, there exists a term M′, types ρ, ρ′, and a type variable Y, such that

[τ/X]M ≡ [ρ/Y]M′ =^{1}_{c^{∗}} [ρ′/Y]M′ ≡ N′  (3)

where, for Γ ⊢ M : σ, we have Γ ⊢ M′ : σ′, and Y not free in Γ nor σ′. Since Axiom C^{∗} is actually applied, then Y ∈ F V (M′) and, thus, X ∉ F V (ρ′); otherwise X would be free in N′, contradicting the assumption. We now apply Term Generalization to [τ/X]M ≡ [ρ/Y]M′.

\underline{Case:} Assume that τ in_{k} ρ for k > 0.

Choose fresh type variables Z_{0}, …, Z_{h} where h = 2^{k}. Then, by Term Generalization (Theorem 5.5), there exist unique Z_{0}, …, Z_{h}-generalizers: Γ_{0} of Γ, Γ; M_{0} of M, M′; and σ_{0} of σ, σ′, such that Γ_{0} ⊢ M_{0} : σ_{0}. Observe now that, by definition of generalizer, we have that Γ = [τ/Z_{0}, Y/Z_{1}, …, Y/Z_{h}] Γ_{0} and σ′ = [τ/Z_{0}, Y/Z_{1}, …, Y/Z_{h}] σ_{0}. But, we also have that Y is not free in Γ or σ′. So Z_{1}, …, Z_{h} cannot be free in Γ_{0} or σ_{0}. Hence, since Γ_{0} ⊢ M_{0} : σ_{0}, we can apply Axiom C^{∗} to M_{0} for the variables Z_{1}, …, Z_{h}. Thus, if we take

N ≡ [X/Z_{0}, ρ′/Z_{1}, …, ρ′/Z_{h}] M_{0}

we get the desired result, as

M ≡ [X/Z_{0}, ρ_{1}^{X}/Z_{1}, …, ρ_{h}^{X}/Z_{h}] M_{0}  M_{0} is the generalizer of M, M′
=_{c^{∗}} [X/Z_{0}, ρ′/Z_{1}, …, ρ′/Z_{h}] M_{0}  by Axiom C^{∗} for Z_{1}, …, Z_{h}
≡ N

and

[τ/X] N ≡ [τ/Z_{0}, ρ′/Z_{1}, …, ρ′/Z_{h}] M_{0}  since X ∉ F V (ρ′)
≡ [ρ′/Y] [τ/Z_{0}, Y/Z_{1}, …, Y/Z_{h}] M_{0} by rearranging substitutions
≡ [ρ′/Y] M′  M_{0} is the generalizer of M, M′
≡ N′  by (3)

\underline{Case:} Assume that ρ in_{k} τ for k ≥ 0 and the previous case does not apply. Choose fresh type variables Z_{0}, …, Z_{h} where h = 2^{k}. Then, by Term Generalization (Theorem 5.5), there exist unique Z_{0}, …, Z_{h}-generalizers: Γ_{0} of Γ, Γ; M_{0} of M, M′; and σ_{0} of σ, σ′, such that Γ_{0} ⊢ M_{0} : σ_{0}. Observe now that, by definition of generalizer, we have that Γ = [Y/Z_{0}, τ/Z_{1}, τ_{2}^{Y} /Z_{2}, …, τ_{h}^{Y} /Z_{h}] Γ_{0} and σ′ = [Y/Z_{0}, τ/Z_{1}, τ_{2}^{Y} /Z_{2}, …, τ_{h}^{Y} /Z_{h}] σ_{0}. But, we also have that Y is not free in Γ or σ′. So Z_{0}, Z_{2}, …, Z_{h} cannot be free in Γ_{0} or σ_{0}. Hence, since Γ_{0} ⊢ M_{0} : σ_{0}, we can apply Axiom C^{∗} to M_{0} for the variables Z_{0}, Z_{2}, …, Z_{h}. Thus, if we let τ′_{i} ≡ [ρ′/Y]τ_{i}^{Y}, and we take

N ≡ [ρ′/Z_{0}, X/Z_{1}, τ′_{2}/Z_{2}, …, τ′_{h}/Z_{h}] M_{0}

we get the desired result, as

M ≡ [ρ/Z_{0}, X/Z_{1}, X/Z_{2}, …, X/Z_{h}] M_{0}  M_{0} is the generalizer of M, M′
=_{c^{∗}} [ρ′/Z_{0}, X/Z_{1}, τ′_{2}/Z_{2}, …, τ′_{h}/Z_{h}] M_{0}  by Axiom C^{∗} for Z_{0}, Z_{2}, …, Z_{h}
≡ N

and

[τ/X] N ≡ [ρ′/Z_{0}, τ/Z_{1}, τ′_{2}/Z_{2}, …, τ′_{h}/Z_{h}] M_{0}  since X ∉ F V (ρ′)
≡ [ρ′/Y] [Y/Z_{0}, τ/Z_{1}, τ_{2}^{Y} /Z_{2}, …, τ_{h}^{Y} /Z_{h}] M_{0}

by rearranging substitutions

≡ [ρ′/Y] M′  M_{0} is the generalizer of M, M′
≡ N′  by (3)

Note that the property of preserving type substitution structure does not hold for Fequality. Backward β_{2} reduction causes problems as witnessed by the following counterexample. Assume x has type ∀Y.Y, and take M ≡ xX with τ ≡ σ_{1} → σ_{2} and N′ ≡ (λZ.x(Z → σ_{2}))σ_{1}. Then,

[τ/X]M ≡ x(σ_{1} → σ_{2}) _{β_{2}}⟵ (λZ.x(Z → σ_{2}))σ_{1} ≡ N′

Now, since τ ≡ σ_{1} → σ_{2} does not occur in N′, then any N such that [τ/X]N ≡ N′ cannot contain X free. Thus, N ≡ [τ/X]N ≡ N′, and N has type τ. But M has type X. Hence, M = N is impossible since they live in different types.

However, all forward reductions preserve type substitution structure, as does backward η_{2} reduction. Proofs of thes are straightforward.

Fact 6.2 If [τ/X]M ⟶_{F} N′ then there exists a term N such that N′ ≡ [τ/X]N and M ⟶_{F} N.

Fact 6.3 If [τ/X]M _{η_{2}}⟵ N′ then there exists a term N such that N′ ≡ [τ/X]N and M _{η_{2}}⟵ N.

7 Weak Genericity

In this section, we prove two weaker forms of the Genericity Theorem, which will be used in the final result. The weakness or asymmetry arises because =_{F} and =_{c^{∗}} are used respectively in the premise instead of =_{F c}. Generalizers are a key tool in the proof with =_{F}. We first need the following lemma about simultaneous substitutions.

Lemma 7.1 Given type σ, if [τ_{1}/X_{1}, …, τ_{n}/X_{n}] σ = [ρ_{1}/X_{1}, …, ρ_{n}/X_{n}] σ and τ_{i} ≠ ρ_{i} for some 1 ≤ i ≤ n, then X_{i} is not free in σ.

Proof: by induction on the structure of σ. Note that the substitution convention is used to assume that X_{1}, …, X_{n} are not free in τ_{1}, …, τ_{n}, ρ_{1}, … ρ_{n}.

Theorem 7.2 (Weak Genericity of F-equality) Let Γ ⊢ M_{1}, M_{2} : σ. If [τ/X]M_{1} =_{F} [τ/X]M_{2} for some type τ, then M_{1} =_{F c} M_{2}.

Proof: Let M′_{1} and M′_{2} be the normal forms of M_{1} and M_{2}. Then, Γ ⊢ M′_{1}, M′_{2} : σ, since normalization preserves typing. Furthermore, since reduction is type-substitutive^{1}, and since type substitution preserves normal forms, then, from [τ/X]M_{1} =_{F} [τ/X]M_{2}, we obtain [τ/X]M′_{1} ≡ [τ/X]M′_{2}. We now apply Term Generalization to

[τ/X]M′_{1} ≡ [τ/X]M′_{2}  (4)

We are in the case τ = ρ so case 1) of the definition of generalizer applies, i.e. h = 1. Thus, choose fresh type variables Z_{0}, Z_{1}, Z_{2}. Then, by Term Generalization (Theorem 5.5), there exist unique Z_{0}, Z_{1}, Z_{2}-generalizers: Γ_{0} of Γ, Γ; M′_{0} of M′_{1}, M′_{2}; and σ_{0} of σ, σ, such that Γ_{0} ⊢ M′_{0} : σ_{0}. By definition of generalizer, we have

\begin{aligned}[X/Z_{0}, τ/Z_{1}, X/Z_{2}] Γ_{0} & = & Γ & = & [τ/Z_{0}, X/Z_{1}, X/Z_{2}] Γ_{0} \\ [X/Z_{0}, τ/Z_{1}, X/Z_{2}] σ_{0} & = & σ & = & [τ/Z_{0}, X/Z_{1}, X/Z_{2}] σ_{0} \end{aligned}

Now, by the substitution convention applied to (4), X ∉ F V (τ). So, in particular, τ ≠ X. We can thus apply lemma 7.1 to the above two equations to obtain that Z_{0} and Z_{1} are not free in Γ_{0} and σ_{0}. Hence, we can apply Axiom C^{∗} to M′_{0} for Z_{0}, Z_{1} in the following:

M_{1} =_{F} M′_{1}  M′_{1} is the normal form of M_{1}
≡ [X/Z_{0}, τ/Z_{1}, X/Z_{2}] M′_{0}  M′_{0} is the generalizer of M′_{1}, M′_{2}
=_{F c} [τ/Z_{0}, X/Z_{1}, X/Z_{2}] M′_{0}  by Axiom C^{∗} for Z_{0}, Z_{1}
≡ M′_{2}  M′_{0} is the generalizer of M′_{1}, M′_{2}
=_{F} M_{2}  M′_{2} is the normal form of M_{2}

1If M reduces to M′ then [τ/X]M reduces to [τ/X]M′ (cf. [Bar84, page 55]).

Theorem 7.3 (Weak Genericity of C^{∗}-equality) Let Γ ⊢ M_{1}, M_{2} : σ. If [τ/X]M_{1} =_{c^{∗}} [τ/X]M_{2} for some type τ, then M_{1} =_{F c} M_{2}.

Proof: Apply Quasi-Genericity of C^{∗}-equality (Theorem 6.1) to [τ/X]M_{1} =_{c^{∗}} [τ/X]M_{2}. Thus, there exists a term N such that M_{1} =_{F c} N and [τ/X]N ≡ [τ/X]M_{2}. Observe that, since M_{1} =_{F c} N, then N must live in σ, the type of M_{1} and M_{2}. Apply now Weak Genericity of F-equality (Theorem 7.2) to [τ/X]N ≡ [τ/X]M_{2}. Then, N =_{F c} M_{2}. Hence, M_{1} =_{F c} N =_{F c} M_{2}.

We will not use the two corollaries below but they clarify where we are in the overall proof, namely at weak forms of the Genericity Theorem.

Corollary 7.4 Let Γ ⊢ M, N : ∀X.σ. If Mτ =_{F} Nτ for some type τ, then M =_{F c} N.

Corollary 7.5 Let Γ ⊢ M, N : ∀X.σ. If Mτ =_{c^{∗}} Nτ for some type τ, then M =_{F c} N.

8 Commutativity of C^{∗}-equality with Reduction

This section describes the commutativity of C^{∗}-equality with reduction. It turns out that C^{∗}-equality commutes with β_{1}, β_{2}, and η_{1} reductions but not with η_{2} reduction. To see this last point, take M of type ∀Z.σ with Z ∉ F V (σ), and X fresh. Then,

λX.MX =_{c} λX.Mτ^{η_{2}}M

but λX.Mτ does not η_{2}-reduce to M.

We need the following lemma about the substitutivity of C^{∗}-equality.

Lemma 8.1 (Substitutivity of C^{∗}-equality) If M_{1} =_{c^{∗}} M_{2} and N_{1} =_{c^{∗}} N_{2} then [N_{1}/x]M_{1} =_{c^{∗}} [N_{2}/x]M_{2} and [τ/X]M_{1} =_{c^{∗}} [τ/X]M_{2}.

Proof: An easy induction on the structure of M_{1}.

We now prove that C^{∗}-equality commutes with β_{1}β_{2}η_{1} reduction, first for the onestep case, then for the multi-step case. Note that, in the one-step case, a multi-step C^{∗}-equality completes the commuting diagram.

Lemma 8.2 (One-Step Commutativity)

If  M =^{1}_{c^{∗}} N_{β_{1}β_{2}η_{1}} _{1} M′  then there exists a term N′ such that [figure: M; =^{1}_{c^{∗}}; N; β_{1}β_{2}η_{1}; 1; M′; =_{c^{∗}}; N′; β_{1}β_{2}η_{1}; 1]

Proof: By case analysis of M ⟶^{1}_{β_{1}β_{2}η_{1}} M′ and M =^{1}_{c^{∗}} N. Since β_{1}β_{2}η_{1} is substitutive, we can assume that the reduction is applied directly to M, ignoring the cases where it is applied to a subterm or superterm of M.

\underline{Case:} (λx:μ.M_{1})M_{2} ⟶^{1}_{β_{1}} [M_{2}/x]M_{1}.

Subcase: Assume that Axiom C^{∗} is applied to M_{1}.

Then, M_{1} =^{1}_{c^{∗}} N_{1} and (λx:μ.M_{1})M_{2} =^{1}_{c^{∗}} (λx:μ.N_{1})M_{2}.

Clearly, (λx:μ.N_{1})M_{2} ⟶^{1}_{β_{1}} [M_{2}/x]N_{1}.

And, by lemma 8.1, [M_{2}/x]M_{1} =_{c^{∗}} [M_{2}/x]N_{1}. Therefore, take N′ ≡ [M_{2}/x]N_{1}.

Subcase: Assume that Axiom C^{∗} is applied to M_{2}.

Then, M_{2} =^{1}_{c^{∗}} N_{2} and (λx:μ.M_{1})M_{2} =^{1}_{c^{∗}} (λx:μ.M_{1})N_{2}.

Clearly, (λx:μ.M_{1})N_{2} ⟶^{1}_{β_{1}} [N_{2}/x]M_{1}.

And, by lemma 8.1, [M_{2}/x]M_{1} =_{c^{∗}} [N_{2}/x]M_{1}. Therefore, take N′ ≡ [N_{2}/x]M_{1}.

Subcase: Assume that Axiom C^{∗} is applied to λx:μ.M_{1}. Then, by definition of Axiom C^{∗}, there exist ν, N_{1}, ρ, ρ′, Y such that

λx:μ.M_{1} ≡ [ρ/Y] (λx:ν.N_{1}) =^{1}_{c^{∗}} [ρ′/Y] (λx:ν.N_{1})

with μ = [ρ/Y]ν and M_{1} ≡ [ρ/Y]N_{1}, and Γ ⊢ λx:ν.N_{1} : ν → σ, and Y not free in Γ or ν → σ. Clearly, Y is also not free in ν. Hence, μ = [ρ/Y]ν = ν. Moreover, Y is not free in σ, the type of N_{1}. Axiom C^{∗} is therefore applied to M_{1} ≡ [ρ/Y]N_{1} and that subcase applies.

Subcase: Assume that Axiom C^{∗} is applied to (λx:μ.M_{1})M_{2}. Then, by definition of Axiom C^{∗}, there exist ν, N_{1}, N_{2}, ρ, ρ′, Y such that

(λx:μ.M_{1})M_{2} ≡ [ρ/Y] ((λx:ν.N_{1})N_{2}) =^{1}_{c^{∗}} [ρ′/Y] ((λx:ν.N_{1})N_{2})

with μ = [ρ/Y]ν, M_{1} ≡ [ρ/Y]N_{1}, M_{2} ≡ [ρ/Y]N_{2}, and Γ ⊢ (λx:ν.N_{1})N_{2} : σ, and Y not free in Γ or σ. Since Γ ⊢ (λx:ν.N_{1})N_{2} : σ, then Γ ⊢ [N_{2}/x]N_{1} : σ. Axiom C^{∗} can thus be applied to [N_{2}/x]N_{1}. Hence, take N′ ≡ [ρ′/Y][N_{2}/x]N_{1}, for then

[M_{2}/x]M_{1} ≡ [ρ/Y][N_{2}/x]N_{1} since M_{1} ≡ [ρ/Y]N_{1} and M_{2} ≡ [ρ/Y]N_{2}
=_{c^{∗}} [ρ′/Y][N_{2}/x]N_{1} by Axiom C^{∗}

and [ρ′/Y] ((λx:ν.N_{1})N_{2}) ⟶^{1}_{β_{1}} [ρ′/Y][N_{2}/x]N_{1}, since β_{1} is substitutive.

\underline{Case:} (λX.M_{1}) μ ⟶^{1}_{β_{2}} [μ/X] M_{1}.

Subcase: Assume that Axiom C^{∗} is applied to M_{1}.

Then, M_{1} =^{1}_{c^{∗}} N_{1} and (λX.M_{1}) μ =^{1}_{c^{∗}} (λX.N_{1}) μ.

Clearly, (λX.N_{1}) μ ⟶^{1}_{β_{2}} [μ/X]N_{1}.

And, by lemma 8.1, [μ/X]M_{1} =_{c^{∗}} [μ/X]N_{1}. Therefore, take N′ ≡ [μ/X]N_{1}.

Subcase: Assume that Axiom C^{∗} is applied to λX.M_{1}. Then, by definition of Axiom C^{∗}, there exist N_{1}, ρ, ρ′, Y such that

λX.M_{1} ≡ [ρ/Y] (λX.N_{1}) =^{1}_{c^{∗}} [ρ′/Y] (λX.N_{1})

with M_{1} ≡ [ρ/Y]N_{1}, and Γ ⊢ λX.N_{1} : ∀X.σ, and Y not free in Γ or ∀X.σ. Clearly, Y is not free in σ, the type of N_{1}. Axiom C^{∗} is therefore applied to M_{1} ≡ [ρ/Y]N_{1} and that subcase applies.

Subcase: Assume that Axiom C^{∗} is applied to (λX.M_{1})μ. Then, by definition of Axiom C^{∗}, there exist N_{1}, ν, ρ, ρ′, Y such that

(λX.M_{1})μ ≡ [ρ/Y] ((λX.N_{1})ν) =^{1}_{c^{∗}} [ρ′/Y] ((λX.N_{1})ν)

with M_{1} ≡ [ρ/Y]N_{1} and μ = [ρ/Y]ν, and Γ ⊢ (λX.N_{1})ν : σ, and Y not free in Γ or σ. Since Γ ⊢ (λX.N_{1})ν : σ, then Γ ⊢ [ν/X]N_{1} : σ. Axiom C^{∗} can thus be applied to [ν/X]N_{1}. Hence, take N′ ≡ [ρ′/Y][ν/X]N_{1}, for then

[μ/X]M_{1} ≡ [ρ/Y][ν/X]N_{1} since μ ≡ [ρ/Y]ν and M_{1} ≡ [ρ/Y]N_{1}
=_{c^{∗}} [ρ′/Y][ν/X]N_{1} by Axiom C^{∗}

and [ρ′/Y] ((λX.N_{1})ν) ⟶^{1}_{β_{2}} [ρ′/Y][ν/X]N_{1}, since β_{2} is substitutive. \underline{Case:} λx:μ.M_{1}x ⟶^{1}_{η_{1}} M_{1} with x not free in M_{1}.

Subcase: Assume that Axiom C^{∗} is applied to M_{1}.

Then, M_{1} =^{1}_{c^{∗}} N_{1} and λx:μ.M_{1}x =^{1}_{c^{∗}} λx:μ.N_{1}x.

Now, since x is not free in M_{1} and since Axiom C^{∗} does not affect term variables, then x is also not free in N_{1}. Thus, λx:μ.N_{1}x ⟶^{1}_{η_{1}} N_{1}. Therefore, take N′ ≡ N_{1}.

Subcase: Assume that Axiom C^{∗} is applied to M_{1}x. Then, by definition of Axiom C^{∗}, there exist N_{1}, ρ, ρ′, Y such that

M_{1}x ≡ [ρ/Y] (N_{1}x) =^{1}_{c^{∗}} [ρ′/Y] (N_{1}x)

with M_{1} = [ρ/Y]N_{1}, and Γ, x:μ ⊢ N_{1}x : σ, and Y not free in Γ, x:μ or σ. Clearly, Y is also not free in μ → σ, the type of N_{1}. Axiom C^{∗} is therefore applied to M_{1} ≡ [ρ/Y]N_{1} and that subcase applies.

Subcase: Assume that Axiom C^{∗} is applied to λx:μ.M_{1}x. Then, by definition of Axiom C^{∗}, there exist ν, N_{1}, ρ, ρ′, Y such that

λx:μ.M_{1}x ≡ [ρ/Y] (λx:ν.N_{1}x) =^{1}_{c^{∗}} [ρ′/Y] (λx:ν.N_{1}x) with μ = [ρ/Y]ν

M_{1} = [ρ/Y]N_{1}, Γ ⊢ λx:ν.N_{1}x : ν → σ, and Y not free in Γ or ν → σ. Y is therefore not free in ν, so, μ = [ρ/Y]ν = ν. Also, Y is not free in σ, the type of N_{1}x. Axiom C^{∗} is thus applied to M_{1}x ≡ [ρ/Y](N_{1}x) and that subcase applies.

Theorem 8.3 (Commutativity)

If  M =_{c^{∗}} N_{β_{1}β_{2}η_{1}}M′  then there exists a term N′ such that [figure: M; =_{c^{∗}}; N; β_{1}β_{2}η_{1}; M′; =_{c^{∗}}; N′; β_{1}β_{2}η_{1}]

Proof: By decomposing the multi-step C^{∗}-equalities and β_{1}β_{2}η_{1}-reductions into single steps, and using One-Step Commutativity (Lemma 8.2) to complete the following diagram:

[figure: M; ^{=^{1}^{c^{∗}}}; N_{1}; ^{=^{1}^{c^{∗}}}; …; ^{=^{1}^{c^{∗}}}; N; β_{1}β_{2}η_{1}; 1; β_{1}β_{2}η_{1}; 1; β_{1}β_{2}η_{1}; 1; M′_{1}; ^{=^{1}^{c^{∗}}}; N_{11}; ^{=^{1}^{c^{∗}}}; …; ^{=^{1}^{c^{∗}}}; N_{1i}; …; β_{1}β_{2}η_{1}; 1; β_{1}β_{2}η_{1}; 1; ⋮; M′_{2}; ^{=^{1}^{c^{∗}}}; …; ^{=^{1}^{c^{∗}}}; N_{2j}; …; …; ⋮; ⋮; β_{1}β_{2}η_{1}; 1; β_{1}β_{2}η_{1}; 1; M′; =_{c^{∗}}; …; …; …; =_{c^{∗}}; N′]

9 The Genericity Theorem

Finally, in this section, we prove the Main Lemma that leads to the Genericity Theorem. We first need the following lemma:

Lemma 9.1 (η_{2}-postponement) If M ⟶_{F} M′ then there exists a term M′′ such that M ⟶_{β_{1}β_{2}η_{1}} M′′ ⟶_{η_{2}} M′.

Proof: Easy; see [BS93].

Lemma 9.2 (Main) Let Γ ⊢ M, N : σ. If [τ/X]M =_{F c} [τ/X]N for some type τ, then M =_{F c} N.

Proof: Observe first that the chain of Fc-equalities from [τ/X]M to [τ/X]N can be written:

[τ/X]M =_{F} M′′_{1} =_{c^{∗}} M′′_{2} =_{F} M′′_{3} =_{c^{∗}}  …  =_{F} M′′_{n−1} =_{c^{∗}} M′′_{n} =_{F} [τ/X]N

that is, as alternations of F-equalities and C^{∗}-equalities with the initial and final equalities being F-equalities. These initial or final F-equalities may be just trivial syntactic identities if, in fact, a C^{∗}-equality starts or ends the chain.

\underline{Case:} The chain consists entirely of F-equalities, i.e., [τ/X]M =_{F} [τ/X]N. Then, by Weak Genericity of F-equality (Theorem 7.2), we have the result M =_{F c} N.

\underline{Case:} The chain consists entirely of C^{∗}-equalities, i.e., [τ/X]M =_{c^{∗}} [τ/X]N. Then, by Weak Genericity of C^{∗}-equality (Theorem 7.3), M =_{F c} N.

\underline{Case:} There is at least one (non-trivial) C^{∗}-equality and one (non-trivial) F-equality. We proceed with a series of transformations on the chain, starting with the first three links:

[τ/X]M =_{F} M′′_{1} =_{c^{∗}} M′′_{2} =_{F} M′′_{3}

First, as a consequence of the equational Church-Rosser property for F, transform the F-equalities into reductions. Then, apply η_{2}-postponement (Lemma 9.1) to the reduction sequence from M′′_{1}. Thus, there exist terms M′_{1}, M′_{3}, N′_{1} such that:

[figure: [τ/X]M; F; M′′_{1} =_{c^{∗}} M′′_{2}; β_{1}β_{2}η_{1}; M′_{1}; η_{2}; N′_{1}; F; M′′_{3}; F; M′_{3}]

Then, by Commutativity of C^{∗}-equality with β_{1}β_{2}η_{1} reduction (Theorem 8.3), there exists M′_{2} such that

[figure: [τ/X]M; F; M′′_{1} =_{c^{∗}} M′′_{2}; β_{1}β_{2}η_{1}; M′_{1} =_{c^{∗}} M′_{2}; η_{2}; N′_{1}; β_{1}β_{2}η_{1}; F; M′′_{3}; F; M′_{3}]

The Church-Rosser property can then be used to complete the diamond between M′_{2} and M′_{3}:

[figure: [τ/X]M; F; M′′_{1} =_{c^{∗}} M′′_{2}; β_{1}β_{2}η_{1}; M′_{1} =_{c^{∗}} M′_{2}; η_{2}; N′_{1}; β_{1}β_{2}η_{1}; F; F; M′′_{3}; F; M′_{3}; F; N′_{3}]

In this way, the original path of Fc-equalities from [τ/X]M to M′′_{3} can be replaced by;

[figure: [τ/X]M; F; M′_{1} =_{c^{∗}} M′_{2}; η_{2}; N′_{1}; F; M′′_{3}; F; N′_{3}]

Now repeat this transformation down the rest of the chain by sets of three consecutive links of the form • =_{F} • =_{c^{∗}} • =_{F} • continuing with M′_{2} =_{F} M′′_{3} =_{c^{∗}} M′′_{4} =_{F} M′′_{5}. Note that the first link of each set coincides with the last link of the previously modified set. At the end, the transformed chain will look like:

[figure: [τ/X]M; F; M′_{1} =_{c^{∗}} M′_{2}; η_{2}; N′_{1}; F; …; M′_{n−1} =_{c^{∗}} M′_{n}; η_{2}; F; N′; [τ/X]N; F]

where each left-pointing arrow, except for the final one, consists of forward η_{2} reductions. The final left-pointing arrow, and all the right-pointing ones, consist of forward β_{1}β_{2}η_{1}η_{2} reductions.

Consider now the start of the transformed chain:

[figure: [τ/X]M; F; M′_{1} =_{c^{∗}} M′_{2}; η_{2}; N′_{1}]

— By Fact 6.2, there exists N_{1} such that N′_{1} ≡ [τ/X]N_{1} and M ⟶_{F} N_{1}.

— By Fact 6.3, there exists M_{1} such that M′_{1} ≡ [τ/X]M_{1} and N_{1} _{η_{2}}⟵ M_{1}.

— By Quasi-Genericity of C^{∗}-equality (Theorem 6.1), there exists M_{2} such that M′_{2} ≡ [τ/X]M_{2} and M_{1} =_{c^{∗}} M_{2}.

Thus, we have, for the first three links of the transformed chain,

[figure: [τ/X]M; F; [τ/X]M_{1} ≡ M′_{1} =_{c^{∗}} M′_{2} ≡ [τ/X]M_{2}; η_{2}; N′_{1} ≡ [τ/X]N_{1}]

with M ⟶_{F} N_{1} _{η_{2}}⟵ M_{1} =_{c^{∗}} M_{2}, i.e., M =_{F c} M_{2}.

Iterate then this process along the transformed chain from M′_{2} ≡ [τ/X]M_{2}, and thus “push” the type substitution [τ/X] along the chain. Finally, we end up with a term M_{n} such that M =_{F c} M_{n} and [τ/X]M_{n} ≡ M′_{n}.

Apply now Weak Genericity of F-equality (Theorem 7.2) to [τ/X]M_{n} ≡ M′_{n} =_{F} [τ/X]N. This gives M_{n} =_{F c} N. Since M =_{F c} M_{n}, then M =_{F c} N as required.

Theorem 9.3 (Genericity) Let Γ ⊢ M, N : ∀X.σ. If Mτ =_{F c} Nτ for some type τ, then M =_{F c} N.

Proof: Choose a fresh type variable Z.

Then, Γ ⊢ MZ, NZ : [Z/X]σ and [τ/Z](MZ) ≡ Mτ =_{F c} Nτ ≡ [τ/Z](NZ). Hence, by the Main Lemma (Lemma 9.2), MZ =_{F c} NZ. Observe that Z fresh implies Z not free in the type of any free term variable in MZ or NZ. So, by ∀-intro, λZ.MZ and λZ.NZ are well-typed terms. Hence, by ξ_{2}, λZ.MZ =_{F c} λZ.NZ, and, by η_{2}, M =_{F c} N.

10 Models

In this section we outline the validity of Axiom C in some relevant models. Details and further references about the model theory of system F may be found in [AL91] or [Hyl]. The reader may also see [LM91] for an introductory presentation of PER models and [GLT89] or [CGW88] for models based on coherent spaces or dI-domains. These constructions provide the main concrete paradigms for the general semantics of impredicative Type Theory and, by this, they allow a more explicit understanding of the semantic problems we will mention at the very end.

In short, in PER models, types are interpreted as partial equivalence relations on an arbitrary (partial) combinatory algebra (D, .), i.e., on a model of (partial) Combinatory Logic. That is, a type is a quotient of a subset of D modulo an equivalence relation. The terms of system F are interpreted as equivalence classes in these quotient sets. Given d ∈ D, call {d}_{A} the equivalence class of d in the p.e.r. A. Now, (D, .) yields a model of the type free λ-calculus (D, ., [[−]]), see [Bar84]. Set then er(M) for the term of system F with all types erased (e.g., er(λx: τ.Mρ) = λx.er(M)) and consider [[er(M)]]_{ξ}, i.e., the interpretation in D, under term environment ξ, of the type-free term er(M). A result in [Mit86] (see also [CL91]) shows that the meaning of an arbitrary term M of system F in the PER model, is given by the equivalence class of the meaning of its erasure, in the p.e.r. which interprets its type. More formally, if environment ξ′ is obtained from ξ by forgetting type information,

[[Γ ⊢ M : σ]]_{ξ} = {[[er(M)]]_{ξ′}}_{[[σ]]}

It is then clear that PER models realize Axiom C: if Mτ and Mτ′ live in the same type σ, then their meanings are identical as er(Mτ) = er(Mτ′). Note that in these few lines, we have omitted to mention the interpretation of type variables which may occur in types; indeed, and more generally, types are maps from (the objects of) PER to (the objects of) PER.

As for dI-based models, we only recall here that these may be constructed over the category of coherent spaces and stable maps, as in [Gir86], or over proper dI-domains as in [CGW88], which we follow. Types then are dI-domains or, more precisely, in view of possibly free type variables, they are maps over dI-domains. Indeed, they may be understood as functors if one considers the subcategory DI^{L} of dI-domains and just rigid embeddings as maps, as in [CGW88].^{2} (The impossibility of viewing types as functors, in general, was discussed in the introduction, in view of the the (contra-) and (co-)variance of the → functor.) In short, let F : DI^{L} → DI^{L} be a functor. Then ΠF, the product functor meant to interpret impredicative second order types, is simply the collection of “uniform families” (t_{X}), where X ranges over dI-domains, such that t_{X} ∈ F (X) and t_{X} = F (f)^{R}t_{Y} for any dI-domain Y and any morphism f from X to Y. Assume now that ∀X.σ is such that X is not free in σ. This means that σ is interpreted by a constant functor F, with respect to X. Then F (f)^{R} = F (f) = id always. In particular, take Y as the universal domain, i.e., any other may be rigidly embedded in it. Then, for any uniform family (t_{X}) and any X, one has t_{X} = t_{Y} in F (X). This is exactly the validity of Axiom C in these models.

There are several ways to describe the general (categorical) semantics of system F. In order to give a general meaning to Axiom C, we follow the presentation by internal categories given in [AL91]. First, though, the naïve, set-theoretic approach may guide our intuition. Let T p be the collection of semantic types. A variable type is then a function F : T p → T p. As usual, a product indexed over T p is given by the set

ΠF = {f : T p → ∪F | ∀X ∈ T p f(X) ∈ F (X)}

Then Axiom C corresponds to

if f ∈ ΠF and ∃A ∀B F (B) = A, then ∃a ∈ A ∀B f(B) = a

Or, also, ΠF and A are set-theoretically isomorphic, when F is constantly equal to A. We know though that classical Set Theory does not yield models of impredicative Type Theory. However, models may be found as categories which are internal not to the category of sets and functions, but to more “constructive” ones, which enjoy the fundamental adjunction (AD) below. Following [AL91], let c = (c_{0}, c_{1}) be an internal category to a Cartesian Closed Category E with all finite limits. Let c^{c_{0}} be the category of internal functors. Then (E, c) yields a model of system F if there exists the (internal) product functor Π : c^{c_{0}} → c as the right adjoint of the (internal) diagonal functor K : c → c^{c_{0}}, i.e., the functor that to each A associates the functor KA, which is constant A. In other words

2A rigid embedding is a projection with injection j and surjection j^{R}, which is the identity below the image of j.

(AD) c^{c_{0}}[K , ] ≅ c[ , Π ]

We claim that, among these models, exactly those which realize the following natural isomorphism

(Const) c^{c_{0}}[K , K ] ≅ c[ , ]

are models of Axiom C. Indeed, by (AD), (Const) implies, naturally in A, B,

c[B, Π(KA)] ≅ c^{c_{0}}[KB, KA] ≅ c[B, A]

This is equivalent, in these models, to the isomorphism Π(KA) ≅ A, i.e., to the intuitive set-theoretic meaning of Axiom C. A final remark: both the term model of system F, of course, and the “retraction” models (see [AL91]) do not realize Axiom C.

The hard part now comes with the semantics of the Genericity Theorem. Indeed,

(GEN) ∃τ Mτ = Nτ ⇒ M = N

is not an equation, but an implication between equations. Thus a model M of Fc does not need to realize it, in either of the two senses

(1) M ⊧ ∃τ Mτ = Nτ ⇒ M ⊧ M = N

or

(2) M ⊧ (∃τ Mτ = Nτ ⇒ M = N)

For example, over PER models or dI-domains, consider 0, K : ∀X.X → (X → X). Take then a type τ which has at most one element, for example, ∀X.X or ∀X.∀Y.X → (Y → X). Then in both classes of models Kτ = 0τ, but, of course, K ≠ 0. We have not yet found models of the “genericity” implication (GEN) in either form, in spite of the many models of Fc and the provability of the implication. Note that their semantic understanding is relevant, not only for “model-theoretic” reasons, but also for the extensions of system F which are relevant in practice. That is, actual polymorphic functional languages are based on extending core calculi by, possibly, more equation schemes. Since (GEN) is not preserved in equational varieties, the investigation of which equational theories realize it is a further theoretical challenge posed by the Genericity Theorem.

Acknowledgments

We are greatly indebted to Pierre-Louis Curien who pointed out a fundamental error in a preliminary version of this work, as well as the connection to Reynolds’s conditions. Thanks also to Jean Gallier for many passionate discussions about system F, to Eugenio Moggi and Roberto Di Cosmo for helpful comments and some early discussions on the Genericity Theorem, and to Simone Martini for valuable suggestions about this paper.

Giuseppe Longo’s work was partially supported by a collaboration at DEC PRL. Sergei Soloviev’s work was carried out at LIENS under a grant from the French Ministry for Research and Technology.

References

[ACC92] M. Abadi, L. Cardelli, P.-L. Curien. “Formal Parametric Polymorphism.” Proceedings of the 20th Symposium on Principles of Programming Languages, Charleston, January 1993.

[AL91] A. Asperti, G. Longo. Categories, Types, and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT Press, 1991.

[BFSS90] E.S. Bainbridge, P.J. Freyd, A. Scedrov, P.J. Scott. “Functorial Polymorphism.” Theoretical Computer Science 70, pages 35–64, January 1990. Corrigendum in 71, page 431, April 1990.

[Bar84] H.P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematics 103. North-Holland, 1984. Revised edition.

[BS93] H.P. Barendregt, R. Statman. Typed Lambda Calculus with Applications. In preparation.

[CL91] L. Cardelli, G. Longo. “A Semantic Basis for Quest.” Journal of Functional Programming 1, pages 417–458, April 1991.

[CMMS91] L. Cardelli, S. Martini, J.C. Mitchell, A. Scedrov. “An Extension of System F with Subtyping.” Proceedings of the Conference on Theoretical Aspects of Computer Software, Sendai, Japan, September 1991. Lecture Notes in Computer Science 526. Springer-Verlag. Edited by T. Ito and R. Meyer.

[CGL92] G. Castagna, G. Ghelli, G. Longo. “A Calculus for Overloaded Functions with Subtyping.” Proceedings of the Conference on LISP and Functional Programming, San Francisco, July 1992. Extended abstract.

[CGW88] T. Coquand, C.A. Gunter, G. Winskel. “DI-Domains as a Model of Polymorphism.” Proceedings of the 3rd Workshop on Mathematical Foundations of Programming Language Semantics, New Orleans, April 1987. Lecture Notes in Computer Science 298, pages 344–363. Springer-Verlag, 1988. Edited by M. Main, A. Melton, M. Mislove, and D. Schmidt.

[DL89] R. Di Cosmo, G. Longo. “Constructively Equivalent Propositions and Isomorphisms of Objects (or Terms as Natural Transformations).” Proceedings of the Workshop on Logic for Computer Science, Berkeley, November 1989. Mathematical Sciences Research Institute Publications 21. Springer-Verlag, 1992. Edited by Y.N. Moschovakis.

[EK66] S. Eilenberg, G.M. Kelly. “A Generalization of the Functorial Calculus.” Journal of Algebra 3, pages 366–375, 1966.

[FGSS88] P.J. Freyd, J.-Y. Girard, A. Scedrov, P.J. Scott. “Semantic Parametricity in Polymorphic Lambda-Calculus.” Proceedings of the 3rd Symposium on Logic in Computer Science, Edinburgh, Scotland, June 1988.

[Gir71] J.-Y. Girard. “Une Extension de l’Interpretation Fonctionelle de Gödel à l’Analyse et son Application à l’Elimination des Coupures dans l’Analyse et la Théorie des Types.” Proceedings of the 2nd Scandinavian Logic Symposium, pages 63–92. North-Holland, 1971. Edited by J.F. Fenstad.

[Gir86] J.-Y. Girard. “The System F of Variable Types, Fifteen Years Later.” Theoretical Computer Science 45, pages 159–192, 1986.

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

[GSS] J.-Y. Girard, A. Scedrov, P.J. Scott. “Normal Forms and Cut-Free Proofs as Natural Transformations.” Proceedings of the Workshop on Logic for Computer Science, Berkeley, November 1989. Mathematical Sciences Research Institute Publications 21, pages 217–241. Springer-Verlag, 1992. Edited by Y.N. Moschovakis.

[Hyl] M. Hyland. “A Small Complete Category.” Annals of Pure and Applied Logic 40, pages 135–165, 1988.

[LM91] G. Longo, E. Moggi. “Constructive Natural Deduction and its ω-set Interpretation.” Mathematical Structures in Computer Science 1 (2), pages 215–253, 1991.

[LS86] J. Lambek, P.J. Scott. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics 7. Cambridge University Press, 1986.

[Mac71] S. Mac Lane. Categories for the Working Mathematician. Springer-Verlag, 1971.

[MR91] Q. Ma, J.C. Reynolds. “Types, Abstraction, and Parametric Polymorphism: Part 2.” Proceedings of the Workshop on Mathematical Foundations of Programming Language Semantics, March 1991. Lecture Notes in Computer Science. Springer-Verlag, 1991. Edited by S. Brookes, M. Main, A. Melton, M. Mislove, and D. Schmidt.

[Mit86] J.C. Mitchell. “A Type Inference Approach to Reduction Properties and Semantics of Polymorphic Expressions.” Proceedings of the Conference on LISP and Functional Programming, 1986.

[Rey74] J.C. Reynolds. “Towards a Theory of Type Structure.” Proceedings of Colloque sur la Programmation. Lecture Notes in Computer Science 19, pages 408–425. Springer-Verlag, 1974. Edited by B. Robinet.

[Rey83] J.C. Reynolds. “Types, Abstraction and Parametric Polymorphism.” Information Processing 83, pages 513–523. North-Holland, 1983. Edited by R.E.A. Mason.

[Sco72] D. Scott. “Continuous lattices.” Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, pages 97–136. Springer-Verlag, 1972. Edited by F.W. Lawvere.

[SP82] M. Smyth, G. Plotkin. “The Category Theoretic Solution of Recursive Domain Equations.” SIAM Journal of Computing 11, pages 761–783, 1982.

[Str67] C. Strachey. “Fundamental concepts in programming languages.” Unpublished lecture notes from the International Summer School in Computer Programming, Copenhagen, August 1967.