<<

. 9
( 10)



>>

This calculus was later rediscovered by Reynolds and, since then, it has received great attention,
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

<<

. 9
( 10)



>>