mostly within the computer science community, from both the syntactic (typing, consistent

extensions, etc.) and semantic points of view. The main novelty of l 2 , over the simply typed

calculus, is the possibility of abstracting a term with respect to type variables; by this, l2 represents

’polymorphic“ functions, that is, functions that may have several types or, more precisely, that may

update their own type.

It is largely agreed that this specific formalization of the broad notion of polymorphism in

programming focuses most of the main concerns of the programmers who apply these methods and

suggests relevant implementations of modularity in functional programming.

The type system of l 2 is an extension of the simple types in section 8.2, and it is meant to

provide a type for polymorphic functions (i.e., terms obtained by type abstraction). As we said, this

is achieved by introducing type variables and allowing a quantification (informally, a product) over all

types. The type "X:Tp.T is the type of all those terms that, when applied to a type S, yield a new

term of type [S/X]T. Types are defined impredicatively since in the inductive definition of the

collection Tp of all types one has to use Tp itself, which is being defined. For example, Tp is used

when defining "X:Tp.T as a type or, also, "X:Tp.T is said to be a type, while it contains a

quantification over all types, including itself. The ’dimensional clash“ (and the semantic difficulty)

which derives from impredicativity is evident when considering that a term of type "X:Tp.T can be

applied to its own type. This circularity, very common in mathematics (e.g., for least upper bounds

and related notions) comes with the expressive power of the system and is reflected in the difficulty

of finding sound mathematical models for it. It is our opinion that Internal Category Theory provides

significant tools for this semantic investigation. First, it allows the explicit use of ’constructive“

universes, as an alternative to the (usually intended) set-theoretic frame for (small) categories, where

the constructions below would provide trivial models. Second, it reflects and gives meaning to the

circularity of impredicativity by a mathematically clear closure property of some internal categories.

251

11. Second Order Lambda Calculus

11.1 Syntax

Types and (rough) terms are first defined in BN-form. The typing rules will pick up, among the

rough terms, the legal ones. Types are built up from type variables, ranged by X, Y, ZÉ; terms are

built up from (term) variables, ranged by x, y,É:

Type expressions: T := X | (T ® S) | ("X:Tp.T )

Term expressions: e := x | (ee) | (eT) | (lx:T.e) | (LX:Tp.e).

We use capital letters T,S,... as metavariables for type expressions.

Conventions: l, L and " are all variable binders. An unbound variable x in e is free in e

(notation: xÎFV(e) ). The substitution of a for x in e ([a/x]e) is defined by induction,

provided that a is free for x in e, as usual.

A context is a finite set G of type variables; GX stands for GÈ{X}. A type T is legal in G iff

FV(T) Í G. A type assignment in G is a finite list E = (x1:T1),É, (xn:Tn) such that any Ti is

legal in G.

The typing relation G;E |- e: T, where E is a type assignment legal in G, e is a term expression

and T is a type expression, is defined as follows:

G;E |_ x:T

(assumption) if (x:T)ÎE

G;E(x:T) |_ e: S

_____________________

(®I)

G;E |_ (lx:T.e) : (T®S)

G;E |- f: (T®S) G;E |- e: T

________________________

(®E)

G;E |- (fe) : S

GX; E |_ e : T

___________________________

("I) (*)

G;E |_ (LX: Tp. e) : ("X : Tp. T)

* if there is no variable in FV(e) whose type depends on X

G;E |_ f : ("X : Tp . T) G |_ S : Tp

________________________________

("E)

G;E |_ (fS) : [S/X]T

252

11. Second Order Lambda Calculus

Conversion Equations among well-typed terms are defined by the following axioms:

(lx:A .b) e = [e/x]b

b.

b2. (LX:Tp .b) A = [A/X]b

lx:A .bx = b if xÏFV(b)

h.

h2. LX:Tp .bX = b if XÏFV(b)

and by the usual rules that turn ’=“ into a congruence relation.

Before starting the formal definition of the models for such a system, it is worthwhile to say a few

words about its interpretation, and to try to explain the following work by a naive presentation of the

categorical meaning of l 2 . Note also that this chapter is followed by one entirely dedicated to

examples of the abstract categorical treatment which we follow here. The reader may find convenient

to check hi/her understanding of it against the structures presented in chapter 12.

As pointed out in chapter 8, any Cartesian closed category C can be used to give a categorical

semantics to the simply typed lambda calculus: types (which are just constant types or ’arrow types“)

are interpreted by objects of C; terms of type T, with free variables x1 :T 1 ,É, xn :T n , are

interpreted as morphisms from T1´É´ Tn to T. The categorical interpretation of the second order

calculus generalizes this semantics; in this case, however, the collection of types Tp must be closed

not only under the arrow construction, but also under universal quantification. If we write "X:Tp.T

as "(lX:Tp.T), where l is an informal lambda notation for functions, " may be readily

understood as a map from (Tp ® Tp) to Tp, as it turns the map lX:Tp.T in (Tp®Tp) into a

type. Thus, the interpretation of " should be a map from ObC®ObC to ObC. The problem is that

this map has to be represented internally in some ambient category. A natural choice is to have some

sort of metacategory E such that C may be regarded as an internal category of E, in the sense of

section 7.2. Recall, in short, that C must consist of a pair (c0 , c1 ) of objects of E such that,

informally, ObC = c0 and MorC = c1 . If E is Cartesian closed, then " may typed as ":

c0c0®c0.

Objects of the kind Tp®Tp (i.e. ’points,“ or ’elements“ of c0c0) are usually called variable

types. As we have already seen, if s is a variable type, the type "(s) represents intuitively the

collection of all the polymorphic terms e such that, for all types T, (eT) : s(T). This is equivalent

to saying that "(s) is a dependent product that is, a product of different copies of c0 indexed by s

on elements of c0 itself. The projections of this dependent product yield the instances of the

polymorphic terms in "(s) with respect to particular types. In other words, there will be in the

model an operation proj: (c0®c0)´c0®c1 that takes a variable type s: c0®c0, a type T, and gives

a morphism projs(T): "(s)®s(T); projs(T) describes how a polymorphic term of type "(s) can

be instantiated into the type s(T), thus modeling the application of a term e in "(s) to a type T.

By the definition of a dependent product, we will also have an isomorphism between the

polymorphic terms in "(s) and the collection of all the families {eT: s(T)}TÎc0 of terms indexed

253

11. Second Order Lambda Calculus

over all types. Let us call D this isomorphism, which relates a family of terms {eT: s(T)}TÎc0 to

the polymorphic term D({eT: s(T)}TÎc0) = LT:Tp.eT : "(s). The functions proj and D satisfy

the following equations:

1. projs(S) ( D({eT}TÎc0) ) = eS ;

2. D({projs(T)(e)}TÎc0) = e ;

whose meaning may be sketched as follows:

1. if we define a polymorphic function from the collection of functions {eT}TÎc0, and then we

consider the particular instance relative to the type S, this is equal to the original function eS;

2. if, given a polymorphic function e, we consider the collection of all its instances

{projs(T)(e)}TÎc0 and then we use this collection to rebuild a polymorphic function, we obtain e

again.

Equations 1. and 2. above are the key facts allowing the interpretation of rules b and h,

respectively, for second order abstraction and application.

Exercise Compare equations 1 and 2 above with the equations for the categorical Cartesian product

pi » <f1,f2> = fi for i = 1,2 ;

< p1 » f, p2 » f > = f .

11.2 The External Model

The informal discussion of the previous section should have motivated the use of internal concepts in

describing the semantics of l2. The model definition inspired by these ideas will be the main object

of study in this chapter and it is presented in the following section. We introduce here a different

notion of categorical model that does not require the use of internal concepts. It is based on an

algebraic generalization of the semantics of the simply typed lambda calculus in a bidimensional

universe of Cartesian closed categories indexed over another (global) CCC. We will call this model

’external.“ In this model the collection of types is represented by a single object of the global

category, say c0 (or W, as it is usually denoted in this approach), but no requirement is made in order

to have an internal category with c0 as an object of objects. This fact, however, must be heavily

compensated for by a number of particular conditions that relate ’on the nose“ categorical properties

of indexed categories, which are not very intuitive. Thus, on one hand, the external model is more

manageable then the internal one; on the other, it is less limpid and, in a sense, less suggestive. We

claim that both these properties of the external model are due to the fact that it is a particularly simple

instance of the internal notion. More specifically, we will show that an external model is just an

internal one whose ambient category is a topos of presheaves, and whose object of objects c0 is a

representable functor [_,W]. The understanding we propose of the external model also sheds some

254

11. Second Order Lambda Calculus

light on the interplay among the different conditions in its definition and gives a new justification for

some apparently ad hoc requirements.

At the base of the external notion of a model for l 2 , there is the notion of a class of small

categories indexed over another (global) category E - essentially a contravariant functor G from E

to Cat. E is a Cartesian category with a distinguished object W, which interprets the collection of

types. Products Wn are used to give meaning to contexts. Arrows in E[Wn,W] represent types with

at most n free variables in the context Wn .

The functor G: E®Cat takes every context W n in E to a (local) category G(W n) whose

objects are the types legal in that context. Thus these types appear both as arrows in E and as objects

in the local categories, and it is natural to require Obj(G(e)) = homE(e, W). The arrows between two

types s and t in a local category G(Wn) correspond to terms of type t and free variables in s.

Every local category is required to be a model of a simply typed lambda calculus and, thus, it is

Cartesian closed. As for the interpretation of the polymorphic product it is described by an adjoint

situation between local categories; moreover this adjointness must be natural with respect to the global

parameter given by the context.

11.2.1 Definition An external l 2 model (PL category) is a triple (E, G, W ) where:

1. E is a Cartesian closed category (global category);

2. W is a distinct object in E;

3. G: Eop ® Cat is a functor such that

i. for each object e in E, Obj(G(e)) = homE(e, W), and, for each morphism s•ÎE[e',e], the

functor G(s•): G(e) ® G(e') acts on the objects of G(e) as homE(s•,W).

ii. for each object e in E, the (local) category G(e) is Cartesian closed; for every s•ÎE[e',e],

the functor G(s•): G(e) ® G(e') preserves the Cartesian closed structure ’on the nose“ (and

not just up to isomorphism); that is, for a,bÎObjG(e) = homE(e, W) it satisfies:

a. G(s•)( tG(e) ) = tG(e'), where tG(e) is the terminal object in G(e)

G(s•)( !a ) = !G(s•)(a)

b. G(s•)( a ´ G(e) b) = G(s•)(a) ´G(e') G(s•)(b), where ´G(e) is the product in G(e)

G(s•)(fsta,b) = fstG( s)(a),G( s)(b)

G(s•)(snda,b) = sndG( s)(a),G( s)(b)

c. G(s•)([a,b]G(e)) = [G(s•)(a), G(s•)(b)]G(e'), where [,]G(e) is the exponent in G(e)

G(s•)(evala,b) = evalG( s)(a),G( s)(b)

iii. an E-indexed adjunction < Fst, ", D > : G ® GW, where

a. GW : Eop ® Cat (see definition 7.1.2) is the functor defined by

GW(e) = G(e´W)

"eÎObE

"sÎE[e',e] GW( s) = G( s´idW)

b. "eÎObE , Fst(e) = G(fste,W ) : G(e) ® GW(e) = G(e´W) (with fste,W: e´W®e).

255

11. Second Order Lambda Calculus

By definition 7.1.6 of an E-indexed adjunction, we have, for every object e in E, an adjunction

< G(fste,W), "(e), D(e) > : G(e) ® G(e´W)

and, moreover, D(e') » G(s•´idW) = G(s) » D(e)

11.2.2 Remark If (E,G) is an external l 2 model, then we have the following natural

transformations:

´G(_): homE´E(K2(_), ( W ,W)) ® homE(_, W),

[,]G(_): homE´E(K2(_), ( W ,W)) ® homE(_, W),

homE(_´W, W) ® homE(_, W),

":

where K2 is the diagonal functor.

Indeed conditions 3.ii.b and 3.ii.c in definition 11.2.1 express exactly the naturality of ´G(_)

and [,]G(_) , while by definition " is natural from GW to G and, a fortiori, also from

homE(_´W, W ) to homE(_, W).

11.2.3 Lemma For every object a in E there are morphisms

x0 : WxW ® W

[,]0 : WxW ® W

"0: WW ® W

such that, for each object e of E and for all objects s,t of G(e),

x0 » <s,t> = s ´G(e)t

[,]0 » <s,t> = [s,t]G(e)

and, for each object r of G(e´W),

"0 » L(r) = "(e)(r)

Proof We have the following natural transformations

e1 = ´G(_) » <,> -1 : homE(_, W´W) ® homE(_, W)

e2 = [,]G(_) » <,> -1 : homE(_, W´W) ® homE(_, W)

e3 = " » L -1 : homE(_, WW) ® homE(_, W)

where

´G(_): homE´E( K2(_), (W,W) ) ® homE(_, W)

[,]G(_): homE´E( K2(_), (W,W) ) ® homE(_, W)

homE(_´W, W) ® homE(_, W)

":

are the natural transformations of remark 11.2.2 and

<,>-1 : homE(_, W´W) ® homE´E( K2(_), (W,W) )

L -1: homE(_, WW) ® homE(_´W, W)

are the natural isomorphisms given by the Cartesian closure of E.

256

11. Second Order Lambda Calculus

Then, by the Yoneda lemma, the arrows x0, [,]0, "0 with the requested properties are obtained

by setting

x0 = e1(W´W)(idW´W)

[,]0 = e2(W´W)(idW´W)

"0 = e3(WW)(idWW)

For example, we have, for s,t: e ® W,

x0 » <s,t> = e1(W´W)(idW´W) » <s,t>

= homE[<s,t>, W´W] (e1(W´W)(idW´W))

= e1(e)(homE[<s,t>, W´W](idW´W))

= e1(e) <s,t>

= s ´G(e)t.

The other equations are proved similarly. ¨

11.3 The External Interpretation

In this section we define, in several steps, the ’external“ interpretation of the second order lambda

calculus.

11.3.1 Type Expressions A type expression T legal in a context G = {X1 ,...,X n } i s

interpreted by a morphism [T]G: [G]®[A] in E (where [G] = c0n=((t´c0)´É´c0), inductively

defined as follows:

[Xi]G = snd»fstn-i;

1.

2. [S®T]G = [,]0 » < [S] G, [T] G >;

3. ["X:Tp.T]G = "0 » L([T]GX ).

Note that, as in the simply typed l-calculus, variables are projections and arrows are exponents.

Morover, impredicative types are interpreted by formalizing (externally) the informal discussion at the

end of 11.2 (see also 11.5.1).

11.3.2 Type assignment A legal type assignment E = (z1 : S1 )... (zn : Sn ), in a context G, is

interpreted by the product (local in G([G]) )

[E]G = (...(tG([G]) ´[S1]G)...)´[Sn]G = xon » <...<tG([G]),[S1]G>...,[Sn]G >

where tG([G]) is the terminal object in the local category G([G]).

11.3.3 Terms A legal term M such that

G = X1,...,Xn ; E = (z1: S1)... (zn: Sn) |- M : T

is interpreted by a morphism

257

11. Second Order Lambda Calculus

[M]GE : [E]G®[T]G in the local category G([G]) .

The inductive definition is

[zi]GE = snd » fstn-i;

1.

2. [MN]GE = eval » <[M]GE, [N]GE>;

3. [lx:S.M]GE = L([M]GE[x:S] );

4. [LX:Tp.M]GE = D([M]GX;E);

5. [M[T]]GE = G(<id, [T] G >) (Proj([G])) » [M]GE,

where Proje is the counit of the adjunction < G(fste,W), "(e), D(e) > : G(e)®G(e´W), i.e., Proje

= D(e)-1(id).

11.3.4 Remark The interpretation we have just given is somewhat informal. Indeed we should

always specify in which local category we are working in, and we should add a lot of indices for the

natural transformations. Note also that the interpretation is not, as it could seem, by induction on the

syntactical structure of terms, but on the lenghth of the proof of their derivation (the proof that the

terms are well typed). For example, a fully specified interpretation for [LX:Tp.M]GE would be: if

GX; E |- M: T and t = [T]GX then [LX:Tp.M]GE = (D([G])([E]G, t ) ) ([M]GX;E).

11.4 The Internal Model

In this section we define the notion of internal l2 model. The intuition is to require for an internal

Cartesian closed category cÎCat(E) the existence of the arrow "0: c0c0®c0, which gives the

depended product, in a such a way that equations 1 and 2 of section 11.1 are verified. We obtain by

this a characterization of internal models by means of ground equations, with the consequence that

internal models are preserved by limit- and exponent-preserving functors.

In what follows, we always assume that the ambient category E is Cartesian closed and has finite

limits.

11.4.1 Definition Let a be an object of E. |a| is the internal category (a, a, id, id, id, id ).

The internal |a| represents (internalizes) the discrete category with exactly one morphism (the

identity) for each point in a.

11.4.2 Definition Let c = (c0, c1, DOM, COD, COMP, ID)ÎCat(E). Define then:

c* = (c0c0, c1c0, DOM*, COD*, COMP*, ID*) with

DOM* = L(DOM » eval)

COD* = L(COD » eval)

COMP* = L(COMP » eval´0eval » p)

258

11. Second Order Lambda Calculus

ID* = L(ID » eval)

where p = <<P1° p1, p2>, <P2° p1, p2>>0 : (c1c0 ´0 c1c0) ´ c0 ® (c1c0 ´ c0) ´0 (c1c0 ´ c0).

The idea behind the previous definition is that the object c* represents internally the category of

functors from |c0| to c. Note that, as |c0| is a discrete category, the functors F from |c0| to c are

fully determined by their functions f0 on objects. In effect, this informal idea may be formalized by

the following remark: if E is Cartesian closed, so it is Cat(E). The object c* of the previous

definition is isomorphic in Cat(E) to the exponent of |c0| and c. The category c* may be also

regarded as the collection of all tuples of elements of c indexed by elements in c0, for |c0| is a

discrete category.

11.4.3 Definition The constant internal functor K : c®c* is K = (k0, k1) with

k0 = L(fst) : c0®c0c0 where fst: c0´c0®c0 is the projection

k1 = L(fst) : c1®c1c0 where fst: c1´c0®c1 is the projection.

K : c®c* must be considered as a sort of diagonal functor. Informally, given an object b in c0, its

image under K is the tuple (indexed on c0) of all-b elements (i.e., the constant-b function from c0

to c0 ). As a right adjoint to the diagonal functor K 2 : C®C 2 yields the categorical product,

similarly, a right adjoint to the functor K : c®c* yields the (categorical) dependent product indexed

over c0.

11.4.4 Definition A model for l 2 is given by

1. a Cartesian closed category E with all finite limits (global category);

2. an internal Cartesian closed category c = (c0,c1,DOM,COD,COMP,ID)ÎCat(E);

3. a right (internal) adjoint to K: c ® c* .

The requirements on the global category E in the previous definition could be slightly relaxed: the

notion of internal category can be also given in interesting ambient categories without all limits (see

the next chapter for an example). Similarly, for a model of l2 we actually need only exponents of the

form ec0 in E. Our requirements are very close to those needed for models of the stronger calculus

Fw. In this case the only further condition is that of having a right (internal) adjoint to Ke: c®ce for

every object e of E, where ce = (c0e, c1e, DOMe, CODe, COMPe, IDe) represents the category

of functors from |e| to c, and Ke: c®ce is the internal functor defined by

Ke = (ke,0 = L(fst): c0®c0e, ke,1 = L(fst): c1®c1e).

By theorem 7.3.7, a right adjoint to K: c ® c* is fully determined by

i. an arrow "0: c0c0® c0,

259

11. Second Order Lambda Calculus

ii. an arrow PROJ: c0c0® c1c0 such that DOM* » PROJ = k0 » "0 , COD* » PROJ = id.

(if h: e ® c0c0 , we use the abbreviation PROJh for PROJ » h )

iii. an arrow D: X"® Y" where X" and Y" are respectively the pullbacks of

< DOM* , COD* > : c1c0® c0c0´c0c0, k0´id : c0´c0c0® c0c0´c0c0

< DOM,COD > : c1® c0´c0, id´"0 : c0´c0c0®c0´c0

such that:

g0. g' » D = g

g1. (PROJ » p2 » g) * ( L(fst) » PY" » D ) = PX"

h. D » < g', (PROJ» p2 » g') * ( L(fst) » PY" ) >0 = idY"

where h*k = COMP* » <h,k>0 = L( L-1(h) oL-1(k) ), and fst: c1´c0®c1 is the projection.

PROJ is the counit of the adjunction. In order to understand its meaning, it is useful to compare it

with the counit of the Cartesian product. In that case, the counit is

(p(a1,a2),1, p(a1,a2),2) Î C2[ (K2(a1´a2), (a1,a2) ]

where K2 is the diagonal functor. That is, the counit is a collection of morphisms p(a1,a2),i in C,

indexed over objects (a1,a2) of C2 and objects i = 1,2 in the category 2, such that each p(a1,a2),i

has domain a1 ´a 2 and codomain ai. Analogously, PROJ: c0 c 0®c 1 c 0 @ c 0 c 0´c 0 ®c 1 is a

collection of morphisms PROJs(T) in c1 indexed over objects s of c* and objects T of c

(which now corresponds to the category 2 above), such that each projection PROJs(T) has domain

"0(s) and codomain s(T).

Consider now two points f: t®c1c0, g: t®c1 in c1c0 and c1. Informally, f is a family of

terms in c1 indexed by objects in c0, and g is a term in c1. If there exists some a such that

DOM » f = K0 » a, that is if all the terms represented by f have a common domain a : t®c0, then

we can ’apply“ the isomorphism D and obtain the polymorphic term D»f (note the usual confusion

between application and composition resulting from reasoning about points). Conversely, if there

exists b such that COD » g = "0 » b, then g is a polymorphic term of type "0»b.

Formally, for every e in E, given f: e ® c1c0 and g: e® c1 such that

DOM » f = K0 » a COD » f = b

DOM » g = a COD » g = "a0 » b

260

11. Second Order Lambda Calculus

equations (g1) and (h) above give

g1. PROJb * ( L(fst) » PY" » D » <<a,b>,f>0 ) = f

h. D » < <a,b>, PROJb * ( L(fst) » g ) >0 = <<a,b>,g>0

and with easy manipulations, recalling that h*k = COMP * » <h,k>0 = L( L-1(h) o L-1(k) ), one

obtains

g1'. L( (eval » PROJb´idc0)o(PY" » D » <<a,b>,f>0 » fst) ) = f

o

h'. D » < <a,b>, L( (eval » PROJb´idc0)o(g » fst) ) >0 = <<a,b>,g>0

o

which are the formalization of equations 1 and 2 of our informal discussion about second order

models in section 11.1.

11.5 The Internal Interpretation

Let us now summarize some of the data that come with an internal model. All these objects,

morphisms, and functions will be used to give an explicit definition of the interpretation for second

order terms as follows:

i. For the global category E:

- a terminal object T, products and exponents

- projections: fst, snd

- evaluation morphism: eval (used for defining COMP*)

- pairing function: <,>

- ’currying“ function: L

ii. For the internal category:

- an arrow t0: T ® c0 defining the internal terminal object

- an arrow x0 : c0´c0 ® c0 defining the internal product

- an arrow [,]0 : c0´c0 ® c0 defining the internal exponent

- an arrow "0: c0c0 ® c0 defining the dependent product

- internal projections: FST: c0´c0 ® c1 , SND: c0´c0 ® c1

- internal evaluation morphism: EVAL: c0´c0 ® c1

- instantiation morphism: PROJ: c0c0 ® c1c0 of the dependent product

- internal pairing: <,>: (c0´c0´c0) ´0 (c1´c1)®(c0´c0´c0) ´0 c1

<,>(a,b,c, f: a®b, g:a®c) = (a,b,c, pairing(f,g): a®b´c )

- internal currying function: L: (c0´c0´c0) ´0 c1® (c0´c0´c0) ´0 c1

L(a,b,c, f:a´b®c) = (a,b,c, curry(f): a®cb)

- dependent pairing: D: (c0´c0c0) ´0 c1c0 ® (c0´c0c0) ´0 c1

D( a, s,{eT: a®s(T)} ) = (a, s, dep_pairing({eT}): a®"(s) ).

261

11. Second Order Lambda Calculus

We point out that an internal model is completely determined by (pullbacks and) a set of ground

equations, that is, equations without (quantified) free variables; this contrasts with external models

(or with standard, ’external“ Cartesian closed categories, for that matter). An important consequence

of this is that internal models are preserved by limit- and exponent- preserving functors (that is

functors preserving the structure for sources and targets of the data defining the model). This fact will

be used later on to relate internal and external models.

Notation For eÎObE, en = (((t´e)´e)´É´e) where t is the terminal object of E and e appears

n times.

11.5.1 Type Expressions A type expression T legal in a context G = {X 1 , ..., Xn } is

interpreted by a morphism [T]G : c0n®c0 in E. In particular:

[Xi]G = snd » fstn-i

1.

2. [S®T]G = [,]0 » < [S]G, [T]G >

3. ["X:Tp.T]G = "0 » L([T]GX )

11.5.2 Type Assignments A type assignment E = (z1 : S1 )...(zm : Sm ) legal in a context G

={X1,...,Xn} is interpreted by the product

[E]G = x0m » <...<t0 ° !c0n,[S1]G>...,[Sm]G> : c0n ® c0

where x01 = x0 and, for i>1, x0i = x0 » (x0i-1´id).

11.5.3.Terms A legal term e such that

G = {X1,...,Xn}; E = [z1: S1]... [zm: Sm] |- e : T

is interpreted by a morphism

[e]GE : c0n ® c1

such that DOM » [e]GE = [E]G : c0n ® c0

COD » [e]GE = [T]G : c0n ® c0

In particular,

[zi]GE = SND o FSTn-i

1.

(where for simplicity we omit the ’indexes“ for FST and SND);

2. if G;E |- f: S®T , G;E |- e:S, s = [S]G , t = [T]G, then

[fe]GE = EVALs,t o ( <,> » < <<[E]G,[S®T]G>, s>0 , <[f]GE,[e]GE> >0);

3. if G;E(x:S) |- e: T , s = [S]G , t = [T]G, then

[lx:S.e]GE = Py' » L » < <[E]G,s,t>, [e]GE(x:S) >0 ;

4. if GX; E |- e: T and t = [T]GX, then

[LX:Tp.e]GE = PY" » D » < <[E]G,L(t)>, L([e]GX;E)>0 ;

262

11. Second Order Lambda Calculus

5. if G,E |- e: "X:Tp.S and s = L([S] GX), then

[eT]GE = L-1(PROJs * ( L(fst) » [e]GE ) ) » <id, [T]G>

= ( L-1(PROJs) o ([e]GE » fst) ) » <id, [T]G>

(where h * k = COMP* » <h,k> ; h o k = COMP » <h,k>).

Given the above definitions, the proof of a soundness theorem, with the required substitution

lemmas, is a routine check (as straightforward as it is tedious and laborious).

11.6 Relating Models

In the previous sections, two different notions of model have been introduced. We are now interested

in the relation between them. It will turn out that the two notions are not as distant as they may seem.

We start by an analysis of how we can define an external model from an internal one. The

construction is based on the externalization process of an internal category via hom-functors

presented in chapter 7, which corresponds, essentially, to the Yoneda embedding. Since the hom-

functor preserves pullbacks and exponents, we will be able to show that any internal model yields an

’equivalent“ external one.

Suppose that c = (c0,c1,DOM,COD,COMP,ID)ÎCat(E) is an internal model. As the reader has

probably imagined, the functor [_,c] : Eop®Cat of definition 7.4.2 plays the role of G in the

external approach. For ease of reference, we recall here that definition.

11.6.1 Definition Let cÎCat(E). The functor G = [_,c] : Eop® Cat is defined in the following

way:

on objects eÎE [_,c] = [e,c] ;

on arrows s: e'®e [_,c](s) = [s,c] is the functor from [e,c] in [e',c] which is defined as

[s,c0] on objects and as [s,c1] on arrows.

11.6.2 Lemma " s: e'®e, G(s) = [s,c]: [e,c]®[e',c] acts on the objects of [e,c] (i.e., on

E[e,c0]) as E[s,c0].

Proof By definition. ¨

11.6.3 Lemma If c is (internally) Cartesian closed, then, for every e in E, Ee,c is Cartesian

closed.

Proof (sketch)

Let 1. < O, T, o > : c ® 1

2. < D, x, < , > > : c ® c´c

3. < x, [,] , L > : c ® c

263

11. Second Order Lambda Calculus

be the internal adjunctions given by the Cartesian closure of c. Then <[_,F], [_,G], Q > :

[_,c]®[_,d] is an E-indexed adjunction. By proposition 7.4.11 there are three E-indexed adjunctions

1'. <[_,O], [_,T], o' > : [_,c]®[_,1]

2'. <[_,D], [_,x], <,>' > : [_,c]®[_,c´c] @ [_,c]´[_,c]

3'. <[_,x], [_, [,] ], L' > : [_,c]®[_,c] with parameters in [_,c].

Hence for every e in E, [e,c] is Cartesian closed, since [e,1] is the terminal category in Cat and

[e,D] : [_,c]®[_,c]´[_,c] is the diagonal functor. ¨

Propositions 7.4.10 and 7.4.11 allow us to give an explicit definition for the natural

isomorphisms in (1')-(3') above. In particular,

given s,t, g : e®c0, and f: e ®c1´c1 such that DOM » f = D0 » s, COD » f = < t, g >

<,>'(f) = Py » <,> » (< <s, <t, g> >, f >0 ) : e ® c1;

given s,t, g : e®c0, and g: e®c1 such that DOM » g = s, COD » f = x0 » < t, g >

<,>'-1(g) = Px » <,>-1» (< < s, <t,g> >, g >0 ) : e ® c1´c1;

given s,t, g : e® c0 and f: e® c1 such that DOM » f = x0 » < s,t >, COD » f = g

L'(f) = Py' » L » (< <<s,t>, g >, f ) : e ® c1;

given s,t, g : e ® c0 and g: e® c1 such that DOM » g = s, COD » g = [,]0 » <t, g >

L'-1(g) = Px' » L-1 » (< <s,<t, g >, g ) : e ® c1.

By exercise 7.4.12, given s,t : e®c0, the projections associated to <,>' are derived from the

internal projections FST and SND by

FSTs,t = FST » <s,t> : e®c1

SNDs,t = SND » <s,t>: e®c1.

Note that

DOM » FSTs,t = x0 » <s,t>

COD » FSTs,t = s

DOM » SNDs,t = x0 » <s,t>

COD » SNDs,t = t.

Analogously, given s,t : e ® c0, the counit EVALs,t of L' for the object [,]0»<s,t> is

EVALs,t = EVAL » <s,t> : e ® c1

where EVAL is the internal evaluation map.

Note that

DOM » EVALs,t = x0 » <[,]0» <s,t>, s >

COD » EVALs,t = t .

11.6.4 Lemma Let c be (internally) Cartesian closed. "s: e'®e, [s,c]: [e,c]®[e,c'] preserves

the Cartesian closed structure "on the nose".

264

11. Second Order Lambda Calculus

Proof We only consider the product; the other cases are similar.

"t,g in [e,c] [s,c](t´g) = [s,c]( [e,x](t,g) )

= [s,c]( x0 » <t,g> ) by def. of [e,x]

= x0 » <t,g> » s

= x0 » <t » s, g » s >

= x0 » < [s,c](t), [s,c](g) >

= [e,x]( [s,c](t), [s,c](g) )

= [s,c](t) ´ [s,c](g) by def. of [e,x]. ¨

11.6.5 Lemma For every e, a objects of E, [e,c|a|] @ [e´a,c] .

Proof E is Cartesian closed, thus there are the isomorphisms

Le,c0: E[e´a, c0] @ E[e, c0a]

Le,c1: E[e´a, c1] @ E[e, c1a].

Le,c0 and Le,c1 are respectively the functions on objects and on arrows of a functor L from [e´a,c]

to [e,c|a|] . Indeed, for every s: e´a®c0

Le,c1(ids) = Le,c1(ID » s)

= Le,c1(ID » eval » Le,c0(s)´id )

= Le,c1(ID » eval) » Le,c0(s)

= IDc|a| » Le,c0(s)

= idL(s)

and for every f, g: e´a®c1

Le,c1(g o f) = Le,c1(COMP » <g,f>)

= L(COMP » <eval » Le,c1(g)´id, eval » Le,c1(f)´id> )

= L(COMP» eval´eval » <Le,c1(g)´id, Le,c1(f)´id> )

= L(COMP» eval´eval » p » <Le,c1(g), Le,c1(f) >´id)

= L(COMP»eval´eval»p) » <Le,c1(g), Le,c1(f) >

= COMPc|a| » <Le,c1(g), Le,c1(f) >

= Le,c1(g) o Le,c1(f)

Similarly, Le,c 0 -1 and L e,c 1 -1 define the functions on objects and on arrows of L -1 ,

respectively. ¨

11.6.6 Lemma Let K: c®c* be the functor of definition 11.4.3. For every e in E, L -1 » [e,K] =

G(fst) = [fst,c] : [e,c]®[e,c|a|].

Proof On objects s: e®c0

(L-1 » [e,K])(s) = L-1([e,K](s) )

= L-1(k0 » s ) by def. of [e,K]

= L-1(k0) » s´id

265

11. Second Order Lambda Calculus

= fst » s´id by def. of k0

= s » fst

= [fst,c](s) by def. of [fst,c].

On arrows f: e®c1

(L-1 » [e,K])(f) = L-1([e,K]( f ) )

= L-1(k1 » f ) by def. of [e,K]

= L-1(k1) » f ´id

= fst » f ´id by def. of k1

= f » fst

= [fst,c]( f ) by def. of [fst,c]. ¨

11.6.7 Corollary Let W = c0 . Then for every e in E, <[fst,c], [e,"] » L , D '» Le,c 1 > :

[e,c]®[e´W,c] is an adjunction.

Proof By lemma 11.6.6, [fst,c] = L -1» [e,K] . Then we have the isomorphisms

D'

Le,c1

[e´W,c][Le,c0-1([e,K](s)), t] @ [e,c*][ [e,K](s), Le,c0(t)] @ [e,c][ s, [e,"](Le,c0(t))]. ¨

Note that, given s: e®c0 ,t: e´a®c0 , and f: e´a®c1 such that

DOM » f = L-1([e,K](s) ) = s » fst

COD » f = t,

we have D'» Le,c1(f) = PY" » D » (<<s, t >, L(f) >0 ) : e®c1, where PY" is as in the diagram

after definition 11.4.4.

Analogously, given s: e®c0, t: e´a®c0, and g: e®c1 such that

DOM » g = s

COD » f = [e,"](L(t) ) = "0 » L(t)

we have the following:

(D'» Le,c1)-1(g) =

= Le,c1-1 (D'-1(g))

= L-1(PX" » D'-1 » (<<s, t >, g >0 ) )

= eval » (PX" » D'-1 » (<<s, t >, g >0 ) )´id: e´a®c1.

In particular, given s : e ® c0c0, the counit (D'» Le,c1)-1(id[e,"](L(t)) ) is

Projs,t = eval » (PX" » D'-1 » (< <s, t >, ID » "0 » L(s) >0 ) )´id: e´c0 ® c1

= eval » (PROJ » <s,t>)´id

= L-1( (PROJ » <s,t>)

where PROJ is the internal counit.

266

11. Second Order Lambda Calculus

11.6.8 Lemma The isomorphism of the adjunction in corollary 11.6.7 is also natural in e; that is,

for every g: e®e', [g,c] » ( D'» Le,c1 ) = ( D'» Le,c1) » [g´id,c].

Proof For every g: e®e', and f: e´a®c1 such that

DOM » f = L-1([e,K](s) ) = s » fst

COD » f = t ( where s: e ® c0 ,t: e´a ® c0 )

([g,c] » (D'» Le,c1))(f) = [g,c] ( D'(Le,c1(f) ) )

= [g,c] ( Py" » D » <<s, t >, L(f) >0 )

= PY" » D » <<s, t >, L(f) >0 » g

= PY" » D » <<s » g , t » g >, L(f)» g >0

= PY" » D » <<s » g , t » g >, L(f » g´id) >0

= (D'» Le,c1) (f » g´id)

= ((D'» Le,c1) ([g´id,c](f) )

= ((D'» Le,c1) » [g´id,c]) (f). ¨

11.6.9 Theorem If (E,c) is an internal l 2 -model, then (E, c0 , G=[_,c]) is an external l 2 -

model. Moreover, for any legal expression Q of l2, the internal interpretation of Q in ( E,c)

coincides with the external interpretation of Q in (E, c0, G=[_,c]); t hat is, they are the same arrow

in E.

Proof Easy, by the previous lemmas. ¨

Now we prove that, using the ’internalization“ technique of chapter 7, we obtain from any external

model G:Eop ®Cat an internal model in the topos of presheaves Eop ®Set. The translation

shows that, essentially, any PL-category is nothing else but an internal category in the category of

presheaves having as object of objects the contravariant hom-functor. Recall (see definition 7.5.1)

that given an E-indexed category G: Eop®Cat , we can build an internal category G = (G0, G1,

DOM, COD, COMP, ID)ÎCat(Eop®Set) in the following way:

for all objects e, e' and arrows f: e'®e in E:

- G0: Eop®Set is the functor defined by

G0(e) = ObG(e)

G0(f) = G(f)ob : ObG(e)®ObG(e')

- G1: Eop®Set is the functor defined by

G1(e) = MorA(e)

G1(f) = G(f)mor : MorG(e)®MorG(e')

- DOM: G1®G0 is the natural transformation whose components are the domain maps in the

local categories, i.e., for eÎObE, DOMe: MorG(e)®ObG(e) is defined by

DOMe(h:s®t) = s.

- COD, ID and COMP are defined analogously, ’fiber-wise.“

267

11. Second Order Lambda Calculus

Note in particular that if (E, c0, G) is a PL category, then G0= E[_, W].

11.6.10 Proposition If (E, c0 , G) is a PL category, then G is an internal Cartesian closed

category.

Proof By proposition 7.5.4. ¨

Before showing that G also has an internal dependent product, it is useful to take a closer look at the

structure of the involved exponents in Eop®Set.

11.6.11 Lemma Let H: Eop ®Set be any functor, and let G0 = E[_, W]. Then their exponent

HG0: Eop®Set is given, up to isomorphisms, by the following data:

a. HG0(e) = H(e´W)

HG0(f) = H(f´idW);

b. eval : HG0´ G0 ® H

evale(m,f) = H(<ide, f>)(m), for eÎObE, mÎH(e´W), fÎE[e,W];

c. L : Nat[F´G0, H] @ Nat[F, HG0]

L(t)(e)(m) = te´W(F(fst)(m),snd),

where t: F´G0®H, eÎObE, mÎF(e), fst:e´W®e, snd: e´W®W.

Proof We use the usual definition of exponents in the category of presheaves (see section 3.5) and

prove that the one given above is equivalent up to isomorphisms. Remember that

HF(e) = Nat[E[_,e]´F, H]

HF (f:e'®e)(s) = s » E[_,f]´idF

where E[_,f] is the natural transformation from E[_,e'] into E[_,e] defined by E[_,f] = f » _ .

When F = G0 = E[_, W], we can use Yoneda's lemma and have

HG0(e) = Nat[E[_,e]´E[_, W], H] @ Nat [E[_,e´W], H] @ H(e´W).

Let now fÎE[e',e]:

HG0 (f) ( s ) = s » E[_,f]´E[_,idW] @ s » E[_,f´idW]ÎNat[E[_,e'´W], H] @ H(e'´W)

Hence, the Yoneda isomorphism yields HG0(f) @ H(f´idW).

Let us check that the above expressions for eval and L satisfy the equations for the exponents. We

have to prove that eval » L(t)´id = t and L(eval » h´id) = h; let mÎF(e) and fÎc0(e):

evale((L(t)e´ide)(m,f)) =

= evale(te´W (F(fst)(m), snd), f) by def. of L

= H(<ide, f>)( te´W (F(fst)(m), snd) ) by def. of eval

= te(F(<ide, f>)(F(fst)(m)), snd » <ide, f> ), by naturality of t

= te(F(fst » <ide, f>)(m), f) for F functor

= te(m, f)

268

11. Second Order Lambda Calculus

L(eval » h´id)e (m) =

= (evale´W » he´W´ide´W) (F(fst)(m), snd) by def. of L

= evale´W( he´W(F(fst)(m)), snd))

= H(<ide´W, snd>)( he´W(F(fst)(m)) ) by def. of eval

= H(<ide´W, snd>)(H(fst´idW)(he(m))) by naturality of h

= H( fst´idW » <ide´W, snd>)( he(m) ) for G functor

= H(<fst,snd>) ( he(m) )

= he(m). ¨

The following lemma exploits the results above in order to give an explicit definition of the constant

internal functor K: G ® G*, whose right adjoint will give the depended product:

11.6.12 Lemma The internal functor K = (k0 , k1 ): G® G * of definition 11.4.3 is given in

E op®Set by

k0(e) = G(fst)obj

k1(e) = G(fst)mor

where fst:e´W®e in E.

Proof Definition 11.4.3 gives the following for K

k0 = L(fst) : G0®G0G0 where fst: G0´G0®G0 in Eop®Set

k1 = L(fst) : G1®G1G0 where fst: G1´G0®G1 in Eop®Set.

Note first that, for eÎObE, the components of the natural transformations fst above behave as the

first projections. Now let hÎc0(e); then

k0(e)(h) = L(fst)(e)(h)

= fste´W( G0(fst)(h), snd ) by lemma 11.6.12, where fst:e´W®e in E

= G0(fst)(h)

= G(fst)(h).

Analogously, for any gÎc1(e):

k1(e)(g) = L(fst)(e)(g)

= fste´W( c1(fst)(g), snd )

= G1(fst)(g)

= G(fst)(g). ¨

11.6.13 Theorem Let (E, G, W) be an external model; then G is an internal model. Moreover,

for any legal expression Q of l2 , the external interpretation of Q in (E, G, W) coincides with the

internal interpretation of Q in G ; that is, they are the same arrow in E.

269

11. Second Order Lambda Calculus

Proof G is Cartesian closed, by proposition 11.6.11. By definition of an external model, the

functor G(fst) has a right adjoint ":GW®G. In view of lemma 11.6.12, this is all we need for the

proof.¨

By the previous theorem, and by the particularly simple way the category G is defined from the

indexed category (E, G, W), every external model can be thought of as an internal model. We could

even say that external models are the internal categories in the topos of presheaves that have the

(contravariant) hom-functor as object of objects (and that have the required internal structure, of

course). In this sense, external models are less general than internal ones, since they result from

fixing some data in an internal model. Note that we have also obtained a posteriori a justification of

the apparent simplicity of the external model. This is due to the choice of the well-known topos of

presheaves as ambient category and of the hom-functor as canonical object of objects for the internal

categories in this topos. This approach, though not fully general, allows a great simplification in the

definitions of the involved exponents.

A final comparison between the two approaches is suggetsted by the following remark. Note first

that any internal model in a presheaves topos ’is“ an indexed category; thus, one can think as well of

a definition of indexed category model in which also the indexing functor is not representable. On the

other hand, if the indexing functor is chosen to be representable, as in the external model, one may

wonder why only the object of objects should enjoy this privileged condition. Note that if we

suppose that also the object of morphisms is representable, i.e., c1 = E[_, W1], then by the Yoneda

embedding, we have an internal model c = ( W, W1, ...) in E.

References The polymorphic lambda calculus was defined in Girard (1971) in his investigation

of foundational problems in mathematics. Three years later it was reinvented by Reynolds (1974),

who was mainly interested in the type structure of programming languages, testifying the relevance of

this formalism for computer science. References to protoype programming languages, where

polymorphism is formalized in terms of second order l-calculi, and a recent application may be found

in Cardelli and Longo (1990).

The model definition based on the internal approach is due to Moggi (1985). Unfortunately, since

at that time there was no known concrete model that could be described ’internally,“ his idea was

never published, and for some years it remained known only to a restricted number of specialists and

collaborators (see Hyland (1987)). Meanwhile a different and in a sense simpler notion of model

based on indexed categories was proposed in Seely (1987). Both models are based on the idea in

Lawvere (1970) of expressing logical quantifications by means of categorical adjunctions. Further

discussions on categorical models of l2 may be found in Reynolds (1984), Bainbridge et al. (1987),

270

11. Second Order Lambda Calculus

Hyland and Pitts (1987), Pitts (1987), Longo and Moggi (1988), Scedrov (1988), Reynolds and

Plotkin (1988) and Meseguer (1988), among others.

This chapter is derived largely from Asperti and Martini (1989).

271

12. Examples of Internal Models

Chapter 12

EXAMPLES OF INTERNAL MODELS

In this chapter we present three examples of internal models: provable retractions inside a PER

model, PER inside w -Set, and PL-Categories inside their Grothendieck completion. The general

categorical investigation of internal models developed in the previous chapter allows a deeper and

unified analysis of the different aspects of these models, which brings, in our view, to in an original

understanding of all of them.

12.1 Provable Retractions

This example continues the analysys of an internal model of retractions developed in chapter 7 (see

examples 7.2.2.2, 7.3.9.1.)

12.1.1 Definition lb(h)p is lb(h) plus a fresh constant p such that

1. pp = p

2. (px)» (px) = px where s» r = lx.s(rx)

a» a=a

________

R.

pa = a

1+2 imply p » p = p and, hence, p is a retraction whose range contains exactly the provable

retractions: range(r) = {a | lbhp |__ ra = a }. The model constructed over this simple type-free

theory is the ’distilled“ (syntactic) version of the various models in the literature based on categories

of retractions: closures, finitary projections, etc. (see the references). It focuses on the general idea of

’types as retractions“ and, thus, clarifies the basic constructions in these models where ’type is a

type“ (i.e., p itself is a retraction). This extension of type-free l-calculus is provably non Church-

Rosser, w.r.t. the obvious reduction relation, but it is consistent (see references). Consider then the

term model of lbhp: it is an applicative structure T = (T, . ), where [M]ÎT iff [M] = { N |

lbhp |_ M = N } and [M] . [N] = [MN]. Sometimes, for semplicity, we will make no distinction

between a term and is equivalence class.

Of course, T is an extensional l-model and, thus, by theorem 9.5.10, T T @ T in PERT

(remember that by definition [M] T [N] iff lbhp |__ M = N ) .

272

12. Examples of Internal Models

It is easy to show that this isomorphism is actually an identity, that is TT = T, indeed:

[M] TT [N] iff "[P],"[Q] [P] T [Q] implies [MP] T [MQ]

iff "P,"Q lbhp |_ P = Q implies lbhp |_ MP = NQ

iff lbhp |_ Mx = Nx

iff lbhp |_ M = N

iff [M] T [N]

As already pointed out, PERT is a Cartesian closed category with all finite limits.

Let RETT = (R0, R1, dom, cod, comp, id)ÎCat(PERT) be the internal category of retractions

on T. As we proved in the example 7.3.9.1, RETT is Cartesian closed; we want to prove that

RETT yields an (internal) l2-model.

We start by giving the explicit definition of R0 and R1. Remember that in PERT the equalizer

of a pair of morphisms f,g: P ® Q is (E, h: E®P) where aEb iff ( aPb and f(a)Qg(b) ) and

h is the injection from E to P. Note also that dom(E) = dom(P) Ç {a | f(a) Q g(a)}, and on this

domain E coincides with P. Then it is easy to verify that [M] R0 [N] iff ( [M] T [N] and lbhp

|_ M » M = M.) In other words R0 coincides with T but is restricted to those terms which are

provable retractions.

The domain of R1 are (lbhp-equivalence classes of) triples <M, F, G>, where < , > is the

standard encoding of tuples in l-calculus, F and G are provable retractions, and M is a morphism

from F to G, that is, lbhp |__ G » M » F = M. Formally:

dom(R1) = { [<M, F, G>] | F » F =lbhp F ; G » G =lbhp G ; G » M » F =lbhp M },

[<M, F, G>] R1 [<M', F', G'>] iff [<M, F, G>] T [<M', F', G'>]

Note moreover that [<M, F, G>] T [<M', F', G'>] iff M =lbhp M', F =lbhp F', G =lbhp G'.

Let RETT* = (R0R 0, R1R 0, dom*, cod*, comp*, id*) be as in definition 11.4.2. We must

prove that the costant functor K: RETT ® RETT * has a right adjoint " = ("0: R0R0®R0, "1:

R1R0®R1). "0 is the function realized by lFlzt.F(pt)(z(pt)). Thus, we need to show that

1. if F is in the domain of R0R0 then "0(F) is in the domain of R0 ;

2. "0 takes elements that are equivalent in R0R0 to elements that are equivalent in R0.

As for (1) we have

"0F » "0F = lx( lzt.F(pt)(z(pt)) )( lt.F(pt)(x(pt)) )

= lx( lt.F(pt)( lt.F(pt)(x(pt)) (pt)) )

= lx( lt.F(pt)( F(pt)(x(pt))) )

= lxlt. F(pt)(x(pt)) because F(pt) is a retraction by hypothesis

= " 0F

(2) is evident.

An element in R1R0 is a triple < T, F, G >, where F and G are in the domain of R0R0, T

is in the domain of T R0 , and for every retraction M, one has TM = GM » TM » FM.

273

12. Examples of Internal Models

" 1 is the function that takes (an equivalence class in R1R 0 of) a triple < T, F, G > in (the

equivalence class in R1 of) the triple < ltlm .T(pm)("0Ft ),"0(F), "0(G) >.

Note that ltlm .T(pm)("0Ft )) is a morphism from the retraction "0F to the retraction "0G;

indeed,

"0G » ltlm .T(pm)("0Ft ) » "0F =

= lz."0G(lm .T(pm)("0Fz) )

= lz. (lxlt.G(pt)(x(pt)) ) (lm .T(pm)("0Fz) )

= lz. lt.G(pt)( (lm .T(pm)("0Fz) ) (pt))

= lz. lt.G(pt)( (T(pt)("0Fz) )

= lz. lt.T(pt)("0Fz) because G(pt) » T(pt) = T(pt) by hypothesis

It should be clear that " 1 is indeed a morphism in PERT its realizer is simply obtained by

abstraction on < T, F, G >.

Given a variable type G in R0R0 and a type N in R0, the projection projG(N) from "0G

to G(N) is realized by the term lx.xN. Indeed, if S has type "0G that is, S = ("0G)S, then

SN = "0GSN = G(N)(SN), and thus SN has type G(N).

We define now the isomorphism D of the adjunction.

Let < T, lx.M, G > be an element in R1R0, where M is a retraction and lx.M = K0(M).

Define then DM,G( < T, lx.M, G > ) = < ltlm .T(pm)t, M, "0G >.

Conversely, given < S, M, " 0 (G) > in R1 , define D M,G -1 ( < S, M, " 0 (G) > ) = <

lmlt.Stm, lx.M, G >. Note that lm.lt.Stm = lm.(lx.xm » S) = lm.( projG (m) » S ). Thus,

for every retraction N, one has

G(N) » lt.StN » M = projG(N) » S » M = G(N) » projG(N) » S » M = lt.StN .

Moreover,

DM,G-1( DM,G( < T, lx.M, G > ) ) =

= DM,G-1( < ltlm .T(pm)t , M, "0(G) > )

= < lmlt.T(pm)t, lx.M, G >

= < lm.T(pm), lx.M, G >

and clearly T and lm.T(pm) are equivalent in T R0.

As for the converse, note first that if S = "0(G) » S, then

St(pm) = "0(G)(St)(pm) = (lm.G(pm)(St(pm)))(pm) = G(pm)(St(pm)) = Stm

DM,G( DM,G-1( < S, M, "0(G) > ) ) =

Thus:

= DM,G( < lmlt.Stm, lx.M, G > )

= < ltlm .St(pm) , M, "0G >

= < ltlm .Stm , M, "0G >

= < S, M, "0G >

274

12. Examples of Internal Models

Define then

D ( < M,G, < T, lx.M, G > > ) = < M, G, < ltlm .T(pm)t , M, "0G > >

and

D-1( < M,G, < S, M, "0G > > ) = <M,G, < lmlt.Stm, lx.M, G > >.

12.1.2 Remark It is possible to give an elegant categorical characterisation of the models of

lb(h)p. Let A be a reflexive object ( AA @ A ) in some category C, and let RETA = (R0, R1,

dom, cod, comp, id) be the internal category of retractions on A in PERA. Let x: R0®AA be as

usual the equalizer of the identity and lf. f » f. All we need to turn RETA in a model for lb(h)p

is that there exist p: AA®R0 such that R0 is a retract of AA via (x,p). Then, in a sense, since

R0 represents all the retractions on A, we can say that the collection of objects of RETA is itself an

object of RETA: more formally, that RETA is internal to RETA w.r.t. PERA. We have thus the

following facts:

1. (AA < A in a CCC C and RETA internal to RETA with respect to PERA )

imply A |= lbp .

2. A |= lbp implies

( AA < A in PERA and RETA internal to RETA w.r.t. PERA ).

The reader should complete the details for exercise.

12.2 PER inside w -Set

This example continues our presentation of PER an an internal category M of w -Set (see examples

7.2.7 and 7.3.9.2, where it is shown that the construction gives also an internal model.)

Let M * be defined as c* in 11.4.2. We next define an internal right adjoint to the constant

functor K : M ® M*, that by def. 11.4.4 will complete the construction of a model for l2.

Again, we shall take advantage of the wise blend of set-theory and computability on which w-Set

is based, in order to avoid the most formal details.

The following lemma motivates the definition of " below.

12.2.2 Lemma If <t,F,G>Îw -Set[M o,M 1] then $n "AÎM o t(A) = {n}F(A)®G(A) .

w

Proof. Suppose that m |__ <t,F,G>. Since 0 |__ A for any AÎPER , then take n = m.0 and

observe that n |__ <t(A),F(A),G(A)>. Thus t(A) = {n}F(A)®G(A). ¨

As for the definition of "0, observe that the intersection of any collection {Ai}iÎI of objects in

PER is still in PER, by viewing them as sets of pairs (of numbers). That is, set

n (Ç iÎI Ai) m iff "iÎI (n Ai m ).

275

12. Examples of Internal Models

12.2.3 Definition

1. "o : [Mo ® Mo] ® Mo, is given by "o(F) = ÇAÎMoF(A),

2. " 1 : [M o ® M 1 ] ® M 1 is defined as follows. If m |_ <t,F,G>Îw -Set[M o ,M 1 ], set

w

"1(<t,F,G>) = <{m.0}"o(F)®"o(G) ,"o(F),"o(G)> .

12.2.4 Proposition. " in definition 12.2.3 is well defined. In particular, "1 is realized by any

number p such that , for all m , p.m = m.0 .

Proof. By definition, if F : M o®M o, then " o(F) is in M o. " o is realized by (any index of)

any total recursive function. By lemma 12.2.2, "1 is well defined as its definition does not depend

on the choice of the realizer m for <F,t,G>. Therefore we only need to show that "1 is realized

by p. Namely, that if

1. m1,m2 |__ <t,F,G>

2. n1 "o(F) n2

3. AÎMo

then one has (p.m1.n1) G(A) (p.m2.n2). Indeed,

4. p.m1 = m1.0 (F(A)®G(A)) m2.0 = p.m2 , by (1)

5. n1 F(A) n2 , by (2) and (3),

and thus (p.m1.n1) G(A) (p.m2.n2) by (4), (5) and the definition of (F(A)®G(A))ÎMo. ¨

12.2.5 Remark. It should be clear that lemma 12.2.2 is a very simple but crucial lemma. Note

first that the morphisms in w -Set[M o,M 1] are described as triples, <t,F,G>, where t: M o ®

ÈAÎMoQ(F(A)®G(A)) is such that t(A)ÎQ(F(A)®G(A)) and F, G: Mo ® Mo give the source

and target of t(A). This is a sound description, since M* = ( [Mo®Mo], [M1®M1],...) may be

viewed as the internal category of functors from the discrete category, whose object of objects is Mo,

to M. Thus [M o ®M 1 ] or w -Set[M o ,M 1 ] are internal natural transformations. By lemma

12.2.2, now, there is a uniform n which realizes t(A) for all A. In a sense these internal natural

transformations are ’almost“ constant maps and only depend on the source and target objects.

We need now to prove that there exists an internal natural isomorphism D, which gives the

adjunction between " and K. We can use the simplicity of the intended universe and perform the

construction directly. As in the proof of the internal Cartesian closure of M, the point is to show that

the functional dependencies, usually implicit in the external world (or given by ’indexes“: recall a,b

|_ La,b), can be turned into internal constructions. Once more, this will be straightforward to check

within w -Set, as the realizers for the natural isomorphism and its inverse will not depend on their

’indexes.“

Let K, with components ko and k1, be the internal constant functor in definition 11.4.3.

276

12. Examples of Internal Models

12.2.6 Definition. For m |__ < t,ko (B),G>Îw -Set[M o ,M 1 ] , set

w

DB,G (< t,ko(B),G>) = < {m.0}B®"o(G) ,B,"o(G)> ÎM 1 .

D-1B,G ( <{m}B®"o(G) ,B,"o(G)> )

and

= < lXÎM o .{m}B®G(X) ,ko (B),G>Îw -Set[M o ,M 1 ].

w

12.2.7 Proposition. D B,G and D -1 B,G in 12.2.6 are well defined, for all BÎM o . and G:

M o®M o (= [M o ® M o]). Moreover, they are realized by p and k (respectively), such that

p.m = m.0 and k.m.n = m .

Proof: By lemma 12.2.2, DB,G does not depend on the choice of the particular realizer m. As for

D -1 B,G , note that, if m(B®" o (G))m, then "n,q ( nBq Þ m .n (Ç AÎMo G(A)) n.q), by

definition of "o, and hence m.n G(A) n.q, for all AÎMo. Therefore, m (B ® G(A)) m for all

AÎMo and D-1B,G too is well defined. By definition, they are uniformly realized by p and k

as above. In particular, p and k compute DB,G and D-1B,G for all B and G. ¨

12.3 PL-Categories Inside Their Groethendiek Completion

This example show another way for obtaining an internal model from a PL-category, different from

the internalization process of chapter 11.

12.3.1 Definition. Given any E-indexed category G, define the category ò G, the Grothendieck

completion of G, having as objects the pairs (e, s) with eÎObj E and sÎObj G(e) and as

morphisms pairs (a, f) such that:

(a, f)ÎòG[(e, s), (e', t)] iff aÎE[e,e'] and fÎG(e)[s,G(a)(t)].

The identity of (e, s) is (ide , ids ); the composition of (a, f)Î ò G [(e,s),(e',t)] and (b,

g)Îò G[(e',t), (d,r)] is (b, g) » (a, f) = ( b » a, G(a)(g) » f).

ò

Let (E, G, W) be an external model (that is an indexed category with the additional requirements

on functor G in 12.2.1); then the Grothendieck completion òG assumes a particularly simple form

Objects: (e, s)Îò G iff sÎObjG(e) = E[e, W]

ò

(hence we can identify objects of òG with arrows s: e®W)

Morphisms: (a,f)Îò G[s:e®W,t:e'®W] iff

ò

aÎE[e,e'] and fÎG(e)[s,G(a)(t)] = G(e)[s,t » a].

The point is that ò G contains an internal category which, in a sense, internalizes the external model

(E, G, W).

277

12. Examples of Internal Models

Warning We are here forcing our terminology, since the category ò G does not need to have all finite

limits, at least not in general, and hence we could not speak of ’internal categories in ò G.“ However,

all the needed pullback diagrams exist in òG, as pointed out below.

The internal category G = (c0, c1, DOM, COD, COMP ,ID)ÎCat(òG) is defined as follows:

ò

c0 = tG(W) : W®W the terminal object in G(W)

c1 = [,]0 : W´W®W [,]0 is given in lemma 11.2.3

DOM = (fst, !) ! is the unique arrow from c1 to c0»fst in G(W´W)

COD = (snd, !)

ID = (<idW, idW>, LG(W)(snd)) sndÎG(W)[tG(W)´idW, idW], hence

L(snd)Î G(W)[tG(W), idW®idW], where idW®idW

The situation for COMP is more delicate, since ò G does not have all finite limits. However, the

pullback of DOM: c1®c0, COD: c1®c0 does exist, and it is given by

c2 = (p2®p3)´(p1®p2),

where product and exponents are in the fiber G(W´W´W) and piÎE[W´W´W, W]; the pullback

projections •1, •2 : c2®c1 are

•1 = (<p2,p3>, id)

• 2 = (<p1,p2>, id).

In order to define COMP, remember that in any CCC, given three objects A, B, C, there exists a

morphism cmpÎHom[CB´BA, CA] that internalizes the composition, namely

for p: (CB´BA)´A®CB´(BA´A) an isomorphism.

cmp = L(eval » id´eval » p)

Define then

COMP = (<p1,p3>, cmp) for cmpÎG(W´W´W)[ c2, p1®p3]

(recall that, in G(W´W´W), p1®p3 = [,]0 » <p1,p3>).

The verification that these data define an internal category is straightforward.

We now prove that if (E, G, W) is an external model, than òG is Cartesian closed.

The terminal object is given by tG(t), the terminal object of the local category G(t) (for t terminal in

E). As for products, they can be defined by using the Cartesian structure of the local categories:

(f:e®W)´òG(g:d®W) := x0 » f´Eg, where x0: W´W®W is the arrow obtained in lemma 11.2.3;

hence f ´òG g = (f » fst)´G(e´d)(g » snd). Projections are obtained as follows. We need FST:

c0´c0®c1, where FST = (a, f) for some a:W´W®W´W and fÎG(W´W)[c0´c0, c1» a]. As for

a, which intuitively takes a pair of objects (s, t) to (s´t, s), we can take a = <x0 , fst>:

W´W®W´W.

In order to define fÎG(W´W)[ tG(W´W), x0 ®fst], we can use again the Cartesian closed

structure of G(W´W) and the fact that, by lemma 11.2.3, one has

x0 = x0 ° id = x0 ° <fst,snd> = fst ´G(W´W) snd.

Define then f = L(fst) where fstÎG(W´W)[fst´snd, fst]. SND is defined analogously.

278

12. Examples of Internal Models

It remains to give the pairing isomorphism <,>; note first of all that the required pullbacks (see

definition 7.3.6, and also appendix A at the end of chapter 7) are given by the following data:

X = [,]0´òG[,]0 » <id´fst, id´snd> : W´(W´W)®W

•X : X®c1´c1 (that is X ® [,]0 ´òG [,]0)

•X = ( <id´fst, id´snd>, id )

r : X ® c0´c0´c0 (that is X ® tG(W´W´W))

r = (id, !)

Y = [,]0 » id´x0 : W´(W´W)®W

•Y : Y®c1 (that is Y ® [,]0 )

•Y = ( id´x0, id)

r' : Y ® tG(W´W´W)

r' = (id, !)

Observe now that, as we are dealing with objects of G(W´(W´W)), by interpreting all products and

exponentials locally in G(W´(W´W)) ), one has

X = (fst ® fst » snd)´(fst ® snd » snd)

Y = fst ® ((fst » snd)´(snd » snd))

and hence X @ Y, since G(W´(W´W)) is Cartesian closed.

The isomorphism < , > : X® Y (in ò G ) is then given by < , > = (id,f), where f is the

isomorphism between X and Y in G(W´(W´W)). The required equations are now easily verified.

Let us now come to the exponents Þ0 = ( [,]0 , !) : c0´c0®c0, where [,]0 is given again by

lemma 11.2.3.

EVAL : c0 ´ c 0 ® c 1 is given by a pair: EVAL = (a ,f), for a :W ´ W ® W ´ W and

fÎG(W´W)[c0´c0, c1» a]. As for a, whose intuitive content is to send a pair of objects (s, t) into

(ts´s, t), we can set a = <x0 » < [,]0, fst>, snd>.

We need now fÎG(W´W)[tG(W´W), [,]0 » <´0 » < [,]0, fst>, snd>]; observe that

[,]0 » <x0 » < [,]0, fst>, snd> =

= (x0 » < [,]0, fst>) ® snd in G(W´W)

= ([,]0 ´ fst) ® snd

= ((fst®snd) ´ fst) ® snd.

Take then evalfst,sndÎG(W´W)[(fst®snd) ´ fst, snd] and set

f = L(evalfst,snd)ÎG(W´W)[tG(W´W), ((fst®snd) ´ fst) ® snd].

Before giving the isomorphism L, we need to express the pullback diagrams of theorem 7.3.7 (see

also appendix A). They can be instantiated as

279

12. Examples of Internal Models

where:

X' = [,]0 » (x0´ idW) Y' = [,]0 » ( idW ´ [,]0 )

•X' = ( x0´ idW, id) •Y' = ( idW´[,]0, id)

s = (idW´W´W, !) s' = (idW´W´W, !)

As before, observe that

X' = fst´(fst » snd)®(snd» snd)

Y' = fst ® ((fst » snd)®(snd» snd)).

Therefore X' @ Y', by the Cartesian closure of G(W´(W´W)) .

The internal Cartesian closed category GÎCat(ò G) is actually an internal model when (E, G, W) is

ò

an external one. In order to define the required adjunction, we need first to show that we can indeed

construct the internal category G*; that is, the exponents c0c0 and c1c0 exist in ò G (as for the

limits, not all the exponents exist in òG).

12.3.2 Lemma

i. For any object e of E, c0tG(e) exists in ò G and it is given by tG(We).

ii.For any object e of E, c1tG(e) exists in ò G and it is given by "([,]0 » eval).

Proof Set s = tG(e).

i. Note first that in ò G, for any e' and t, every arrow (b,g):t®tG(e') has g = !. We must then

show that, for c0s = tG(We), the following diagram commutes, for any object t and arrow (a,!):

which is immediate.

280

12. Examples of Internal Models

ii. Let t: e'®W be any object of ò G; we are looking for the unique L(a, f) such that the following

diagram commutes:

Since a: e'´e®W´W, if we set L(a,f) = (a,f), a natural choice for a is a = L(a):e'®(W´W)e.

Moreover, for (a, f):t´s®[,]0, we have the following:

fÎG(e'´e)[t´s, [,]0»a ] @

@ G(e'´e)[t» fst, [,]0» a] by s = tG(e) and the definition of product in òG

@ G(e')[t» fst, "([,]0» a)] via the isomorphism D of the adjuction giving the

external model

@ G(e')[t» fst, "([,]0» eval) » L(a)] by naturality of ".

We can then define

c1s = "([,]0 » eval) : (W´W)e®W

and take f = D(f); the previous diagram then commutes for eval = (eval, projc0s).

We can eventually give the data for the adjunction

"0 : c0c0 ® c0

"0 = ("0 : WW ® W, !).

As for PROJ = (a, f): c0c0®c1c0, we need a : WW®(W´W)W and fÎG(WW)[c0c0, c1c0» a].

For eval : WW´W®W and fst: WW´W®WW, set a = L(<"0 » fst, eval>). As for f, note first that

c0c0 = tG(WW)

and

c1c0» a = "([,]0 » eval) » L(<"0 » fst, eval>)

= "([,]0 » <"0 » fst, eval>) by naturality of "

= "(("0 » fst) ® eval) by the usual isomorphims.

We are then looking for fÎG(WW)[tG(WW), "(("0 » fst) ® eval) ]; as we did in the proof of the

previous lemma, let us look for an arrow hÎG(WW´W)[tG(WW)» fst, ("0 » fst) ® eval]. Then the f

we need will then be D(h). Observe now that projevalÎG(WW´W)["0 » fst, eval]; this immediately

gives the required h in the following diagram:

281

12. Examples of Internal Models

In conclusion, the Grothendieck completion provides yet another example of the general categorical

construction of model in chapter 11. Moreover, it gives further insight into the external versus

internal approach by giving a setting where the external models may be viewed as internal

constructions.

References The examples in this chapter may be found, in part, in the many papers mentioned at the

end of the previous chapter. Since Moggi's hint for the small completeness of the PER construction,

in particular, these models have been thoroughly explored by many authors. The three sections above

develop the ideas in Amadio and Longo (1986) and in Longo and Moggi (1988), and follow Asperti

and Martini (1989), respectively. By this, the first two sections extend to higher order the