This is a preprint of a paper that has been submitted to Information and Computation.

On Functors Expressible in the Polymorphic Typed Lambda Calculus

John C. Reynolds^{∗} Carnegie Mellon University and Gordon D. Plotkin^{†} University of Edinburgh

January 22, 1991

Abstract

Given a model of the polymorphic typed lambda calculus based upon a Cartesian closed category K, there will be functors from K to K whose action on objects can be expressed by type expressions and whose action on morphisms can be expressed by ordinary expressions. We show that if T is such a functor then there is a weak initial T -algebra and if, in addition, K possesses equalizers of all subsets of its morphism sets, then there is an initial T -algebra. These results are used to establish the impossibility of certain models, including those in which types denote sets and S → S′ denotes the set of all functions from S to S′.

∗Research supported by the Institut National de Recherche en Informatique et en Automatique, and by NSF Grants MCS-8017577, CCR-8620191, and CCR-8922109. The research was also supported in part by DARPA (DOD), monitored by the Avionics Laboratory, Air Force Wright Aeronautical Laboratories, Aeronautical Systems Division (AFSC), Wright-Patterson AFB, Ohio 45433-6543 under Contract F33615-87-C-1499, ARPA Order No. 4976, Amendment 20. The views and conclusions contained in this document are those of the authors and should not be interpreted as representing the official policies, either expressed or implied, of any agency of the US Government.

†Research supported by the British Petroleum Venture Research Group.

The polymorphic, or second-order, typed lambda calculus [11, 9, 30] is an extension of the typed lambda calculus in which polymorphic functions can be defined by abstraction on type variables, and such functions can be applied to type expressions. It is known that all expressions of this language are normalizable [11, 9], indeed strongly normalizable [27]. It is also known that the elements of any free many-sorted anarchic algebra are isomorphic to the closed normal expressions of a type that is determined by the signature of the algebra [17, 5]. (This result was anticipated in [33, Proposition 3.15.18].) These facts led to the conjecture in [31] that the polymorphic typed lambda calculus should possess a “set-theoretic” model in which types denote sets and S → S′ denotes the set of all functions from S to S′.

However, Reynolds [28] later showed that no such model exists. Shortly thereafter, Plotkin [26] generalized this proof by considering, for models based upon arbitrary Cartesian closed categories, the behavior of functors that can be defined in the calculus. In this joint paper, we give an exposition of this generalization, and show why it precludes the existence of several kinds of model.

The authors wish to thank one of the referees for a suggestion that led us to generalize the concept of a definable functor by permitting type variables to denote arbitrary objects. (What in previous versions of this paper were called “expressible” functors are functors definable from an empty list of objects.) This generalization has simplified our arguments and allowed us to strengthen our impossibility results.

1. Mathematical Preliminaries

When f is a function, we write dom f for the domain of f, f⌉S for the restriction of f to S ⊆ dom f, and fx (often without parentheses) for the application of f to an argument x. We assume that application is left-associative, so that fx y = (fx)y.

We write [ f | x: x′] to denote the function with domain dom f ∪{x} such that [ f | x: x′]y = if y = x then x′ else fy, and also [ x_{1}: y_{1} | … | x_{n}: y_{n}] (where the x_{i}’s are distinct) to denote the function with domain {x_{1},…, x_{n}} that maps each x_{i} into y_{i}. As a special case, [ ] denotes the empty function. We also write ⟨y_{1}, y_{2}⟩ for the pair [ 1: y_{1} | 2: y_{2} ].

When K is a category, we write |K| for the collection of objects of K, k ⟶_{K} k′ for the set of morphisms from k ^{∈} |K| to k′ ^{∈} |K|, α;_{K} α′ for the composition (in diagrammatic order) of α ^{∈} k ⟶_{K} k′ with α′ ^{∈} k′ ⟶_{K} k′′, and I_{k}^{K} for the identity morphism in k ⟶_{K} k. (In these and later notations, we will frequently elide subscripts or superscripts denoting categories or other entities that are evident from context.) We also write K^{op} for the dual of K.

Let F be a function from some (finite) set dom F to |K|. Then a (finite) product of F in K consists of an object ∏^{K}F and, for each v ^{∈} dom F, a morphism P^{K}[F, v] ^{∈} ∏^{K}F → F v, such that, if k ^{∈} |K| and Γ is a function with the same domain as F that maps each v ^{∈} dom F into a morphism in k → F v, then there is a unique morphism, denoted by ⟨Γ⟩^{K}, in k → ∏^{K} F such that

[figure: k; ∏^{K} F; F v; Γv; P^{K}[F, v]; ⟨Γ⟩^{K}]  (1)

commutes in K for all v ^{∈} dom F.

It is easily shown that, when Γv = P^{K}[F, v] for all v ^{∈} dom F,

⟨Γ⟩^{K} = I_{Π^{K} F}  (2)

and, when β ^{∈} k_{0} → k,

β ; ⟨Γ⟩^{K} = ⟨Γ′⟩^{K} ,  (3)

where Γ′ is the function with the same domain as Γ such that Γ′v = β; Γv for all v ^{∈} dom Γ.

We will frequently use the abbreviations

⟨ Γ | v: φ ⟩^{K} =^{def} ⟨[ Γ | v: φ]⟩^{K}

and

⟨ v_{1}: φ_{1} | … | v_{n}: φ_{n} ⟩^{K} =^{def} ⟨[ v_{1}: φ_{1} | … | v_{n}: φ_{n}]⟩^{K} .

Thus Equation 3 implies

β ; ⟨ v_{1}: φ_{1} | … | v_{n}: φ_{n} ⟩^{K} = ⟨ v_{1}: β ; φ_{1} | … | v_{n}: β ; φ_{n} ⟩^{K} .  (4)

An important special case of the product occurs when F is the empty function. Then its product in K is an object ∏^{K}[ ], called a terminal object, which we will denote more succinctly by ⊤^{K}. It has the property that, for each k ^{∈} |K|, the set k → ⊤^{K} contains exactly one member, namely ⟨⟩^{K}. (Note that k is determined by context.) The corresponding special case of Equation 4 is that, for β ^{∈} k_{0} → k,

β ; ⟨⟩^{K} = ⟨⟩^{K} .  (5)

Another important special case occurs when dom F = {1, 2}. Here we write k_{1} ×_{K} k_{2} for ∏^{K}[ 1: k_{1} | 2: k_{2} ], p_{k_{1}×k_{2}}^{i,K} for P^{K}[[ 1: k_{1} | 2: k_{2} ], i], and, when α_{1} ^{∈} k → k_{1} and α_{2} ^{∈} k → k_{2},

⟨α_{1}, α_{2}⟩^{K} for ⟨ 1: α_{1} | 2: α_{2} ⟩^{K}. The corresponding special cases of Equations 1, 2, and 4 are that, for α_{1} ^{∈} k → k_{1}, α_{2} ^{∈} k → k_{2}, and β ^{∈} k_{0} → k,

⟨α_{1}, α_{2}⟩; p_{k_{1}×k_{2}}^{i} = α_{i} ,  (6)
⟨p_{k_{1}×k_{2}}^{1}, p_{k_{1}×k_{2}}^{2}⟩ = I_{k_{1}×k_{2}} ,  (7)

β ; ⟨α_{1}, α_{2}⟩ = ⟨β ; α_{1}, β ; α_{2}⟩ .  (8)

For γ_{1} ^{∈} k_{1} → k′_{1}, and γ_{2} ^{∈} k_{2} → k′_{2}, we define the morphism

γ_{1} ×_{K} γ_{2} =^{def} ⟨(p_{k_{1}×k_{2}}^{1,K} ; γ_{1}), (p_{k_{1}×k_{2}}^{2,K} ; γ_{2})⟩^{K}

in k_{1} × k_{2} → k′_{1} × k′_{2}. (The use of × as an operation on both objects and morphisms reflects the fact that × is actually a bifunctor.) From Equations 8 and 6 it follows that, for α_{1} ^{∈} k → k_{1}, α_{2} ^{∈} k → k_{2}, γ_{1} ^{∈} k_{1} → k′_{1}, and γ_{2} ^{∈} k_{2} → k′_{2},

⟨α_{1}, α_{2}⟩; (γ_{1} × γ_{2}) = ⟨α_{1} ; γ_{1}, α_{2} ; γ_{2}⟩ .  (9)

Let K be a category with finite products, and k′, k′′ ^{∈} |K|. Then an exponentiation of k′′ by k′ consists of an object k′ ⟹_{K} k′′ and a morphism ap_{k′k′′}^{K} ^{∈} (k′ ⟹_{K} k′′) × k′ → k′′ such that, for each k ^{∈} |K| and ρ ^{∈} k × k′ → k′′, there is a unique morphism, denoted by ab^{K} ρ, in k → (k′ ⟹_{K} k′′) such that

[figure: k × k′; (k′ ⟹_{K} k′′) × k′; k′′; ρ; ap_{k′k′′}^{K}; ab^{K} ρ × I_{k′}]  (10)

commutes in K.

A category is said to be Cartesian closed if it possesses all finite products (including a terminal object) and all exponentiations. (For a given category, there may be several definitions of ∏, ⇒, and their associated morphisms that meet the definitions given above. However, when we speak of a category as Cartesian closed, we will assume that these entities have unambiguous meanings, i.e. that a Cartesian closed category is a category with distinguished finite products and exponentiations.)

For α ^{∈} k_{0} → (k′ ⇒ k′′) and α′ ^{∈} k_{0} → k′ we define

α >_{K} α′ =^{def} ⟨α, α′⟩^{K} ; ap_{k′k′′}^{K} .

From Equation 8, it follows that, for β ^{∈} k_{1} → k_{0},

β ; (α > α′) = β ; α > β ; α′ .  (11)

For ρ ^{∈} k × k′ → k′′, δ ^{∈} k_{0} → k, and θ ^{∈} k_{0} → k′, the definition of > and Equation 9 give

δ ; ab ρ > θ = ⟨δ, θ⟩; (ab ρ × I_{k′}) ; ap_{k′k′′} ,

so that Diagram 10 gives

δ ; ab ρ > θ = ⟨δ, θ⟩; ρ .  (12)

On the other hand, suppose 12 holds for all ρ ^{∈} k × k′ → k′′, δ ^{∈} k_{0} → k, and θ ^{∈} k_{0} → k′. Taking k_{0} = k × k′, δ = p_{k×k′}^{1}, and θ = p_{k×k′}^{2}, the definition of > and Equation 9 give

⟨p_{k×k′}^{1}, p_{k×k′}^{2}⟩; (ab ρ × I_{k′}) ; ap_{k′k′′} = ⟨p_{k×k′}^{1}, p_{k×k′}^{2}⟩; ρ ,

so that Equation 7 gives Diagram 10. Thus, for ρ ^{∈} k ×k′ → k′′, ab ρ is the unique morphism in k → (k′ ⇒ k′′) such that Equation 12 holds for all k_{0} ^{∈} |K|, δ ^{∈} k_{0} → k and θ ^{∈} k_{0} → k′.

In a category with a distinguished terminal object, a morphism in ⊤ → k is called a global element of k. When the category is Cartesian closed, there is an isomorphism between the global elements of k′ ⇒ k′′ and the morphisms in k′ → k′′. To see this, suppose α ^{∈} k′ → k′′ and take k = ⊤ and ρ = p_{⊤×k′}^{2} ; α in Diagram 10. Since ⟨⟨⟩, I_{k′}⟩ is an isomorphism from k′ to ⊤ × k′, we may add it to the beginning of the paths in Diagram 10 and still have a unique characterization of ab(p_{⊤×k′}^{2} ; α). Then, by Equations 9 and 6 and the definition of >, ab(p_{⊤×k′}^{2} ; α) is the unique solution of

⟨⟩; ab(p_{⊤×k′}^{2} ; α) > I_{k′} = α .

Thus, if we define the functions ϕ_{k′k′′}^{K} from ⊤ → (k′ ⇒ k′′) to k′ → k′′ and ψ_{k′k′′}^{K} from k′ → k′′ to ⊤ → (k′ ⇒ k′′) by

ϕ_{k′k′′}^{K}γ =^{def} ⟨⟩; γ > I_{k′} ,  (13)

and

ψ_{k′k′′}^{K}α =^{def} ab(p_{⊤×k′}^{2} ; α) ,

then

ϕ_{k′k′′}(ψ_{k′k′′}α) = α ,  (14)

and

ψ_{k′k′′}(ϕ_{k′k′′}γ) = γ .

For any object c of a Cartesian closed category K, there is a functor Q_{c}^{K} from K to K^{op} such that Q_{c}^{K}(k) = k ⟹_{K} c for all k ^{∈} |K|. A characterization of the action of Q_{c}^{K} on morphisms can be obtained from Equation 12 by replacing k by k′ ⇒ c, k′ by k, and k′′ by c, to find that, for ρ ^{∈} (k′ ⇒ c) × k → c, ab ρ is the unique morphism in (k′ ⇒ c) → (k ⇒ c) such that 12 holds for all k_{0} ^{∈} |K|, δ ^{∈} k_{0} → (k′ ⇒ c), and θ ^{∈} k_{0} → k. Next, for any α ^{∈} k → k′, take ρ = (I_{k′⇒c} × α) ; ap_{k′c}, so that ⟨δ, θ⟩; ρ = δ > θ ; α by Equation 9 and the definition of >, and define Q_{c}α to be ab ρ. Then Q_{c}α is the unique morphism in (k′ ⇒ c) → (k ⇒ c) such that

δ ; Q_{c}α > θ = δ > θ; α  (15)

holds for all k_{0} ^{∈} |K|, δ ^{∈} k_{0} → (k′ ⇒ c), and θ ^{∈} k_{0} → k.

It is immediately evident that Q_{c}I_{k} = I_{k⇒c}. To see that Q_{c} satisfies the composition law for functors, suppose α ^{∈} k → k′, α′ ^{∈} k′ → k′′, δ′ ^{∈} k_{0} → (k′′ ⇒ c), and θ ^{∈} k_{0} → k.

Substituting δ′ ; Q_{c}α′ for δ in Equation 15 and θ ; α for θ′ in the analogous equation with primed variables gives

δ′ ; Q_{c}α′ ; Q_{c}α > θ = δ′ ; Q_{c}α′ > θ; α = δ′ > θ; α; α′ ,

which establishes that Q_{c}(α; α′) = Q_{c}α′ ; Q_{c}α.

2. The Polymorphic Typed Lambda Calculus

The following syntactic description is somewhat unusual, since we wish to avoid assumptions that are stronger than necessary to obtain our results. In particular, we wish to encompass extensions of the polymorphic typed lambda calculus involving, for example, additional type and expression constructors.

We assume that the language is built from infinite sets T of type variables and V of ordinary variables. For each finite set N of type variables, there is a set Ω_{N} of type expressions over the type variables in N. These sets must satisfy:

1. If τ ^{∈} N then τ ^{∈} Ω_{N} ,

2. If ω, ω′ ^{∈} Ω_{N} then ω → ω′ ^{∈} Ω_{N} ,

3. If τ ^{∈} T and ω ^{∈} Ω_{N∪{τ}} then Δτ. ω ^{∈} Ω_{N} ,

4. If N ⊆ N′ then Ω_{N} ⊆ Ω_{N′} .

For example,

s ^{∈} Ω_{{s}} ⊆ Ω_{{s,t}} ,
s → t ^{∈} Ω_{{s,t}} ,
Δs. s → t ^{∈} Ω_{{t}} ⊆ Ω_{{s,t}} .

We will not need to make any assumptions about equality of type expressions (although it is usual to regard as equal type expressions that are alpha variants with respect to the binding structure induced by Δ).

A type assignment π over N is a function from some finite set dom π of ordinary variables to Ω_{N}; we write Ω_{N}^{∗} for the set of type assignments over N. For example,

[ x: s | f: s → t | p: Δs. s → t ] ^{∈} Ω_{{s,t}}^{∗} .

From Condition 4, we have

5. If N ⊆ N′ then Ω_{N}^{∗} ⊆ Ω_{N′}^{∗} .

Finally, we must define ordinary expressions. For each finite set N of type variables and finite set V of ordinary variables, there is a set E_{V}^{N} of ordinary expressions over the variables in N and V. These sets must satisfy:

6. If v ^{∈} V then v ^{∈} E_{V}^{N} ,

7. If e_{1}, e_{2} ^{∈} E_{V}^{N} then e_{1}e_{2} ^{∈} E_{V}^{N} ,

8. If v ^{∈} V, ω ^{∈} Ω_{N}, and e ^{∈} E_{V ∪{v}}^{N} then λv_{ω}. e ^{∈} E_{V}^{N} ,

9. If e ^{∈} E_{V}^{N} and ω ^{∈} Ω_{N} then e[ω] ^{∈} E_{V}^{N} ,

10. If τ ^{∈} T and e ^{∈} E_{V}^{N∪{τ}} then Λτ. e ^{∈} E_{V}^{N} ,

11. If N ⊆ N′ and V ⊆ V′ then E_{V}^{N} ⊆ E_{V′}^{N′} .

The relationship between ordinary and type expressions is expressed by formulas called typings. If π ^{∈} Ω_{N}^{∗}, ω ^{∈} Ω_{N}, and e is an ordinary expression then π ⊢_{N} e: ω is a typing that asserts that e belongs to E_{dom π}^{N} and takes on type ω when its free ordinary variables are assigned types by π. We assume that the following inference rules for typings are valid:

12. For π ^{∈} Ω_{N}^{∗} and v ^{∈} dom π:

\overline{π ⊢_{N} v: πv ,}

13. For π ^{∈} Ω_{N}^{∗} and ω, ω′ ^{∈} Ω_{N}:

π ⊢_{N} e_{1}: ω → ω′
π ⊢_{N} e_{2}: ω
π ⊢_{N} e_{1}e_{2}: ω′ ,

14. For π ^{∈} Ω_{N}^{∗} and ω, ω′ ^{∈} Ω_{N}:

[ π | v: ω] ⊢_{N} e: ω′
π ⊢_{N} λv_{ω}. e: ω → ω′ ,

15. For π ^{∈} Ω_{N}^{∗}, ω ^{∈} Ω_{N}, and τ ^{∈} N:

\frac{π ⊢_{N} e: Δτ. ω}{π ⊢_{N} e[τ]: ω ,}

16. For π ^{∈} Ω_{N−{τ}}^{∗} and ω ^{∈} Ω_{N∪{τ}}:

π ⊢_{N∪{τ}} e: ω
π ⊢_{N} Λτ. e: Δτ. ω ,

17. For N ⊆ N′, π ^{∈} Ω_{N}^{∗}, and ω ^{∈} Ω_{N}:

\frac{π ⊢_{N} e: ω}{π ⊢_{N′} e: ω ,}

18. For π, π′ ^{∈} Ω_{N}^{∗} such that π = π′⌉ dom π, and ω ^{∈} Ω_{N}:

\frac{π ⊢_{N} e: ω}{π′ ⊢_{N} e: ω .}

For example, the following are valid typings:

[ f: t → t | x: t ] ⊢_{{t}} f: t → t by 12 [ f: t → t | x: t ] ⊢_{{t}} x: t by 12 [ f: t → t | x: t ] ⊢_{{t}} f x: t by 13 [ f: t → t | x: t ] ⊢_{{t}} f(f x): t by 13 [ f: t → t ] ⊢_{{t}} λx_{t}. f(f x): t → t by 14 [ ] ⊢_{{t}} λf_{t→t}. λx_{t}. f(f x): (t → t) → (t → t) by 14 [ ] ⊢_{{}} Λt. λf_{t→t}. λx_{t}. f(f x): Δt. (t → t) → (t → t) by 16 [ ] ⊢_{{t}} Λt. λf_{t→t}. λx_{t}. f(f x): Δt. (t → t) → (t → t) by 17 [ ] ⊢_{{t}} (Λt. λf_{t→t}. λx_{t}. f(f x))[t]: (t → t) → (t → t) by 15 [ g: t → t ] ⊢_{{t}} (Λt. λf_{t→t}. λx_{t}. f(f x))[t]: (t → t) → (t → t) . by 18

Actually, for the ordinary polymorphic typed lambda calculus, Inference Rule 15 is subsumed by the more general rule

15′. For π ^{∈} Ω_{N}^{∗}, ω ^{∈} Ω_{N∪{τ}}, and ω′ ^{∈} Ω_{N}: π ⊢_{N} e: Δτ. ω

π ⊢_{N} e[ω′]: (ω/τ → ω′) ,

where (ω/τ → ω′) denotes the result of substituting ω′ for τ in ω. However, Rule 15 is sufficient for our needs, and we wish to avoid the difficulty of defining substitution (with renaming) in a way that would not circumscribe possible extensions of the language.

The notion of typing is prerequisite to any semantics of the polymorphic typed lambda calculus; ordinary expressions will possess meanings only when they satisfy typings, which will determine the kind of meanings they will possess. Specifically, for each π ^{∈} Ω_{N}^{∗} and ω ^{∈} Ω_{N}, the set

E_{πω}^{N} =^{def} { e | e ^{∈} E_{dom π}^{N} and π ⊢_{N} e: ω } ,

of expressions that take on type ω under the type assignment π, must be mapped into meanings appropriate to π and ω.

3. K-Models

It is well known that Cartesian closed categories provide models of the ordinary typed lambda calculus. In this section, we formalize the idea of extending such models to the polymorphic case. As with syntax, the properties that we postulate for such extensions are weaker than those one would normally require of a model; our intent is to assume only those properties needed to obtain the results of this paper.

(We believe that these properties hold for any general category-theoretic definition of the concept of a model. For example, given a PL category (G, S) in the sense of Seely [32], one can take K to be the Cartesian closed category G(1), where 1 is the terminal object of S.)

Given a category K, a function from a finite set of type variables to |K| is called an object assignment. Then, a K-model of the polymorphic typed lambda calculus consists of:

1. A Cartesian closed category K.

2. For each object assignment O with domain N, a semantic function MO from Ω_{N} to |K|. These functions must satisfy:

(a) If τ ^{∈} N then

MOτ = Oτ ,  (16)

(b) If ω, ω′ ^{∈} Ω_{N} then

MO(ω → ω′) = MOω ⟹_{K} MOω′ ,  (17)

(c) If O = O′⌉N and ω ^{∈} Ω_{N} then

MO′ω = MOω .  (18)

3. For each object assignment O with domain N, π ^{∈} Ω_{N}^{∗}, and ω ^{∈} Ω_{N}, a semantic function μ_{πω}^{O} from E_{πω}^{N} to ∏^{K}(MO · π) ⟶_{K} MOω, where MO · π denotes the function from dom π to |K| such that (MO · π)v = MO(πv) for all v ^{∈} dom π. These functions must satisfy:

(a) If π ^{∈} Ω_{N}^{∗} and v ^{∈} dom π then

μ_{π,πv}^{O}[[v]] = P[MO · π, v] ^{∈} ∏(MO · π) ⟶_{K} MO(πv) ,

(b) If π ^{∈} Ω_{N}^{∗}, ω, ω′ ^{∈} Ω_{N}, π ⊢_{N} e_{1}: ω → ω′, and π ⊢_{N} e_{2}: ω then

μ_{πω′}^{O}[[e_{1}e_{2}]] = μ_{π,ω→ω′}^{O}[[e_{1}]] > μ_{πω}^{O}[[e_{2}]] ^{∈} ∏(MO · π) ⟶_{K} MOω′ ,

(c) If π ^{∈} Ω_{N}^{∗}, ω, ω′ ^{∈} Ω_{N}, and [ π | v: ω] ⊢_{N} e: ω′ then

μ_{π,ω→ω′}^{O}[[λv_{ω}. e]] = ab(⟨ Ξ | v: p_{Π(MO·π)×MOω}^{2} ⟩; μ_{[π|v:ω],ω′}^{O}[[e]]) ,

where Ξ is the function with the same domain as π such that

Ξv′ = p_{Π(MO·π)×MOω}^{1} ; P[MO · π, v′]

for all v′ ^{∈} dom π; in other words, μ_{π,ω→ω′}^{O}[[λv_{ω}. e]] is the unique morphism in

∏(MO · π) ⟶_{K} (MOω ⇒ MOω′) such that

[figure: ∏(MO · π) × MOω; (MOω ⇒ MOω′) × MOω; ∏(MO · [ π | v: ω]); MOω′; μ^{O}[[e]]; ⟨ Ξ | v: p_{Π(MO·π)×MOω}^{2} ⟩; ^{ap^{MOω,MOω′}}; μ^{O}[[λv_{ω}. e]] × I_{MOω}]

commutes in K, where

[figure: ∏(MO · π) × MOω; ∏(MO · π); MO(πv′); Ξv′; P[MO · π, v′]; p_{Π(MO·π)×MOω}^{1}]

commutes for all v′ ^{∈} dom π.

(d) If O = O′⌉N, π ^{∈} Ω_{N}^{∗}, ω ^{∈} Ω_{N}, and π ⊢_{N} e: ω then

μ_{πω}^{O′}[[e]] = μ_{πω}^{O}[[e]] ,  (19)

(e) If π, π′ ^{∈} Ω_{N}^{∗}, π = π′⌉ dom π, ω ^{∈} Ω_{N}, and π ⊢_{N} e: ω then

μ_{π′ω}^{O}[[e]] = ⟨Υ⌉ dom π⟩; μ_{πω}^{O}[[e]] ,

where Υ is the function with the same domain as π′ such that

Υv′ = P[MO · π′, v′]

for all v′ ^{∈} dom π′,

(f) If π ^{∈} Ω_{N−{τ}}^{∗}, ω ^{∈} Ω_{N}, τ ^{∈} N, and π ⊢_{N} e: ω then

μ_{πω}^{O}[[(λv_{Δτ. ω}. v[τ])(Λτ. e)]] = μ_{πω}^{O}[[e]] .  (20)

Conditions 2a, 2b, 3a, 3b, and 3c stipulate that the semantics of the ordinary typed lambda calculus, which is a sublanguage of the polymorphic typed lambda calculus, is the standard semantics given by the Cartesian closed category K. Conditions 2c and 3d stipulate that the meanings of type and ordinary expressions are independent of irrelevant type variables, while Condition 3e stipulates that the meanings of ordinary expressions are independent of irrelevant ordinary variables. Condition 3f stipulates the soundness of the following combination of an ordinary and type beta-reduction:

(λv_{Δτ. ω}. v[τ])(Λτ. e) ⟹ (Λτ. e)[τ] ⟹ e .

Conditions 3a, 3b, 3c, and 3e can be recast in forms more suitable for analyzing the meanings of specific expressions. In the following, suppose Γ is a function with the same domain as π such that Γv ^{∈} k_{0} → MO(πv) for all v ^{∈} dom π, Γ′ bears a similar relation to π′, and φ ^{∈} k_{0} → MOω. If π ^{∈} Ω_{N}^{∗} and v ^{∈} dom π then Condition 3a and Equation 1 give

⟨Γ⟩; μ_{π,πv}^{O}[[v]] = Γv .  (21)

If π ^{∈} Ω_{N}^{∗}, ω, ω′ ^{∈} Ω_{N}, π ⊢_{N} e_{1}: ω → ω′, and π ⊢_{N} e_{2}: ω then 3b and 11 give

⟨Γ⟩; μ_{πω′}^{O}[[e_{1}e_{2}]] = ⟨Γ⟩; μ_{π,ω→ω′}^{O}[[e_{1}]] > ⟨Γ⟩; μ_{πω}^{O}[[e_{2}]] .  (22)

If π ^{∈} Ω_{N}^{∗}, ω, ω′ ^{∈} Ω_{N}, and [ π | v: ω] ⊢_{N} e: ω′ then 3c, 12, 3, 6, and 1 give

⟨Γ⟩; μ_{π,ω→ω′}^{O}[[λv_{ω}. e]] > φ = ⟨ Γ | v: φ ⟩; μ_{[π|v:ω],ω′}^{O}[[e]] .  (23)

If π, π′ ^{∈} Ω_{N}^{∗}, π = π′⌉ dom π, ω ^{∈} Ω_{N}, and π ⊢_{N} e: ω then 3e, 3, and 1 give

⟨Γ′⟩; μ_{π′ω}^{O}[[e]] = ⟨Γ′⌉ dom π⟩; μ_{πω}^{O}[[e]] .  (24)

4. SET-Models

An important special case of a K-model arises when K is the Cartesian closed category SET, for which:

1. |SET| is the class of sets, and

(a) k ⟶_{SET} k′ is the set of all functions from k to k′,

(b) Composition is functional composition,

(c) I_{k}^{SET} is the identity function on k.

2. ∏^{SET} is the general Cartesian product, and

(a) If v ^{∈} dom F then P[F, v] ^{∈} ∏ F → F v is the function such that

P[F, v]η = ηv

for all η ^{∈} ∏ F,

(b) If, for all v ^{∈} dom F, Γv ^{∈} k → F v, then ⟨Γ⟩ ^{∈} k → ∏ F is the function such that

⟨Γ⟩x v = Γvx

for all x ^{∈} k and v ^{∈} dom F.

3. ×_{SET} is the binary Cartesian product, and

(a) p_{k_{1}×k_{2}}^{i} ^{∈} k_{1} × k_{2} → k_{i} is the function such that

p_{k_{1}×k_{2}}^{i}⟨x_{1}, x_{2}⟩ = x_{i}

for all x_{1} ^{∈} k_{1} and x_{2} ^{∈} k_{2},

(b) If α_{1} ^{∈} k → k_{1} and α_{2} ^{∈} k → k_{2} then ⟨α_{1}, α_{2}⟩^{SET} ^{∈} k → k_{1} × k_{2} is the function

such that

⟨α_{1}, α_{2}⟩^{SET}x = ⟨α_{1}x, α_{2}x⟩

for all x ^{∈} k.

4. k′ ⟹_{SET} k′′ is the set k′ → k′′, and

(a) ap_{k′k′′} ^{∈} (k′ → k′′) × k′ → k′′ is the function such that

ap_{k′k′′}⟨f′, x′⟩ = f′x′

for all f′ ^{∈} k′ → k′′ and x′ ^{∈} k′,

(b) If ρ ^{∈} k × k′ → k′′ then ab ρ ^{∈} k → (k′ → k′′) is the function such that

ab ρ x x′ = ρ⟨x, x′⟩

for all x ^{∈} k and x′ ^{∈} k′.

5. Q_{c}^{SET} is the functor from SET to SET^{op} such that

(a) If k is a set then

Q_{c}k = k ⇒ c = k → c ,

(b) If α ^{∈} k → k′ and β ^{∈} k′ → c then (Q_{c}α)β = α; β .

By substituting these equations into the general definition of a K-model, we find that a SET-model consists of:

1. The Cartesian closed category SET.

2. For each set assignment O with domain N, a semantic function MO from Ω_{N} to |SET|, such that:

(a) If τ ^{∈} N then

MOτ = Oτ ,

(b) If ω, ω′ ^{∈} Ω_{N} then

MO(ω → ω′) = MOω → MOω′ ,

(c) If O = O′⌉N and ω ^{∈} Ω_{N} then

MO′ω = MOω .

3. For each set assignment O with domain N, π ^{∈} Ω_{N}^{∗}, and ω ^{∈} Ω_{N}, a semantic function μ_{πω}^{O} from E_{πω}^{N} to ∏^{SET}(MO · π) → MOω, such that

(a) If π ^{∈} Ω_{N}^{∗} and v ^{∈} dom π then, for all η ^{∈} ∏(MO · π),

μ_{π,πv}^{O}[[v]]η = ηv ,

(b) If π ^{∈} Ω_{N}^{∗}, ω, ω′ ^{∈} Ω_{N}, π ⊢_{N} e_{1}: ω → ω′, and π ⊢_{N} e_{2}: ω then, for all η ^{∈}

∏(MO · π),

μ_{πω′}^{O}[[e_{1}e_{2}]]η = (μ_{π,ω→ω′}^{O}[[e_{1}]]η)(μ_{πω}^{O}[[e_{2}]]η) ,

(c) If π ^{∈} Ω_{N}^{∗}, ω, ω′ ^{∈} Ω_{N}, and [ π | v: ω] ⊢_{N} e: ω′ then, for all η ^{∈} ∏(MO · π) and

a ^{∈} MOω,

μ_{π,ω→ω′}^{O}[[λv_{ω}. e]]ηa = μ_{[π|v:ω],ω′}^{O}[[e]][ η | v: a] ,

(d) If O = O′⌉N, π ^{∈} Ω_{N}^{∗}, ω ^{∈} Ω_{N}, and π ⊢_{N} e: ω then

μ_{πω}^{O′}[[e]] = μ_{πω}^{O}[[e]] ,

(e) If π, π′ ^{∈} Ω_{N}^{∗}, π = π′⌉ dom π, ω ^{∈} Ω_{N}, and π ⊢_{N} e: ω then, for all η′ ^{∈} ∏(MO · π′),

μ_{π′ω}^{O}[[e]]η′ = μ_{πω}^{O}[[e]](η′⌉ dom π) ,

(f) If π ^{∈} Ω_{N−{τ}}^{∗}, ω ^{∈} Ω_{N}, τ ^{∈} N, and π ⊢_{N} e: ω then

μ_{πω}^{O}[[(λv_{Δτ. ω}. v[τ])(Λτ. e)]] = μ_{πω}^{O}[[e]] .

Note that 2a, 2b, 3a, 3b, and 3c stipulate the “classical” set-theoretic semantics of the ordinary typed lambda calculus.

5. POS- and DCPO-Models

We will also be interested in K-models where K is either POS, the category of posets and monotone functions, or DCPO, the category of directed-complete posets and continuous functions, or various full sub-ccc’s of these categories. (A sub-ccc of a Cartesian closed category is a Cartesian closed subcategory with the same finite product and exponentiation operations.)

A directed-complete poset (called a predomain in [29]) is a poset with least upper bounds of all directed subsets, and a continuous function is one that preserves all such least upper bounds. (Our results will also hold for the weaker definition of these concepts in which “directed subsets” is replaced by “ω-chains”.) Note that a directed-complete poset need not contain a least element. Indeed, if we regard a set as a discretely ordered poset, then every set is a directed-complete poset, every function between sets is continuous, and SET is a full sub-ccc of DCPO, as well as of POS.

Only slight modifications of the previous section are needed to describe models based on POS (DCPO) or a full sub-ccc thereof. The morphism sets k → k′ become the sets of monotone (continuous) functions, and products and exponentiations are equipped with pointwise orderings. Thus k ⇒ k′, Q_{c}k, and MO(ω → ω′) all denote pointwise ordered posets of monotone (continuous) functions.

For any of these categories, the functor Q_{c} has several significant properties. If c is discretely ordered then Q_{c}k is discretely ordered for any object k. If c has a least element then Q_{c}k has a least element for any k and Q_{c}α is strict (least-element preserving) for any α ^{∈} k → k′.

6. Definable Functors

Let T be a functor from K to K, and c_{1},…, c_{n} be objects of K. Roughly speaking, we say that T is definable from c_{1},…, c_{n} in a K-model when its action on objects can be expressed by type expressions and its action on morphisms can be expressed by ordinary expressions, using type variables to denote the objects c_{1},…, c_{n}. To define this concept precisely, suppose c_{1},…, c_{n} is an arbitrary but fixed list of n distinct type variables. Then T is definable from c_{1},…, c_{n} in a K-model if and only if both:

1. For any type expression ω there is a type expression T[ω] such that, whenever N is a finite set of type variables satisfying c_{1},…, c_{n} ^{∈} N and ω ^{∈} Ω_{N},

(a) T[ω] ^{∈} Ω_{N} ,

(b) For all object assignments O with domain N satisfying Oc_{i} = c_{i} whenever 1 ≤

i ≤ n,

MO(T[ω]) = T (MOω) .  (25)

2. For any type expressions ω, ω′ and ordinary expression e there is an ordinary expression T_{ωω′}[e] such that, whenever N is a finite set of type variables and π is a type assignment satisfying c_{1},…, c_{n} ^{∈} N, ω, ω′ ^{∈} Ω_{N}, π ^{∈} Ω_{N}^{∗}, and π ⊢_{N} e: ω → ω′,

(a) π ⊢_{N} T_{ωω′}[e]: T[ω] → T[ω′] ,

(b) For all object assignments O with domain N satisfying Oc_{i} = c_{i} whenever 1 ≤ i ≤ n, and all global elements η of ∏(MO · π),

ϕ(η ; μ^{O}[[T_{ωω′}[e]]]) = T (ϕ(η ; μ^{O}[[e]])) ,  (26)

where ϕ is the isomorphism defined by Equation 13.

Trivially, the identity functor can be defined from the empty list of objects by T[ω] = ω and T_{ωω′}[e] = e. A family of less trivial definable functors is provided by the following proposition:

Proposition 1 For any K-model and any object c ^{∈} |K|, the functor Q_{c} ; Q_{c} is definable from c.

Proof : Our main task is to show that, roughly speaking (since it is a functor from K to K^{op} rather than K to K), Q_{c} is definable from c. Using the type variable c to denote the object c, let

Q[ω] =^{def} ω → c .

If c ^{∈} N and ω ^{∈} Ω_{N} then Q[ω] ^{∈} Ω_{N} and, for any object assignment O with domain N satisfying Oc = c,

MO(Q[ω]) = MOω ⇒ MOc = MOω ⇒ c = Q_{c}(MOω) .  (27)

Next, let

Q_{ωω′}[e] =^{def} (λf_{ω→ω′}. λg_{ω′→c}. λx_{ω}. g(f x))e .

When c ^{∈} N, ω, ω′ ^{∈} Ω_{N}, π ^{∈} Ω_{N}^{∗}, and π ⊢_{N} e: ω → ω′, we have π ⊢_{N} Q_{ωω′}[e]: Q[ω′] → Q[ω]. Moreover, suppose O is an object assignment with domain N satisfying Oc = c, and η is a global element of ∏(MO · π). Then, for all k_{0} ^{∈} |K|, δ ^{∈} k_{0} → (MOω′ ⇒ c), and θ ^{∈} k_{0} → MOω,

δ ; ϕ(η ; μ^{O}[[Q_{ωω′}[e]]]) > θ

= (⟨⟩; η ; μ^{O}[[Q_{ωω′}[e]]] > δ) > θ by 13, 11, 5

= ((⟨⟩; μ^{O}[[λf_{ω→ω′}. λg_{ω′→c}. λx_{ω}. g(f x)]] > ⟨⟩; η ; μ^{O}[[e]]) > δ) > θ by 22, 24

= ⟨ f: ⟨⟩; η ; μ^{O}[[e]] | g: δ | x: θ ⟩; μ^{O}[[g(f x)]] by 23

= δ > (⟨⟩; η ; μ^{O}[[e]] > θ) by 22, 21

= δ > θ; ϕ(η ; μ^{O}[[e]]) . by 5, 11, 13 Thus, by the uniqueness property of Equation 15,

ϕ(η ; μ^{O}[[Q_{ωω′}[e]]]) = Q_{c}(ϕ(η ; μ^{O}[[e]])) .  (28)

Finally, let

T[ω] =^{def} Q[Q[ω]] ,

and

T_{ωω′}[e] =^{def} Q_{Q[ω′],Q[ω]}[Q_{ωω′}[e]] .

Using Equations 27 and 28, it is easily seen that Q_{c} ; Q_{c} is defined from c by T[ω] and T_{ωω′}[e]. (End of Proof )

We can now establish our main result about definable functors:

Proposition 2 Suppose T is a functor from K to K that is definable from c_{1},…, c_{n} in a K-model. Then there is an object P ^{∈} |K| and a morphism H ^{∈} T P → P such that, for all k ^{∈} |K| and α ^{∈} T k → k, there is a morphism M ^{∈} P → k making the diagram

[figure: T P; T k; P; k; T M; M; H; α]

commute in K.

Proof : Let c_{1},…, c_{n}, and k be distinct type variables, N = {c_{1},…, c_{n}}, and O = [ c_{1}: c_{1} | … | c_{n}: c_{n}]. Then let

P =^{def} Δk. (T[k] → k) → k ,
M =^{def} λp_{P}. p[k]f ,
H =^{def} λq_{T[P]}. Λk. λf_{T[k]→k}. f(T_{Pk}[M]q) ,

so that

P ^{∈} Ω_{N} ,
[ f: T[k] → k ] ⊢_{N∪{k}} M: P → k ,
[ ] ⊢_{N} H: T[P] → P .

Intuitively, our proof is based on the fact that the diagram commutes syntactically, i.e. by expressing composition as usual in the lambda calculus, and using beta reduction and type beta reduction. To formalize this intuition, we must work through the semantics of the expressions in this diagram.

[figure: T[P]; T[k]; P; k; T_{Pk}[M]; M; H; f]

Let P =^{def} MOP. Since μ^{O}[[H]] is a global element of MO(T[P] → P) and, by Equations 17 and 25, MO(T[P] → P) = T P ⇒ P, we may define

H =^{def} ϕ(μ^{O}[[H]]) ^{∈} T P → P .  (29)

Then, for any k ^{∈} |K| and α ^{∈} T k → k, by Equations 17, 25, and 16,

ψα ^{∈} ⊤ → (T k ⇒ k) = ⊤ → M[ O | k: k](T[k] → k) ,

so that

⟨ f: ψα ⟩; μ^{[O|k:k]}[[M]] ^{∈} ⊤ → M[ O | k: k](P → k) ,

and by Equations 17, 18, and 16, M[ O | k: k](P → k) = P ⇒ k, so that we may define

M =^{def} ϕ(⟨ f: ψα ⟩; μ^{[O|k:k]}[[M]]) ^{∈} P → k .  (30)

Finally, we must show that the diagram given in the proposition commutes, i.e. that H ; M = T M ; α. We have

H ; M = H ; (⟨⟩; ⟨ f: ψα ⟩; μ^{[O|k:k]}[[M]] > I_{P} ) by 30, 13 = ⟨ f: ⟨⟩; ψα ⟩; μ^{[O|k:k]}[[M]] > H by 11, 5, 4 = ⟨ f: ⟨⟩; ψα | p: H ⟩; μ^{[O|k:k]}[[p[k]f]] by 23 = ⟨ p: H ⟩; μ^{[O|k:k]}[[p[k]]] > ⟨⟩; ψα by 22, 24, 21 = (⟨⟩; μ^{[O|k:k]}[[λp_{P}. p[k]]] > H) > ⟨⟩; ψα by 23 = (⟨⟩; μ^{[O|k:k]}[[λp_{P}. p[k]]] > ⟨ q: I_{T P} ⟩; μ^{O}[[Λk. λf_{T[k]→k}. f(T_{Pk}[M]q)]]) > ⟨⟩; ψα

by 29, 13, 23

= ⟨ q: I_{T P} ⟩; μ^{[O|k:k]}[[(λp_{P}. p[k])(Λk. λf_{T[k]→k}. f(T_{Pk}[M]q))]] > ⟨⟩; ψα by 24, 19, 22 = ⟨ q: I_{T P} ⟩; μ^{[O|k:k]}[[λf_{T[k]→k}. f(T_{Pk}[M]q)]] > ⟨⟩; ψα by 20 = ⟨⟩; ψα > ⟨ q: I_{T P} | f: ⟨⟩; ψα ⟩; μ^{[O|k:k]}[[T_{Pk}[M]q]] by 23, 22, 21 = ⟨ q: I_{T P} | f: ⟨⟩; ψα ⟩; μ^{[O|k:k]}[[T_{Pk}[M]q]] ; (⟨⟩; ψα > I_{T k}) by 11, 5 = ⟨ q: I_{T P} | f: ⟨⟩; ψα ⟩; μ^{[O|k:k]}[[T_{Pk}[M]q]] ; α by 13, 14 = (⟨ f: ⟨⟩; ψα ⟩; μ^{[O|k:k]}[[T_{Pk}[M]]] > I_{T P} ); α by 22, 24, 21

= ϕ(⟨ f: ψα ⟩; μ^{[O|k:k]}[[T_{Pk}[M]]]); α by 4, 13

= T (ϕ(⟨ f: ψα ⟩; μ^{[O|k:k]}[[M]])); α by 26

= T M ; α . by 30

(End of Proof )

7. T -algebras

Our result about definable functors can be stated more succinctly by introducing the concepts of T -algebras and weak initiality.

If K is a category and T is a functor from K to K, then T alg is the category such that

|T alg| =^{def} { ⟨k, α⟩ | k ^{∈} |K| and α ^{∈} T k ⟶_{K} k } ,

⟨k, α⟩ ⟶_{Talg} ⟨k′, α′⟩ =^{def} { β | β ^{∈} k ⟶_{K} k′ and T β ;_{K} α′ = α;_{K} β } ,

β ;_{Talg} β′ =^{def} β ;_{K} β′ ,

I_{⟨k,α⟩}^{Talg} =^{def} I_{k}^{K} .

The objects of T alg are called T -algebras, and the morphisms in ⟨k, α⟩ ⟶_{Talg} ⟨k′, α′⟩ are called homomorphisms from ⟨k, α⟩ to ⟨k′, α′⟩.

An initial (weak initial) object of a category K is an object v ^{∈} |K| such that, for all k ^{∈} |K|, the set v → k contains exactly one (at least one) morphism.

Then Proposition 2 can be restated as:

Proposition 3 If a functor T from K to K is definable from c_{1},…, c_{n} in a K-model then there is a weak initial T -algebra.

A further property of T -algebras is given by:

Proposition 4 Suppose T is a functor from K to K that maps the objects and morphisms of K into objects and morphisms of some subcategory K′ of K. Let T′ be the restriction of T to a functor from K′ to K′. If there is a weak initial T -algebra then there is a weak initial T′-algebra.

Proof : Suppose ⟨u, θ⟩ is a weak initial T -algebra and ⟨k, α⟩ is any T′-algebra. Then ⟨k, α⟩ is also a T -algebra, so that there is a morphism β from ⟨u, θ⟩ to ⟨k, α⟩. By applying T to the commuting diagram satisfied by β, and adding a trivially commuting diagram on the right, we find that

[figure: T (T u); T (T k); T k; T u; T k; k; T (T β); T α; T β; α; T θ; T α; α]

commutes in K. But in fact this diagram lies entirely within K′. Thus ⟨T u, T θ⟩ is a weak initial T′-algebra. (End of Proof )

8. Equalizers and Initiality

Our next goal is to find circumstances in which definable functors will lead to initial, rather than just weak initial, T -algebras. We will find that a sufficient condition is the existence of enough equalizers.

Suppose K is any category, k, k′ ^{∈} |K|, and S ⊆ k → k′. If u ^{∈} |K| and ε ^{∈} u → k are such that

[figure: u; k; k′; ε; β_{1}; β_{2}]

commutes for all β_{1}, β_{2} ^{∈} S, then ε is said to be an equalizing cone of S. If ε ^{∈} u → k is an equalizing cone of S and, for all equalizing cones ε′ ^{∈} u′ → k of S, there is exactly one morphism θ ^{∈} u′ → u such that

[figure: u′; u; k; ε′; ε; θ]

commutes, then ε is said to be an equalizer of S.

In the particular case where K is SET, it is easily seen that an equalizer of S is obtained by taking ε to be the identity injection from u to k, where

u = { x | x ^{∈} k and (∀β_{1}, β_{2} ^{∈} S) β_{1}x = β_{2}x } .

Thus SET possesses equalizers of all subsets of its morphism sets.

For any category K, suppose ε ^{∈} u → k is an equalizer of some S ⊆ k → k′, and ϕ, ψ ^{∈} u′ → u. Then ϕ; ε and ψ; ε are both equalizing cones of S. Thus, if ϕ; ε = ψ; ε then the commutativity of

[figure: u′; u; k; ϕ; ε = ψ ; ε; ε; ϕ; ψ]

implies ϕ = ψ. In other words, equalizers are right-cancellable or monic.

The connection between equalizers and initiality is established by the following proposition, which is a slight variation of Theorem V.6.1 in [19]:

Proposition 5 In a category with a weak initial object w, there is an initial object v if and only if both:

1. w → w has an equalizer,

2. Every pair of morphisms with the same domain and the same codomain has an equalizing cone.

Proof : Suppose Conditions (1) and (2) hold, and let ε ^{∈} v → w be the equalizer of w → w. For every object k, since w is weakly initial, there is a morphism ϕ ^{∈} w → k, so that ε ; ϕ ^{∈} v → k; thus v is also weakly initial. To see that it is actually initial, suppose β_{1}, β_{2} ^{∈} v → k. Let ε′ ^{∈} u → v be an equalizing cone of {β_{1}, β_{2}}, and let ρ be some morphism in w → u, whose existence is insured by the weak initiality of w. Then

[figure: v; w; u; v; k; ε; ρ; ε′; β_{1}; β_{2}]

commutes, since ε′ is an equalizing cone. But

[figure: v; w; w; ε; ρ; ε′ ; ε; I_{w}]

also commutes, since ε equalizes w → w. Moreover, since ε is monic, ε; ρ; ε′ ; ε = ε implies ε; ρ; ε′ = I_{v}. Thus

β_{1} = ε; ρ; ε′ ; β_{1} = ε; ρ; ε′ ; β_{2} = β_{2} .

On the other hand, suppose v is initial, with unique morphisms ε_{k} ^{∈} v → k for each object k. Then, for any β_{1}, β_{2} ^{∈} k → k′, ε_{k} is an equalizing cone of {β_{1}, β_{2}}, since initiality gives ε_{k} ; β_{1} = ε_{k′} = ε_{k} ; β_{2}.

Moreover, if w is weakly initial then ε_{w} is an equalizer of w → w. To see this, suppose ε′ ^{∈} v′ → w is an equalizing cone of w → w, and let ρ be some morphism in w → v, whose existence is guaranteed by the weak initiality of w. Then ρ ; ε_{w} ^{∈} w → w, so that ε′ ; ρ; ε_{w} = ε′ ; I_{w} since ε′ is an equalizing cone. Thus taking θ = ε′ ; ρ makes

[figure: v′; v; w; ε′; ε_{w}; θ]

commute. On the other hand, the initiality of v gives I_{v} = ε_{w}; ρ. Thus, if θ is any morphism making the above diagram commute, then θ = θ; ε_{w} ; ρ = ε′ ; ρ. (End of Proof )

Next, to apply the above proposition to the existence of initial T -algebras, we must relate equalizers in T alg to equalizers in the underlying category K. The following proposition is a special case of Theorem 3.4.1 in [4]:

Proposition 6 Suppose T is a functor from K to K and, for some T -algebras ⟨k, α⟩ and ⟨k′, α′⟩,

S ⊆ ⟨k, α⟩ ⟶_{Talg} ⟨k′, α′⟩ ⊆ k ⟶_{K} k′ .

If S has an equalizer in K then S has an equalizer in T alg.

Proof : Let ε ^{∈} u → k be the equalizer of S in K. For any β_{1}, β_{2} ^{∈} S, consider the diagram

[figure: T u; T k; T k′; u; k; k′; T ε; ε; T β_{1}; T β_{2}; β_{1}; β_{2}; α; α′]

in K. Since ε is an equalizer, ε; β_{1} = ε; β_{2}, and since T is a functor, T ε; T β_{1} = T ε; T β_{2}. Then, since β_{1} and β_{2} are morphisms of T -algebras,

T ε; α; β_{1} = T ε; T β_{1} ; α′ = T ε; T β_{2} ; α′ = T ε; α; β_{2} .

Thus T ε; α is an equalizing cone of S in K, so that there is a unique θ ^{∈} T u → u such that

[figure: T u; T k; u; k; T ε; ε; θ; α]

commutes. This implies that ε ^{∈} ⟨u, θ⟩ ⟶_{Talg} ⟨k, α⟩. Moreover, for any β_{1}, β_{2} ^{∈} S, since composition is the same in T alg as in K, we have ε;_{Talg}β_{1} = ε;_{Talg}β_{2}. Thus ε is an equalizing cone of S in T alg.

Now suppose ε′ ^{∈} ⟨u′, θ′⟩ ⟶_{Talg} ⟨k, α⟩ is any equalizing cone of S in T alg. Since composition is the same in T alg as in K, ε′ is also an equalizing cone of S in K, so that there is a unique σ such that

[figure: u′; u; k; ε′; σ; ε]

commutes in K. Then σ will also be the unique morphism such that

[figure: ⟨u′, θ′⟩; ⟨u, θ⟩; ⟨k, α⟩; ε′; σ; ε]

commutes in T alg, providing it is a morphism of T -algebras.

To see that σ ^{∈} ⟨u′, θ′⟩ ⟶_{Talg} ⟨u, θ⟩, consider the diagram

[figure: T u′; T u; T k; u′; u; k; T ε′; T σ; T ε; ε′; σ; ε; θ′; θ; α]

in K. The lower triangle commutes since ε is an equalizer and ε′ is an equalizing cone, and the upper triangle then commutes since T is a functor. The square commutes since ε ^{∈} ⟨u, θ⟩ ⟶_{Talg} ⟨k, α⟩, and the rear parallelogram commutes since ε′ ^{∈} ⟨u′, θ′⟩ ⟶_{Talg} ⟨k, α⟩. Thus

T σ ; θ; ε = T σ ; T ε; α = T ε′ ; α = θ′ ; ε′ = θ′ ; σ ; ε ,

and since ε is monic, T σ ; θ = θ′ ; σ. Thus σ ^{∈} ⟨u′, θ′⟩ ⟶_{Talg} ⟨u, θ⟩. (End of Proof )

From Propositions 5 and 6, it follows that:

Proposition 7 If T is a functor from K to K, all subsets of the morphism sets of K have equalizers, and there is a weak initial T -algebra, then there is an initial T -algebra.

9. Initial T -algebras and Isomorphisms

To complete our development, we use the fact that the morphism parts of initial T -algebras are isomorphisms. The following proposition is given in [3], where it is attributed to J. Lambek:

Proposition 8 If ⟨u, θ⟩ is an initial T -algebra, then θ is an isomorphism from T u to u in K.

Proof : From the obviously commuting diagram

[figure: T (T u); T u; T u; u; T θ; θ; T θ; θ]

it is evident that ⟨T u, T θ⟩ is a T -algebra and θ ^{∈} ⟨T u, T θ⟩ ⟶_{Talg} ⟨u, θ⟩. Let η be the unique morphism in ⟨u, θ⟩ ⟶_{Talg} ⟨T u, T θ⟩. Then η ; θ and I_{u} are both morphisms belonging to ⟨u, θ⟩ ⟶_{Talg} ⟨u, θ⟩, so that the initiality of ⟨u, θ⟩ gives η ; θ = I_{u}. Moreover, since η ^{∈} ⟨u, θ⟩ ⟶_{Talg} ⟨T u, T θ⟩ and T is a functor,

θ; η = T η ; T θ = T (η ; θ) = T (I_{u}) = I_{T u} .

(End of Proof )

10. Impossible Models

We can now combine our results to show the impossibility of models based on certain Cartesian closed categories.

Proposition 9 Suppose K and K′ are Cartesian closed categories such that K′ is a sub-ccc of both K and SET, there is an object c of K′ that contains more than one member, all objects and morphisms in the range of the functor Q_{c}^{K} belong to K′, and all subsets of the morphism sets of K′ have equalizers. Then there is no K-model.

Proof : Assume that there is a K-model and let T = Q_{c}^{K};Q_{c}^{K}. By Proposition 1, T is definable from c, so that by Proposition 3 there is a weak initial T -algebra. Since the objects and morphisms in the range of T are in the range of Q_{c}^{K}, they belong to K′, so that by Proposition 4 there is a weak initial T′-algebra, where T′ is the restriction of T to K′.

Since K′ possesses the necessary equalizers, Proposition 7 gives that there is an initial T′-algebra, and Proposition 8 gives that there is an object u in K′ such that T′u is isomorphic to u. Moreover, since u and c belong to K′, which is a sub-ccc of both K and SET,

T′u = (u ⟹_{K} c) ⟹_{K} c = (u ⟹_{K′} c) ⟹_{K′} c = (u → c) → c .

But it is well known that, when c has more than one member, (u → c) → c has higher cardinality than u, and thus cannot be isomorphic to u in any subcategory of SET.

(End of Proof )

Simply taking K and K′ to be SET gives the result of [28] that there is no SET-model. (Of course, the cardinality argument is particular to classical logic; as shown in [24] and [18], “set-theoretic” models can be found in a constructive metatheory. On the other hand, as shown in [23], there is still a sense in which the above proposition carries over to the constructive case.) Moreover, since POS and DCPO both contain SET as a full sub-ccc (endowing sets with the discrete partial order) and, when c is a (so ordered) set, the objects in the range of Q_{c}^{POS} and Q_{c}^{DCPO} are all sets, one can take K to be POS or DCPO and K′ to be SET, to show that there is no POS- or DCPO-model.

One can also rule out various full sub-ccc’s of DCPO. For example, Achim Jung has characterized the four maximal Cartesian closed categories that are full sub-ccc’s of the category of algebraic directed-complete posets [16]. These are the category of all disjoint unions of bifinite domains (the SFP objects in [25]), the category of all disjoint unions of L-domains [14, 6], the category of profinite domains [13], and the category of the so-called FL domains. To see that these cannot give K-models, one applies Proposition 9, taking K′ to be SET or the category of finite sets, as appropriate.

The proposition can also be used to rule out some Cartesian closed categories of metric spaces used for the semantics of programming languages, such as the category of bounded ultrametric spaces and non-distance-increasing functions, or the full subcategory of the complete spaces [2]. In both cases one takes K′ to be SET (endowing sets with the discrete metric).

These results give some indication that it is necessary to require a least element to get a model over a category of posets. We can also obtain a result that indicates the need to require functions to be continuous. Let PPOS be the full sub-ccc of POS in which the objects are required to possess least elements, and (henceforth) let c be the poset

⊥ ⊤

Then Proposition 10 There is no solution in PPOS to the isomorphism (u ⇒ c) ⇒ c ≃ u.

Proof : Assume for the sake of contradiction that there is a poset P and an isomorphism ϕ from (P ⇒ c) ⇒ c to P. Using ordinal recursion, for each ordinal δ, we define \overline{δ} ^{∈} P by

\overline{δ} = ϕ(λf: P ⇒ c. ⨆_{c}\{ f\overline{μ} | μ < δ \}) .

We show by induction on δ′ that if \overline{δ} ⊑ \overline{δ′} then δ ≤ δ′. So suppose that \overline{δ} ⊑ \overline{δ′}. Since ϕ is an isomorphism, it follows that

⨆_{c}\{ f\overline{μ} | μ < δ \} ⊑ ⨆_{c}\{ f\overline{μ′} | μ′ < δ′ \}

holds for any f ^{∈} P ⇒ c. Now choose any ordinal μ satisfying μ < δ, and evaluate this inequality at the monotone function

fx = \{ \begin{matrix}⊤ & if \overline{μ} ⊑ x \\ ⊥ & otherwise . \end{matrix}

Since ⊤ occurs in the set on the left, it must occur in the set on the right, so that there is an ordinal μ′ < δ′ such that \overline{μ} ⊑ \overline{μ′}. Then the induction hypothesis gives μ ≤ μ′, so that μ < δ′. Then since μ is an arbitrary ordinal satisfying μ < δ, we obtain δ ≤ δ′, as desired.

As a consequence, if \overline{δ} = \overline{δ′} then δ = δ′, and so we have different elements of P for different ordinals. This is a contradiction, since the collection of elements of P is a set while that of the ordinals is a proper class. (End of Proof )

To use this result to show that there is no PPOS-model, we must get around the difficulty that PPOS has a paucity of equalizers. For example, if β_{1}, β_{2} ^{∈} c → c are the constant functions yielding ⊥ and ⊤, then {β_{1}, β_{2}} has no equalizer.

However, let PPOS_{⊥} be the subcategory of PPOS in which all morphisms are strict functions. Although it is not Cartesian closed, PPOS_{⊥} possesses equalizers of all subsets of its morphism sets. Specifically, the equalizer of S ⊆ k ⟶_{PPOS_{⊥}} k′ is the identity injection from

u = { x | x ^{∈} k and (∀β_{1}, β_{2} ^{∈} S) β_{1}x = β_{2}x }

to k.

Thus, by using Proposition 4 to move from PPOS to PPOS_{⊥}, we can prove:

Proposition 11 There is no PPOS-model.

Proof : Assume that there is a PPOS-model, and let T = Q_{c}^{PPOS} ; Q_{c}^{PPOS}. By Propositions 1 and 3 there is a weak initial T -algebra. Since every object of PPOS is also an object of PPOS_{⊥}, and the morphisms in the range of T, being also in the range of Q_{c}^{PPOS}, are strict, by Proposition 4 there is a weak initial T′-algebra, where T′ is the restriction of T to PPOS_{⊥}. Then Proposition 7 gives the existence of an initial T′-algebra, and Proposition 8 gives the existence of an object u that is isomorphic to T′u in PPOS_{⊥}. But T′u = T u = (u ⟹_{PPOS} c) ⟹_{PPOS} c, and an isomorphism in PPOS_{⊥} is an isomorphism in PPOS, which gives a contradiction with the previous proposition. (End of Proof )

Beyond these results, it would be particularly interesting to know whether a model is possible when K is the category CPO of complete posets (directed-complete posets with a least element) and continuous functions, or various full sub-ccc’s, particularly that of the bifinite domains. Currently, such “domain” models (e.g. [21], [20], [1], [10], and [7]) are known only for very special subcategories of CPO. However, this question cannot be resolved by the techniques developed in this paper, since CPO contains solutions to isomorphisms such as (u ⇒ c) ⇒ c ≃ u.

11. Application to Known Models

In several models of the polymorphic typed lambda calculus, the meaning of a type is (the set of equivalence classes of) a partial equivalence relation on a model of the untyped lambda calculus [9, 34, 22, 8, 15]. The underlying Cartesian closed categories of such models possess the equalizers needed to apply Proposition 7, so that there is an initial T -algebra for every definable T. An important open question for these models, however, is whether the equalizer construction is necessary, or whether ⟨P, H⟩, as defined in the proof of Proposition 2, is already an initial (rather than just weakly initial) T -algebra.

Underlying other models, such as [21], [20], [1], [10], and [7], are Cartesian closed subcategories of CPO. Unfortunately, these subcategories, like PPOS, have few equalizers. Indeed, there are few initial T -algebras for these subcategories; the usual notion of a continuous algebra [12] is equivalent to that of a T -algebra for the category CPO_{⊥} of complete partial orders and strict continuous functions, which possesses equalizers of all subsets of its morphism sets, but is not Cartesian closed.

There seems to be a connection between the weak initial T -algebras obtained for these models and continuous algebras based on CPO_{⊥}. However, it must be more complex than the connection used in the proof of Proposition 4, since the range of an arbitrary definable functor (most obviously, of the identity functor) is not limited to strict functions. Moreover, CPO_{⊥} is not a subcategory of the categories underlying the “domain” models, while the restriction of these categories to strict functions gives subcategories that do not possess equalizers of all subsets of their morphism sets.

References

[1] Amadio, R., Bruce, K. B., and Longo, G. The Finitary Projection Model for Second Order Lambda Calculus and Solutions to Higher Order Domain Equations. in: Proceedings Symposium on Logic in Computer Science, Cambridge, Massachusetts, June 16–18. 1986, pp. 122–130.

[2] America, P., de Bakker, J. W., Kok, J. N., and Rutten, J. Denotational Semantics of a Parallel Object-Oriented Language. Information and Computation, vol. 83 (1989), pp. 152–205.

[3] Barr, M. Coequalizers and Free Triples. Mathematische Zeitschrift, vol. 116 (1970), pp. 307–322.

[4] Barr, M. and Wells, C. Toposes, Triples, and Theories. Grundlehren der mathematischen Wissenschaften, vol. 278, Springer-Verlag, New York, 1985, xiii+345 pp.

[5] Böhm, C. and Berarducci, A. Automatic Synthesis of Typed Λ-Programs on Term Algebras. Theoretical Computer Science, vol. 39 (1985), pp. 135–154.

[6] Coquand, T. Categories of Embeddings. in: Proceedings Third Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, July 5–8. 1988, pp. 256–263.

[7] Coquand, T., Gunter, C. A., and Winskel, G. Domain Theoretic Models of Polymorphism. Information and Computation, vol. 81 (1989), pp. 123–167.

[8] Freyd, P. J. and Scedrov, A. Some Semantic Aspects of Polymorphic Lambda Calculus. in: Proceedings Symposium on Logic in Computer Science, Ithaca, New York, June 22–25. 1987, pp. 315–319.

[9] Girard, J.-Y. Interprétation Fonctionnelle et Élimination des Coupures de l’Arithmétique d’Ordre Supérieur, Thèse de doctorat d’état. Université Paris VII, June 1972.

[10] Girard, J.-Y. The System F of Variable Types, Fifteen Years Later. Theoretical Computer Science, vol. 45 (1986), pp. 159–192.

[11] Girard, J.-Y. 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. in: Proceedings of the Second Scandinavian Logic Symposium, University of Oslo, June 18– 20, 1970, edited by J. E. Fenstad. Studies in Logic and the Foundations of Mathematics, vol. 63, North-Holland, Amsterdam, 1971, pp. 63–92.

[12] Goguen, J. A., Thatcher, J. W., Wagner, E. G., and Wright, J. B. Initial Algebra Semantics and Continuous Algebras. Journal of the ACM, vol. 24 (1977), pp. 68–95.

[13] Gunter, C. A. Universal Profinite Domains. Information and Computation, vol. 72 (1987), pp. 1–30.

[14] Gunter, C. A. and Jung, A. Coherence and Consistency in Domains (Extended Outline). in: Proceedings Third Annual Symposium on Logic in Computer Science, Edinburgh, Scotland, July 5–8. 1988, pp. 309–317.

[15] Hyland, J. M. E. A Small Complete Category. Annals of Pure and Applied Logic, vol. 40 (1988), pp. 135–165.

[16] Jung, A. Cartesian Closed Categories of Domains. CWI Tracts, vol. 66, Centrum voor Wiskunde en Informatica, Amsterdam, 1989.

[17] Leivant, D. Reasoning About Functional Programs and Complexity Classes Associated with Type Disciplines. in: 24th Annual Symposium on Foundations of Computer Science, IEEE, Tucson, Arizona, November 7–9. 1983, pp. 460–469.

[18] Longo, G. and Moggi, E. Constructive Natural Deduction and its ‘ω-set’ Interpretation. Mathematical Structures in Computer Science, vol. 1 (1991), pp. 215–254.

[19] Mac Lane, S. Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5, Springer-Verlag, New York, 1971, ix+262 pp.

[20] McCracken, N. J. A Finitary Retract Model for the Polymorphic Lambda-Calculus. Unpublished, Syracuse University, 1982.

[21] McCracken, N. J. An Investigation of a Programming Language with a Polymorphic Type Structure, Ph. D. Dissertation. Syracuse University, June 1979, iv+126 pp.

[22] Mitchell, J. C. A Type-Inference Approach to Reduction Properties and Semantics of Polymorphic Expressions (Summary). in: Proceedings of the 1986 ACM Conference on Lisp and Functional Programming, Cambridge, Massachusetts, August 4–6. 1986, pp. 308–319.

[23] Pitts, A. M. Non-trivial Power Types can’t be Subtypes of Polymorphic Types. in: Proceedings Fourth Annual Symposium on Logic in Computer Science, Pacific Grove, California, June 5–8. 1989, pp. 6–13.

[24] Pitts, A. M. Polymorphism is Set Theoretic, Constructively. in: Category Theory and Computer Science, Edinburgh, Scotland, September 7–9, edited by D. H. Pitt, A. Poigné, and D. E. Rydeheard. Lecture Notes in Computer Science, vol. 283, Springer-Verlag, Berlin, 1987.

[25] Plotkin, G. D. A Powerdomain Construction. SIAM Journal on Computing, vol. 5 (1976), pp. 452–487.

[26] Plotkin, G. D. Private communication. July 16, 1984.

[27] Prawitz, D. Ideas and Results in Proof Theory. in: Proceedings of the Second Scandinavian Logic Symposium, University of Oslo, June 18–20, 1970, edited by J. E. Fenstad. Studies in Logic and the Foundations of Mathematics, vol. 63, North-Holland, Amsterdam, 1971, pp. 235–307.

[28] Reynolds, J. C. Polymorphism is not Set-Theoretic. in: Semantics of Data Types, International Symposium, Sophia-Antipolis, France, June 27–29, edited by G. Kahn, D. B. MacQueen, and G. D. Plotkin. Lecture Notes in Computer Science, vol. 173, Springer-Verlag, Berlin, 1984, pp. 145–156.

[29] Reynolds, J. C. Semantics of the Domain of Flow Diagrams. Journal of the ACM, vol. 24 (1977), pp. 484–503.

[30] Reynolds, J. C. Towards a Theory of Type Structure. in: Programming Symposium, Proceedings, Colloque sur la Programmation, Paris, April 9–11, edited by B. Robinet. Lecture Notes in Computer Science, vol. 19, Springer-Verlag, Berlin, 1974, pp. 408– 425.

[31] Reynolds, J. C. Types, Abstraction and Parametric Polymorphism. in: Information Processing 83, Proceedings of the IFIP 9th World Computer Congress, Paris, September 19–23, 1983, edited by R. E. A. Mason. Elsevier Science Publishers B. V. (North-Holland), Amsterdam, 1983, pp. 513–523.

[32] Seely, R. A. G. Categorical Semantics for Higher Order Polymorphic Lambda Calculus. Journal of Symbolic Logic, vol. 52 (1987), pp. 969–989.

[33] Takeuti, G. Proof Theory. Studies in Logic and the Foundations of Mathematics, vol. 81, North-Holland, Amsterdam, 1975, viii+372 pp.

[34] Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. edited by A. S. Troelstra. Lecture Notes in Mathematics, vol. 344, Springer-Verlag, Berlin, 1973, xvii+485 pp.