<<

. 8
( 10)



>>

typable and, if so, assigns a type to it (actually, the ’most general type“).
This effective interactive feature of ML provides a partial check for correctness, as one may
automatically control whether type errors occur. This is similar to what physicists call ’dimensional
analysis“ for equations when they verify, say, whether a force faces a force, etc. Of course, a lot
must be settled. For example, the actual decidability of the type assignment and the existence of ’type
schemes“ such that all types of a given program are instances of these. The identity function, for
example, has type A ® A for all instances of A.
As for the semantics, one must first be able to interpret the type-free language, as handled by the
programmer, and then interpret types as objects of suitable CCC constructed over the type-free
model. In other words, one must be able to obtain an interpretation of types out of a model for the
type-free calculus. ’Soundness“ then means that a program, once it is assigned a type, is actually
interpreted as an ’element“ of the interpretation of its type. Decidability and soundness have been
positively clarified by a mathematical investigation of computability and programming, which goes
beyond the scope of this book (see references).




220
9. Reflexive Objects and the Type-Free Lambda Calculus


Our present purpose is to survey the main ’type structures“ (categories) one may construct out of
type-free models and to complete, in this way, the categorical understanding of typed versus type-free
calculi, as required for the semantics of the type assignment process. Most of the work may be done
over an arbitrary combinatory algebra (X, . ), i.e., over an arbitrary model of Combinatory Logic.
Indeed, it is even not required that "." , the application in X, is a total operation. As already
mentioned, if ’.“ is not always defined, (X, .) is no longer a model of CL. However, the
categories constructed below still have the same properties (products, exponents, whenever
possible...), which the reader should check as an exercise.

9.5.1 Definition Let A = (X,.) be an applicative structure.
i. The set of monomials over A is inductively defined by
x,y....x1,x2...(variables)...are monomials
a,b....a1,a2....(constants from X )... are monomials
MN is a monomial if M and N are monomials.
Substitution of constants for variables, i.e. M[a/x], in monomials is defined by induction in the usual
way. M1M 2...Mn stands for (...(M1M 2)...Mn) .
ii. f: Xn®X is algebraic if f(a) = M[a/x] for some monomial M and any a = (a1,... ,an)ÎXn
and x of length n. (That is, the set P n(A) = P[Xn,X] of algebraic functions of n-arguments is
defined by the monomials over X, with at most n variables, modulo extensional equality.)
iii. Given (X,.), call f : Xn ® X representable if $aÎX "bÎX n f(b)= a.b 1 .....b n .


By using algebraic functions, one may define a simple category over an arbitrary applicative
structure.

9.5.2 Definition Let A = (X, .) be an applicative structure. The category P A of polynomials
over A, has as
XnÎPA, for all n Î w;
objects:
morphisms: fÎPA[Xn,Xm] iff f: Xn®Xm and "i<m prmi°fÎPn, with prmi i-th projection.
(If there is no ambiguity write P[Xn,Xm] for PA[Xn,Xm]).

For example, f(x,y) = (xb(xax),yxa) for a,bÎX, is in P[X2,X2]. By substitution, one may easily
show that morphisms are closed under composition; moreover, prniÎP[Xn,X] = Pn and, thus, PA
is a category.

Exercise (Curry-Shoenfinkel) Prove that exactly in combinatory algebras every algebraic function
is representable (hint: use the argument which translates a l-term lx.M into an S-K-term <x>M in
the introduction).



221
9. Reflexive Objects and the Type-Free Lambda Calculus




If A is a combinatory algebra, then, by the exercise, P A may be considered the category of
representable morphisms.

9.5.3 Lemma Let A = (X,.) be an applicative structure. Then P A is a cartesian category with
enough points. Moreover, if C is a CC with enough points and C, U and A(u) are as in definition
9.2.1, then PA(u) is a full sub-cartesian category of C.
Proof. Set Xn ´X m = Xn+m and T = X0 (= a singleton set) for the terminal object. The
projections pri 's are given above. Clearly, PA has enough points. The rest easily follows from
definition 9.2.1 and the assumption that C has enough points. The reader may complete the proof as
an exercise. ¨


Given a category C, U and A(u) as in lemma 9.5.3, we say that gÎC[U n ,U] induces f :
A(u)®A(u) if f(h) = g° h for all hÎC[T,U]. It is straightforward to prove that all algebraic
functions defined by a monomial in n variables over A(u), and no constants, are induced by
morphisms in C[Un,U]. One only has to interpret variables as projections (see section 9.3) and
argue by induction on the structure of the ’algebraic term“ defining the function. For example, for
f(x1,x2,x3) = (x3.x1).x2 write
u°<pr3,pr1> : U3 ® U´U ® U , which is x3.x1 , and then
u°<u°<pr3, pr1>,pr2> : U3 ® UxU ® U, which induces f.
Next, we generalize a definition of category given over a specific applicative structure in example
3.4.1. The definition is slightly different (besides being more general). Since it is an important
construction, it is worth seeing it again, under a different and more general viewpoint.

9.5.4 Definition Let A = (X,.) be an applicative structure. Define then:
1. The category PER A of partial equivalence relations given by:
objects: RÎPERA iff R is an equivalence relation on a subset XR of X, i.e., XR = dom R
= range R.
morphisms: for RÎPER A let pR (n) = {m | nRm }; then fÎPER[R,S] iff $f'ÎP[X,X] f ° pR
= pS ° f' on XR, i.e., the following diagram commutes:




(we then say that f' computes f ).



222
9. Reflexive Objects and the Type-Free Lambda Calculus


2. The category ER A of (total) equivalence relations is given as above by using equivalence
relations on X (i.e., XR = X in 1.).


PERA and ERA are clearly categories. Similarly as for PA we write (P)ER[R,S] for (P)ERA[R,S]
when unambiguous.


Exercise Let A be an applicative structure. Give a terminal object for PERA and ERA, and prove
that they have enough points. (Hint: recall that the constant functions are algebraic).

9.5.5 Proposition Let A = (X,.) be an applicative structure. Then, if X´X < X in P A , ER A
and PERA are CCs (with enough points). Moreover, PA and ERA are full sub-CC's of PERA.
Proof Let X´X < X via ([-,-],<p1,p2>). Then R´S may be defined componentwise, by
a(R´S)b iff (p1(a))R(p1(b)) and (p2(a))S(p2(b)).
This turns ERA and PERA into CC's.
Observe now that "n Xn < X via ([-,...,-],<p1,...,pn>) in PA, by iterating X´X < X. Thus
PA may be faithfully embedded in PERA by taking, for each Xn, the identity relation restricted to
the image of Xn in X via [-,...,-]. Call this restricted identity idn. Moreover, P A is full in
PERA, since P[Xn,Xm] @ PER[idn, idm], as sets, by the following isomorphism G (take m =
1, for the sake of simplicity). Let gÎP[Xn,X], then, for x = [x1,...,xn], define G(g)ÎPER[idn,
id] by G(g)(x) = g(p1 (x),...,pn (x)) = g(x1 ,...,xn ). G(g) is computed, in the sense of 9.5.4, by
g°<p1,... ,pn> : X ® Xn ® X.
G is an isomorphism, whose reverse map is given as follows: if hÎPER[idn, id] is computed
by h'ÎP[X,X], then G-1(h) = h'°[-,... ,-] : Xn ® X ® X. By definition, ER A is a full sub-CC
of PERA, and both categories have enough points, by the exercise. ¨


The next theorem proves the converse of theorem 9.2.5 and, moreover, it shows that, by applying
the construction in definition 9.2.1 and theorem 9.2.5 to a combinatory algebra, one gets back to the
given combinatory algebra.


9.5.6 Theorem Let A = (X,.) be a combinatory algebra and PA be the category of polynomials
over A. Then T < X, XxX < X in P A and, for u(x,y) = x.y, uÎP[X 2 ,X] is K-universal in the
category PA. Moreover, A(u) = A.
Proof T < X trivially holds, for X¹Æ. Clearly, XxX exists in P A , by lemma 9.5.3. Let then
c,c1,c2ÎX represent lxyz.zxy, lxy.x, lxy.y, respectively, in the sense of definition 9.5.1(iii). c
is the element that codes pairs (they are commonly coded in this way in l-calculus), while c1, c2
will be used to define projections. Thus, for [x,y] = cxy and pi(x) = xci, one has [-,-] ÎP[X2,X],
piÎP[X,X] and X´X < X via ([-,-],<p1,p2>). Finally, assume that fÎP[X2,X] and that aÎX



223
9. Reflexive Objects and the Type-Free Lambda Calculus


represents f. Then f = u°((lx.ax)´id) and, hence, u is K-universal. It is easy to check from the
definition that A(u) = A. ¨


9.5.7 Corollary Let A = (X,.) be an applicative structure. Then A is a combinatory algebra iff,
in PA, one has T < X, X´X < X and, for u(x,y) = x.y, u is K-universal.
Proof (Þ) by theorem 9.5.6; (Ü) by theorem 9.2.6. ¨


As already pointed out, one needs CCC's in order to take care of l-models. However, also
combinatory algebras are tidely characterized within CCC's. The following immediate consequence
of theorem 9.5.6 and proposition 9.2.6, plus proposition 9.2.7, fully characterizes the least
requirement for functional completeness in CCC's.


9.5.8 Corollary Let A = (X,.) be a combinatory algebra. Then PERA is a CCC, where T < X,
X´X < X and, for u(x,y) = x.y, L(u)ÎPER[X,XX] is principal. Moreover A(u) = A.
Proof. In view of theorem 9.5.6 and proposition 9.5.5, we only need to define the object SR in
PERA, which represents PER[R,S]. Set then
aSRb iff "x,yÎX (xRy Þ (ax)S(by)).
Recall now that, by assumption, each function in P[X,X] is representable. The rest of the proof that
PERA is a CCC is an obvious generalization of example 3.4.1. ¨

9.5.9 Remark While completing the proof that PER A is a CCC, in corollary 9.5.8, one may
notice that it is only required, for all R, S and all fÎPER[R,S], that f has a representative in X.
This is the point which allows the generalization to the partial case (see section 9.6, besides PERw in
example 3.4.1).


The next result proves the converse of corollary 9.1.12 and completes our categorical understanding
of l-models.


9.5.10 Theorem Let A = (X, ., e) be a l-model. Then, in the CCC PER A , there exist
yÎPER[XX ,X] and fÎPER[X, XX ] such that XX < X via (y, f). Moreover, (X,.) @ A(L-
1(f)), and e = y(y°f). If A is extensional, then XX @ X .
Proof Let fÎPER[X,X] and aÎX be a representative for f. Define then y(f) = ea. By (e2), y
is well defined. Recall also that XX is the exponent representing PER[X,X] in PER A , hence
yÎPER[XX ,X].
As for f, define f(a) = lx.ax for any aÎX. Clearly fÎPER[X,XX]. Compute then
if a represents f
f(y(f)) = lx.eax
=f by (e1).



224
9. Reflexive Objects and the Type-Free Lambda Calculus


Thus XX < X, via (y, f).
Finally, (X,.) @ A(L -1 (f)), since f(a)(b) = ab. Moreover y(f(a)) = ea and, hence, e
represents y°f. Thus
by definition of y
y(y°f) = ee
by (e3).
=e
Finally, if a = ea = y(f(a)) for all a , then y°f = id and, hence, XX @ X. ¨


We conclude this part by summarizing the connections between type-free l-calculus and categories
with enough points obtained so far. This provides a unified framework for the topic.

9.5.11 Theorem Let C be a CCC and A an object of C. Then
1. AA @ A Þ A is an extensional l-model;
2. AA < A Þ A is a l-model;
3. $pÎC[A, A A] principal, T < A and A´A < A Þ A is a combinatory algebra.
Conversely,
1. A is an extensional l-model Þ AA @ A in PERA;
2. A is a l-model Þ AA < A in PERA;
3. A is a combinatory algebra Þ $pÎPERA[A,A A] principal, T < A and A´A < A in PERA.

9.5.12 Remark In the categorical semantics of lambda calculus, we have to deal with Cartesian
(closed) categories, and thus with products and projections. Without much increasing the complexity
of the semantics, it is thus possible to consider also a type-free l-calculus with explicit pairing,
lbhp, in analogy to the typed case, see section 8.2. We leave to the reader the task of defining, as an
exercise, this calculus and giving its semantics on a reflexive object U in a CCC C. As a matter of
fact, one only needs to add A´A @ A to (1) and (2) in theorem 9.5.11 in order to obtain
characterizations of the models of lb(h)p.
In conclusion, the diligent reader will notice that the models of lbhp are exactly the CCC with
e.p. and with a unique object nonisomorphic to the terminal one. It may be fair, then, to call lbhp
the ’unityped“ l-calculus.




9.6 Typed and Applicative Structures: Applications and Examples
In the first part of this section, we sketch a recent application of the typed and type-free l-calculus to
category theory. In a sense, this application goes in the other direction with respect to our prevailing
perspective, as, so far, we mostly applied categorical tools to the understanding of deductive systems
and their calculus of proofs (l-calculus).




225
9. Reflexive Objects and the Type-Free Lambda Calculus


The question we answer here may be simply stated, in categorical terms:
(1) which isomorphisms hold in all CCC's ?
The motivation is clear, as a simple and decidable equational theory of types will allow us to detect
provably isomorphic types or, equivalently, valid isomorphisms in all models. In functional
programming, for example, when retrieving programs from a library where they are collected
according to their types, the search should be done ’up to provable isomorphisms“, as the same
program may have been coded under isomorphic types; for example, a search program for lists of a
given length, may be typed by INT´LISTS ® LISTS or, equivalently, by LISTS® (INT ®
LISTS) (see references). The result turns out to be an application of l-calculus to categories, as we
look at the problem from a proof-theoretic view point and, by the work done in chapter 8, we actually
answer to the following equivalent question.
Consider the intuitionistic calculus of sequents, in section 8.3, and suppose that proofs of Aú¾
B and of Aú¾ B are given. Then one may ask
(2) in which cases the composition of Aú¾ B and Bú¾ A (and of Bú¾ A and Aú¾ B)
reduce, by cut-elimination, to the axiom Aú¾ A (and Bú¾ B, respectively) ?
Clearly, (2) corresponds to (1) when types are understood as objects. The point is that the
deductions in (2) are coded by l-terms, M and N, say, as described in section 8.3. By this, and
by a lot of (hinted) hacking on l-terms, we will characterize valid isomorphisms by looking at the
structure of M and N such that M°N = IA and N°M = IB, by b-conversion.

The second part develops little general Category Theory since it essentially gives more examples of
CCC's and of l-models. The structures presented will be combinatory algebras and models of type-
free lb, since models of lbh may be derived from the general results in chapter 10. In particular,
we introduce a few relevant categories of complete partial orders as well as their ’effective“ versions
and hint how they relate to the various categories of quotients or PER's that we largely used in the
previous sections.



Part 1: Provable isomorphisms of types
Consider the following equational theory of types. It is given by axiom schemata plus the obvious
inference rules that turn ’=“ into a congruence relation.


Definition Th is axiomatized as follows, where T is a constant symbol:
9.6.1
1. A´T=A
2. A´B=B´A
3. A ´ (B ´ C) = (A ´ B) ´ C
4. (A ´ B)® C = A ® (B ® C)



226
9. Reflexive Objects and the Type-Free Lambda Calculus


5. A® (B ´ C) = (A ® B) ´ (A ® C)
6. A®T = T
7. T®A = A.

In remark 3.3.3, we already asked the reader to prove that, when ® and ´ are interpreted as
cartesian product and exponent, the provable equations of Th hold as isomorphisms in any CCC.
Note, though, that there are categorical models which realize Th, but are not CCC's. Take, say, a
cartesian category and a bifunctor ’®“ that is constant in the second argument.
We next hint how to prove the non trivial fact that Th characterizes exactly the valid
isomorphisms in all CCC's, by using l-calculus.
As pointed out in section 8, the typed l-calculus is, at the same time:
a - the ’theory“ of CCC's;
b - the calculus of proofs of the intuitionistic calculus of sequents.
Thus the theorem is shown by observing that the isomorphic types in the (closed) term model of
typed l-calculus are provably equal in Th . This answers to (2) in the introduction above and, thus,
to (1).
A term model is closed, when terms in it contain no free variables.


9.6.2 Definition Given (an extension of) the typed l-calculus, l , the (closed) term model is the
type structure
|l| = {| M: A| / M is a (closed) term of type A}
l
where |M: A| = { N / l ú¾ M = N }.

Clearly, the type structure is non trivial, if a collection of ground or atomic types is given. The (pure)
l-calculus may be extended by adding fresh types and constants as well as consistent sets of
equations. Consider now the extension of lbhpt in section 8.3 by adding:
1 - a special atomic type T (the terminal object);
2 - an axiom schema
*A: A ® T
which gives a constant of that type;
3 - a rule
M: A ® T
_______
M = *A
that gives the unicity of *A.




227
9. Reflexive Objects and the Type-Free Lambda Calculus


Call l b h p *t this extended calculus and Tp* its collection of types. The point is that the closed
term model of lbhp*t (and its extensions) forms a CCC, as the reader may check as an exercise.
Then the provable equations of Th are realized in |lbhp*t|, as isomorphisms. We give an explicit
name to these isomorphisms, as l-terms provide the basic working tools.

9.6.3 Definition Let A,BÎTp*. Then A and B are provably isomorphic (A @ p B) iff
there exist closed l-terms M : A ® B and N : B ® A such that lbhp* t |Ð M » N = IB and
lbhp*t |Ð N » M = IA, where IA and IB are the identities of type A and B. We then say that
M and N are invertible terms in lbhp*t .

9.6.4 Remark By general categorical facts, we then have the easy implication of the equivalence
we want to show; namely, Th |- A = B Þ A @p B. It may be worth for the reader to work out
the details and construct the l-terms which actually give the isomorphisms. Indeed, they include the
’abstract“ verification of cartesian closure; for example, ’currying“ is realized by lz.lx.ly.z<x,y>
with inverse lz.lx.z(p1 x)(p2 x), that prove (A ´ B)® C @p A ® (B ® C); the term lz.<lx.(p1
(zx)),lx.(p2 (zx))> with inverse lz.lx.<(p1 z)x,(p2 z) x> prove A® (B ´ C) @p (A ® B) ´ (A
® C). The others are easily derived.


The proof of the other implication, i.e., A @p B Þ Th |- A = B, roughly goes as follows. As a
first step, types are reduced to ’type normal forms“, in a ’type rewrite“ system. This will eliminate
terminal types and bring products at the outermost level. Then one needs to show that isomorphisms
between type normal forms yield componentwise isomorphisms. This takes us to the pure typed l-
calculus (i.e., no products nor T's). Then a characterization of the invertible terms of the pure type-
free calculus is easily applied in the typed case, as the invertible type-free terms happen to be typable.
The syntactique structure of the invertible terms gives the result.
The axioms of Th suggest the following rewrite system R for types (essentially Th ’from left to
right “, with no commutativity):


9.6.5 Definition (Type rewriting R ) Let ">" be the transitive and substitutive type-reduction
relation given by:
1. A ´ T > A
1'. T ´ A > A
3. A ´ (B ´ C) > (A ´ B) ´ C
4. (A ´ B)® C > A ® (B ® C)
5. A® (B ´ C) > (A ® B) ´ (A ® C)
6. A®T > T
7. T®A > A .



228
9. Reflexive Objects and the Type-Free Lambda Calculus


The system R yields an obvious notion of normal form for types (type normal form), i.e.,
when no type reduction can be applied. Note that 1, 1', 6 and 7 ’eliminate the T's“, while 4 and 5
’bring outside ´“. It is then easy to observe that each type normal form is identical to T or has the
structure S1 ´ ... ´S n where each Si does not contain T nor "´". We write nf(S) for the
normal form of S (there is exactly one, see 1.6) and say that a normal form is non trivial if it is not
T.


9.6.6 Proposition R is Church-Rosser and each type has a unique type normal form in R .
Proof Easy exercise. ¨

By the implication discussed in remark 9.6.4, since R |- S > R implies Th |- S = R , it is clear that
any reduction R |- S > R is wittnessed by an invertible term of type S®R.


9.6.7 Corollary Given types S and R, one has:
1 - Th |- S = nf(S) and, thus,
2 - Th |- S = R Û Th |- nf(S) = nf(R).


In conclusion, when Th |- S = R, either we have nf(S) º T º nf(R), or Th |- nf(S) º (S1´ ...
´Sn) = (R1´ ... ´Rm) º nf(R). A crucial lemma below shows that, in this case, one also has n =
m.
The assertion in the corollary can be reformulated for invertible terms in a very convenient way:


9.6.8 Proposition (commuting diagram) Given types A and B, assume that F: A®nf(A) and
G: B®nf(B) prove the reductions to type n.f.. Then a term M: A®B is invertible iff there exist an
invertible term M': nf(A)®nf(B), such that M = G-1°M'°F.
Proof. Ü) Set M-1 º (G-1°M'°F)-1 º F-1°M'-1°G, then M is invertible.
Þ) Just set M' = G°M°F-1. Then M'-1 º F°M-1°G-1 and M' is invertible. ¨


A diagram easily represents the situation in the proposition:




229
9. Reflexive Objects and the Type-Free Lambda Calculus


M
B
A

F G


A1 B1
´ M' ´
: :
´
´
B
An m

We now state a few lemmas that should guide the reader through the basic ideas of this application of
l-calculus to category theory. Most technical proofs, indeed l-calculus proofs, are omitted (and the
reader should consult the references).
Recall first that, when Th |- S = R, one has
nf(S) º T º nf(R), or Th |- nf(S) º (S1´ ... ´Sn) = (R1´ ... ´Rm) º nf(R).
Notice that, in the latter case, there cannot be any occurrence of T in either type. Indeed, a non
trivial type normal form cannot be provably equated to T, as it can be easily pointed out by taking a
non trivial model. Thus it may suffice to look at equations such as (S1´ ... ´Sn) = (R1´ ... ´Rm)
with no occurrences of T and, hence, to invertible terms with no occurrences of the type constant T
in their types. We can show that these terms do not contain any occurrence of *A either, for no type
A, via the following lemma.


9.6.9 Lemma Let M be a term of lbhp*t in n.f..
1 - (Terms of a product type) If M: A´B, then either M º <M1, M2>, or there is x:C such that
xÎFV(M) and A´B is a type subexpression of C.
2 - (Every term, whose type contains no T, has no occurrence of *A constants) Assume that in M
there is an occurrence of *A, for some type A. Then there is some occurrence of the type constant
T in the type of M or in the type of some free variable of M.
Proof. By induction on the structure of M. ¨

Note now that (the equational theory of) lbhp*t is a conservative extension of (the equational
theory of) lbhpt. Similarly for lbhpt w.r.t. lbht. Thus, invertibility in the extended theory,
given by terms of a purer one, holds in the latter.


9.6.10 Proposition (Isomorphisms between type normal forms are given by terms in lbhp t)
Assume that S and R are non trivial type normal forms. If the closed terms M and N prove S
@p R in lbhp*t, then their normal forms contain no occurrences of the constants *A. (Thus, M
and N are actually in lbhpt).




230
9. Reflexive Objects and the Type-Free Lambda Calculus


Proof By the previous lemma, as the terms are closed and no T occurs in their type. ¨

So we have factored out the class of constants *A, and we restricted the attention to lbhpt. By the
next step, we reduce the problem to the pure calculus, i.e., we eliminate pairing as well, in a sense.

9.6.11 Proposition (Isomorphic type normal forms have equal lenght ) Let S º S1´ ... ´Sm
and R º R1´ ... ´Rn be type normal forms. Then S @p R iff
n = m and there exist M1,...,Mn ; N1,...,Nn such that
x1: S1, ..xn: Sn |- <M1,...,Mn>: (R1´ ... ´Rn)
y1: R1, ..yn : Rn |- <N1,...,Nn>: (S1´ ... ´Sn)
with Mi[ x := N] =bh yi , for 1 £ i £ n
Nj[ y := M] =bh xj , for 1 £ j £ n
and there exist permutations s, p over n such that
Mi = lui.xsi Pi and Nj = lvj.ypj Qj
( M is a vector of terms; substitution of vectors of equal lenght is meant componentwise).
Proof (Not obvious, see references). ¨


By induction, one may easily observe that terms of lbhpt whose type is arrow-only belong to lbht.
Thus, one may look componentwise at terms that prove an isomorphism. The next point is to show
that each component, indeed a term of lbht, yields an isomorphism. This will be done by using a
characterization of invertible terms in the pure calculus. The same result will be applied once more in
order to obtain the result we aim at.
The characterization below has been given in the type-free calculus, as an answer to an old
question of Church on the group of type-free terms. We follow the type-free notation, also for
notational convenience.


9.6.12 Definition Let M be a type-free term. Then M is a finite hereditary permutation
(f.h.p.) iff either
(i) lbh |Ðu M = lx.x , or
(ii) lbh |Ðu M = lz. lx.zN s , where if |x| = n then s is a permutation over n and zN s =
zNs1Ns2É Nsn , such that, for 1 £ i £ n, lxi.Ni is a finite hereditary permutation.


For example, lz.lx 1 .lx 2 .zx 2 x 1 and lz.lx 1 .lx 2 .zx 2 (lx 3 .lx 4 .x 1 x 4 x 3 ) are f.h.p.'s. The
structure of f.h.p.'s is tidily desplayed by Bšhm-trees. The Bšhm-tree of a term M is
(informally) given by:
BT(M) = W if M has no head normal form
BT(M) = lx1 ... xn. y if M =b lx1...xn. y M1 ... Mp



231
9. Reflexive Objects and the Type-Free Lambda Calculus


/ ... \
BT(M1) BT(Mp)
(see references).
It is easy to observe that a BT(M) is finite and W-free iff M has a normal form. Then one may
look at f.h.p.'s as Bšhm-trees, as follows:

lz x. z




ly1. xs 1 . . . lyn. xsn
: :
and so on, up to a finite depth (note that yi may be an empty string of variables). Clearly, the
f.h.p.'s are closed terms and possess a normal form. In particular, exactly the abstracted variables at
level n+1 appear at level n+2, modulo some permutation of the order (note the special case of z at
level 0). The importance of f.h.p.'s arises from the following classic theorem of l-calculus.
(Clearly, the notion of invertible term given in 9.6.3 easily translates to type-free l-calculi).

9.6.13 Theorem Let M be an untyped term possessing normal form. Then M is lbh-invertible
iff M is a f.h.p..


Recall now that all typed terms possess a (unique) normal form (see references). Let then M be a
typed l-term and write e(M) for the erasure of M, i.e. for M with all type labels erased.


Remark Observe that the erasures of all axioms and rules of the typed lambda calculus are
themselves axioms and rules of the type-free lambda calculus. Then, if M and N are terms of
lbht and lbht |Ð M = N, one has lbh |Ð e(M) = e(N). Thus, in particular, if M : s ® t and N :
t ® s are invertible terms in lbht, e(M) and e(N) are f.h.p.'s.

Exercise Show that the f.h.p.'s are typable terms (Hint: Just follow the inductive definition and
give z, for instance, type A1 ® (A2..... ® B), where the Ai's are the types of the Nsi.) Then,
by the a small abuse of language, we may talk also of typed f.h.p.'s. Observe that these are exactly
the typed invertible terms in definition 9.6.3.


The first application of 9.6.13 we need is the following.




232
9. Reflexive Objects and the Type-Free Lambda Calculus


9.6.14 Proposition Let M1 , ... Mn , N1 , ... ,Nn and permutation s be as in lemma 9.6.11.
Then, for all i, lxsi.Mi : Ssi®Ri and lyi.Nsi : Ri®Ssi are invertible terms.
Proof. For a suitable typing of the variables it is possible to build the following terms of lbht (we
erase types for convenience):
M = lzx1...xn.zM1 ... Mn
N = lzy 1 ...yn .z N1 ... Nn .
It is an easy computation to check, by the definition of the Mi's and of the Ni's, that M and N are
invertible. Moreover, they are (by construction) in normal form, thus, by theorem 9.6.13, M and N
are f.h.p.'s. This is enough to show that every Mi has only one occurrence of the xi's (namely
xsi); similarly for the Ni's.
Thus we obtain
Mi[x := N] º Mi[ xs(i) := Ns(i)] =bh yi, for 1 £ i £ n
Ni[y := M] º Ni[ yp(i) := Mp(i)] =bh xi, for 1 £ i £ n
and, hence, for each i, lxs(i).Mi : Ss(i)®Ri and lyi.Ns(i) : Ri®Ss(i) are invertible. ¨

As a result of the work done so far, we can then focus on invertible terms whose types contain only
’®“ i.e., investigate componentwise the isomorphisms of type normal forms. Of course, these
isomorphisms will be given just by a fragment of theory Th.
Call S the subtheory of Th given by just one proper axiom (plus the usual axioms and rules for
’=“), namely
(swap) A®(B®C) = (B®(A®C)) .
S is a subtheory of Th by axioms 2 and 4 of Th.

9.6.15 Proposition Let A, B be type expressions with no occurences of T nor ´. Then
A @p B Þ S |ÐA = B.
Proof Suppose A @p B via M and N. As usual, we may assume without loss of generality that
M and N are in normal form. By lemma 9.6.9 and the remark after 9.6.11, M and N actually
live in lbht and, by theorem 9.6.13, they are f.h.p.'s. We prove S |Ð A = B by induction on the
depth of the Bšhm-tree of M.
Depth 1: M º lz : C. z. Thus M : C ® C, and S |Ð C = C by reflexivity.
Depth n+1: M º lz : E. lx : D. zNs. Recall zNs = zNs1 ... Nsn where if the ith abstraction in
lx : D is lxi : Di then the erasure of lxi : Di.Nsi is a f.h.p.. Thus lxi : Di.Nsi gives (half of) a
provable isomorphism from Di to some Fi. Hence the type of Nsi is Fi. In order to type check,
we must have E = (Fs1 ® ... ® Fsn ® B) for some B. Thus the type of M is ( Fs1 ® ... ®
F s n ® B) ® (D 1 ® ... ® Dn ® B). By induction, since the height of the Bšhm tree of (the
erasure of) each lxi : Di. Nsi is less than the height of the Bšhm tree of M, ona has S |Ð Di =
Fi for 1 £ i £ n. By a repeated use of the rules for "=", we get



233
9. Reflexive Objects and the Type-Free Lambda Calculus


S |Ð ( Fs1 ® ... ® Fsn ® B) = ( Ds1 ® ... ® Dsn ® B).
Hence it suffices to show
S |Ð ( Ds1 ® ... ® Dsn ® B) = ( D1 ® ... ® Dn ® B).
This is quite simple to show by a repeated use of axiom (swap) above in conjunction with the rules.
¨


Clearly, also the converse of proposition 9.6.15 holds, since the "Ü" part in 9.6.15 is provable by
a fragment of the proof hinted in 9.6.4. Thus one has:
S |Ð A = B Û A @p B by terms in lbht.
The result we aim at, is just the extension of this fact to Th and lbhp*t.


9.6.16 Main Theorem S @ p R Û Th|- S = R
Proof. In view of 9.6.4, we only need to prove S @ p R Þ Th |- S = R. As we know, this is
equivalent to proving nf(S) @ nf(R) Þ Th |- nf(S) = nf(R).
Now, by proposition 9.6.11, for nf(S) º (S1´ ... ´Sn) and (R1´ ... ´Rm) º nf(R), we have
nf(S) @ nf(R) Þ n = m and there exist M1, ..., Mn , N1, ..., Nn
and a permutation s such that lxsi.Mi : Ssi®Ri and lyi.Nsi : Ri®Ssi .
By 9.6.14, these terms are invertible, for each i. Thus, by 9.6.15, S |- Ri = Ssi and, hence, by
the rules, Th |- S = R. ¨

This concludes the proof of the main theorem of this part.


9.6.17 Corollary Given types A and B, it is decidable whether they are (their interpretation
yields) isomorphic (objects) in all CCC's.
Proof (Hint) Reduce A and B to type normal form. Check that these have an equal number of
factors. If so, observe that theory S does not change the lenght of types and perfom the required
swaps to check the equality, in that theory, of each component. ¨


Exercise Check the complexity of the theory of provable isomorphisms.



Part 2: Higher type objects as models of the type-free l -calculus
We give here some examples of categories and objects with the properties mentioned in the previous
sections and discuss connections to Higher Type Recursion Theory, a highly developed topic to
which denotational semantics of programming languages is greatly indebted. This theory suggested
the early structures for a ’generalized theory of computation,“ stressed the role of CCC's and, jointly




234
9. Reflexive Objects and the Type-Free Lambda Calculus


with category theory, set the basis for the construction of the early models of (type-free) l-calculus
and, thus, of functional programming languages.
We first mention a simple way to obtain lots of type-free models in CCC's with reflexive objects.
Then we apply this construction to the main type structures for higher type recursion: the partial
continuous and computable functionals in all finite higher types. Well-established results allow to
recover from those structures the various hierarchies of total functionals, which actually started the
topic (see references).
In section 2.4 we already gave two examples of reflexive objects in different CCC and, thus, of
l-models. When presenting the first, Pw, in 2.4.1, we promised to show the reflexivity of another
very familiar Scott domain: the collection P(R) of the partial (recursive) functions from w to w . Its
reflexivity, see theorem 9.5.2, will be a consequence of a stronger property, with respect to a suitable
category.


Exercise Let C be a CCC and T be a terminal object. Then "X,YÎObC, if T < Y, one has X
< XY .
(Solution: The retraction (i,j) is given by i = L(pr1)ÎC[X,XY] and j = eval°(id´t)ÎC[XY,X]
for some fixed tÎC[T, X]. Indeed, j° i = j° (i´d T ) = eval° (id´t)° (i´d T ) = eval° (i´id) ° (id´t) =
eval°(L(pr1)´id)°(id´t) = pr1°id´t = id .)

Let the set of type symbols, Tp, contain at least the atomic type 1. Then, for X in a CCC C, set
X1 = X, and, for A = Xs and B = Xt, set Xs®t = BA and Xs´t = A´B.


9.6.18 Lemma Let U be a reflexive object in a CCC C. Then, for {Us}sÎTp as above
"s, tÎTp Us < Ut in C
In particular, then, "sÎTp Us®s < Us.
Proof Assume, by induction on the syntactic structure of types, that U < Us and U < Ut .
Clearly, U´U < Us´t. It is also easy to check that UU < Us®t. Similarly, from the inductive
assumptions Us < U and Ut < U, one has Us®t < U U < U, as U is a reflexive object, and
U s´t < U´U < U, by proposition 2.3.6. Finally, U < U´U and U < UU , by T < U and the
exercise. Therefore, "s,tÎTp Us < U < Ut in C. ¨

As already shown, Scott domains, coherent domains and other categories of continuous functions
have nontrivial reflexive objects. By the lemma, in these categories there are lots of l-models, one in
each higher type s, over the reflexive object. We consider here yet another simple category with a
reflexive object, namely the category pcD of w-algebraic pair-consistent c.p.o.•s, and the object P
of partial functions from integer to integer.




235
9. Reflexive Objects and the Type-Free Lambda Calculus


Call first a subset D of a p.o.set (X,£) pairwise consistent if any pair of elements in D has
an upper bound in X (and write xÝy for $zÎX x,y £ z ) . (X,£) is pair-consistent if any
pairwise consistent subset has a l.u.b. Call pcD the category of w-algebraic pair-consistent c.p.o.•s
(cf. examples in 2.4.1), with continuous maps as morphisms.

Exercise Prove that pcD is a full subCCC of the category D of Scott domains in 2.4.1.


9.6.19 Theorem Let P be the set of the partial number-theoretic functions. Then for any object
X in pcD, X < P . In particular, P is reflexive.
Proof. Let X = (X, X0 , < ) be in pcD, and let e: w®X 0 be an enumeration of the compact
elements of X. Define j: X®P by setting, for all nÎw,
j(x)(n) = if e(n) £ x then 0
else if ˜(xÝe(n)) then 1
else ^ .
Equivalently, j(x)ÎP is uniquely determined by the ordered pair in which its domain splits
á{ nÎw | j(x)(n) = 0}, {nÎw | j(x)(n) = 1} ± = á{nÎw | e(n) £ x}, {nÎw | ˜(xÝe(n)) }±.
It is easy to prove that j is continuous.
In order to define y: P®X , for any fÎP, set
Xf = {e(i) | f(i) = 0 and "j < i, ˜(e(i)Ýe(j)) ® f(j) ¹ 0}.
First, Xf is pairwise consistent. Let i, j be such that e(i), e(j)ÎXf. Then f(i) = f(j) = 0. Suppose
that ˜(e(i)Ýe(j)). Then i < j Þ f(i) ¹ 0 and j < i Þ f(j) ¹ 0 , which is impossible. Thus
e(i)Ýe(j), so Xf is pairwise-consistent. By the consistency property of X , we can define y: P®X
by y(f) = supX(Xf). It is a simple exercise to prove that y is continuous and that y°j(x) = x for
all xÎX. Therefore X is a retract of P. ¨


It is clear that computability is at hand. As a matter of fact, the categories and results described so far
can be ’effectivized,“ in analogy to the examples in 2.4.1, e.g., the category ED. Denote by Xo the
collection of the compact elements of (X,£) in pcD.


9.6.20 Definition Let X = (X,Xo ,eo ,£) be in pcD and eo : w®X o (bijective). Then X is
effectively given i f
1. eo(n)Ýeo(m) is a decidable predicate
2. $gÎR "n,m ( eo(n)Ýeo(m) Þ eo (g(n,m)) = sup{eo(n), eo(m)} ).

It is easy to show that if X and Y are effectively given, then also the space of continuous functions
from X to Y is effectively given. Indeed, the category of effectively given w-algebraic pair-
consistent c.p.o.•s and continuous functions is cartesian closed (similarly to ED).



236
9. Reflexive Objects and the Type-Free Lambda Calculus


Recall that ideals are downward closed directed subsets of a poset (X,£). As in the definition of
the category CD of constructive domains in 2.4.1, the idea now is to take, within an effectively given
(X,Xo ,eo,£), only the l.u.b of those ideals of Xo, which are indexed over a recursively enumerable
set. Call computable elements the l.u.b of the r.e. indexed ideals. Clearly, the computable elements
of P are exactly the partial recursive functions, PR.


9.6.21 Definition A sub-p.o.set X c of an effectively given X = (X,X o ,e o ,£) is a
constructive and pair-consistent domain (ccd) if for any ideal D Í Xo one has:
D is principal in Xc iff eo-1(D) is a recursively enumerable set.

Thus Xc contains exactly the computable elements of X , e.g., Pc = PR. By the following
exercise, this gives yet another interesting CCC.


Exercises
i. Let CCD be the category whose objects are ccd's and whose morphisms are the continuous and
computable functions (computable as elements of the function spaces). Prove that CCD is cartesian
closed.
ii. Prove 9.6.19 above for PR instead of P, i.e., prove that also PR is reflexive in CCD.

Consider now the type structure {PRs}sÎTp constructed over PR in CCD. These are known as
the (higher type) partial recursive functionals. By the exercise and lemma 9.6.18, they yield a (type-
free) l-model in any finite type, as PRs®s < PRs .
CCD tidily relates to categories defined in the previous section, provided that a minor
generalization is made. So far, we have only been dealing with total applicative structures, i.e.,
where ’.“ is everywhere defined, as combinatory algebras are total structures. There exist, though,
interesting partial applicative structures: for example, Kleene's K = (w,.), where n.m = fn(m) for
some acceptable Gšdel numbering f: w®PR of the partial recursive functions.
In general, given a partial applicative structure B = (X,.), i.e., ’.“ may be a partial binary
operation, one can define the categories PB, ERB and PERB as in definitions 9.5.2 and 9.5.4, with
a minor caution. Since we deal here with categories of total morphisms, we consider only total
polynomials in each P[Xn,Xm]; in particular in P[X,X], when defining ER[R,S] in definition 9.5.4.
As for PER[R,S], each fÎPER[R,S] is ’computed,“ in the sense of 9.5.4, by a (possibly partial)
gÎP[X,X] which must be total on domR, though. In conclusion, by the exercise before 9.5.3 and
remark 9.5.9, if X´X < X in PB , then proposition 9.5.5 applies similarly and PB and ER B are
full sub-CC of the CC PERB. Moreover, if B is a partial combinatory algebra, then PERB is a
CCC by corollary 9.5.8 and what follows. The remaining results carry on similarly.




237
9. Reflexive Objects and the Type-Free Lambda Calculus


This remark has already been (implicitly) applied when defining PER over w. As a matter of fact,
Kleene•s K = (w,.) is a partial combinatory algebra, as it contains (indices for) partial k and s.
Thus, the properties of PER (= PERK and ER = ERK) could be derived also by the work in this
chapter.

Exercise The reader has already checked that the category EN of numbered sets (see the examples
in section 2.2) is equivalent to ERK. He or she may try to give now an extension of EN which is
cartesian closed and equivalent to PERK.

We already mentioned, in example 2.4.1, an important theorem, the Generalized Myhill-
Shepherdson Theorem, which related constructive domains and EN. In this frame, it may be restated
as ’CCD is equivalent, as a category, to a full subCCC of ER K .“ Jointly to the exercise, this
provides interesting embeddings, up to equivalence, of CCD into ERK into PERK.
It should be clear why Kleene's K is only a partial combinatory algebra and not a total one. If
w w represents PER[w,w] = P[w,w], then there is no principal pÎPER[w,w w ], as there is no
Gšdel-numbering or effective enumeration of P[w,w] = R, the recursive functions.
One may try another way to turn K into a combinatory algebra. Consider first the category
CCDp of ccd's and partial morphisms, i.e., partial continuous maps with open domain. Let _^ =
_° be the lifting functor defined in example 5.2.4. CCD[w^,w^], then, coincides with PR plus
the everywhere constant function on w^. From any acceptable Gšdel-numbering of PR it is easy to
construct a principal p'ÎCCD[w ^ ,PR]; however, w ^ ´w ^ < w ^ in CCD fails, by a simple
continuity argument. Thus also (w ^ ,.) does not yield a combinatory algebra. However, by
PRs®s < PRs in CCD and 9.5.10, l-models may be found at any finite higher type.
Note that p' above or the Gšdel-numberings are principal morphisms which cannot be turned
into retractions, by the latter observation or because, given a partial recursive function, there is no
uniform effective choice of one of its indices, by the Rice theorem. More examples could be given by
taking combinatory algebras which cannot be turned into l-models. Indeed, a simple example is
given by the term model of Combinatory Logic, i.e., by a ’model“ constructed by purely syntactic
tools.

Remark (Partial vs. total maps) The reader may have noticed that there are various notions of
partiality mentioned in these sections. As for the last, it poses no problem: a partial applicative
structure has a (possibly) partial application. One may construct over it, though, categories of total
maps, such as EN, ERK (cf. the definition of morphisms in these categories).
Note now that we called {PRs}sÎTp the partial continuous and computable functionals, even
though, at any type higher then 1, these are total, i.e., always defined, continuous (and computable)
maps. Why are they called partial, in the literature? The intuition should be clear, but the categorical



238
9. Reflexive Objects and the Type-Free Lambda Calculus


notion of complete object (see definition 2.5.6) may provide a better or more rigorous understanding.
As for the intuition, PR contains partial maps, in the ordinary sense, and each of the higher types
contains a least element: the empty set in PR, the constantly empty map in PRPR and so on.
Intuitively, these least elements give the ’undefined value“ in the intended type. Categorically, this is
understood by observing that, by this, each higher type, except for type 0 ( i.e., w) is a complete
object in the intended category of partial maps, in the sense of section 2.5. The point is that these
objects, by theorem 2.5.9, are exactly those such that the partial morphisms may be extended, and
indeed viewed, as total ones.

Remark (On total functionals) Consider now w and the total maps from w to w. We hint now at
how to move to higher types and preserve totality of morphisms, in a categorical environment where
it is possible to give a good notion of computability.
In sections 3.4 and 5.3 we presented the CCC (sep-)FIL of (separable) filter spaces and
discussed some of its categorical properties. We also mentioned that this category is essentially
nontopological, as some relevant types are not in the range of the embedding functor H: Top®FIL,
defined in example 5.3.7. In particular, FIL-w, the sub-CCC of sep-FIL generated by w, endowed
with (the convergence induced by) the discrete topology, contains non topological types. The objects
in FIL-w are the sets of total continuous functionals.
On separable filter spaces, with an enumeration {Ui}iÎw of the base, one may consider the
effectively given objects by generalizing the technique for domains in example 2.4.1 and definition
9.6.3. In short, one has to require that the base is decidable in the sense that
{ i | Ui = Æ } and { (i1,..., im ,k1,...,kn) | Ui1Ç...ÇU im Í U k1Ç...ÇU kn }
are recursive (uniformely in n and m). Then the computable elements are defined as limits of r.e.
indexed filters. More precisely, let ¯s be the notion of convergence over filter spaces given in (s-
conv.) in 5.3.7. Then set, for (X,F)Îsep-FIL with a decidable base,
xÎX is computable iff $F¯sx { i | UiÎF } is r.e..
In higher types, this defines total computable functionals.


Exercise Embedd the category ED, as topogical spaces, in 2.4.1 into sep-FIL by the functor H :
Top®FIL in 5.3.7 and describe how H and its left adjoint behave on computable elements. The
computable elements of FIL-w are the (Kleene-Kreisel) total continuous and computable functionals
(see references).


As a final connection to the other categories of effective maps we used here, we just mention that
a complex quotienting technique, which hereditarily defines total elements as the functions that take
total elements to total elements, allows us to establish adjoint equivalences between ED-w^, the sub-
w
CCC generated by w ^ in ED, and PER K -w, the sub-CCC generated by (w,id) in PER K .



239
9. Reflexive Objects and the Type-Free Lambda Calculus


Similarly, the subCCC PERPw-w in PERPw, the category of p.e.r.•s over the reflexive object Pw,
corresponds to FIL-w. (See references).



References The original construction in Scott (1972) gives a non trivial isomorphism AA @ A in
a CCC of lattices. The general notion of categorical model of the type-free calculus l b h and l b are
investigated in Berry (1979), Obtulowicz and Wiweger (1982), Koymans (1982), by using, though,
the category of retractions, which does not need to have e.p., instead of PER (see Barendregt (1984)
for a survey). By this one may deal with a weaker notion of model, the l-algebras. l-algebras,
originally called pseudo-l-models in Hindley and Longo (1980), are exactly the models of
Combinatory Logic with b-equality (see also Barendregt (1984) or Hindley and Seldin (1986)). They
are characterized as in theorem 9.5.11(2), by dropping the assumption that C has enough points and
they are in between combinatory algebras and l-models (in Barendregt and Koymans (1980) it is
shown that the term model of CL cannot be turned into a l-algebra.) However, retractions do not
form a CCC on combinatory algebras and do not help in the categorical understanding of CL Thus we
used PER, as in Longo and Moggi (1990), which we largely followed and where the models of CL
were first characterized. The use of a choice operator e in order to extend combinatory algebras to
l-models, which we followed here, is formalized in Meyer (1982).
Cousineau and al. (1985) and Curien (1986) introduce the categorical abstract machine.
The valid isomorphisms in Cartesian Closed categories are characterized in Bruce and DiCosmo
and Longo (1990) (by a different proof, they where also given in Soloviev (1983)). The invertibility
theorem 9.6.13, for the type-free l-calculus, is due to Dezani (1976). Rittri (1989) applies
isomorphisms in all CCC's to retrieval methods in libraries of programs.
Finally, pairwise consistent domains and the properties of Tw are investigated in Plotkin (1978).
Filter spaces and related categories are used, for higher type recursion theory, in Hyland (1979).
Ershov (1973-76) and Longo and Moggi (1984-84a) establish the relation between various classes of
total and partial functionals.




240
10. Recursive Domain Equations


Chapter 10


RECURSIVE DOMAIN EQUATIONS

One of the early applications of Category Theory to computer science was the solution of recursive
domain equations. This kind of equation is typical of every language that allows an explicit or implicit
form of self-application of its data types (such as a recursive procedure call, say).
For example, by theorem 9.5.10 we already know that in order to give semantics to the pure l-
calculus we need a domain isomorphic to its own function space; moreover, if we are interested in
computing over a fixed domain A of atoms, we need a solution to the equation
(*) X @ A+(X®X).
In general, recursive specification of domains can be seen as a particular case of recursive
definition of data types that is an even more important topic in computer science. For example every
programmer is used to considering the data type of all the lists of objects of type A as a solution to the
following recursive equation:
A_List = Nil + A´(A_list)
where Nil is a one-element data type.
In many respects, the general and unified theory of this kind of equation, mainly developed in the
framework of Category Theory, has provided the base for the elimination, in most modern
languages, of many unreasonable restrictions in the definition of recursive data types that existed in
older languages. Note that these restrictions were not always motivated by implementation problems,
but often by a real misunderstanding of the semantics of recursive definitions.
The first mathematical difficulty in giving a meaning to recursive specifications of data types is
that they do not always have a set-theoretic solution. For example, equation (*) above has no solution
in Set by obvious cardinality reasons: the arrow-domain A®B cannot be interpreted as the
collection of all functions between A and B. The natural choice is to consider categories other than
Set, with fewer morphisms but sufficiently many as to include all ’computable functions“ over the
intended data types. The relevance of morphisms suggests why the categorial framework arises so
naturally in this context. Note that the intended category C must be still Cartesian closed, in order to
give the correct interpretation to the function space constuction. Once C is fixed, the idea for solving
recursive domain equations is to use some sort of fixed point technique. To be more specific, in the
categorical approach, the general form of equations such as (*) above, looks like
(**) X @ F(X)
where X ranges over the object of a category C and F: C®C is a covariant endofunctor of the
category. If C is w-cocomplete, C has an initial object, and F is w-continuous, then theorem 6.5.2




241
10. Recursive Domain Equations


gives a solution to (**). The main problem is that an obvious definition does not always exist for
such an F, as we are going to show in the next section.



10.1 The Problem of Contravariant Functors
Consider again the equation
(*) X @ A+(X®X)
in the introduction. In order to apply theorem 6.5.2, we need to work in a w-cocomplete category C.
Moreover, the category must be Cartesian closed and have coproducts, so that we can give the
expected interpretation to the operators ® and +, which appear in (*).
Such a category is not difficult to find: an example is the category CPOS of c.p.o.•s with a least
(bottom) element and strict (bottom-preserving) continuous functions for morphisms. The next step
is to define a covariant functor F: C®C such that, for any object X of C, F(X) = A+(X®X).
The first idea would be to express F as a composition of the functors of sum and exponentiation
associated to the closure properties of C. For example, if A+_: C®C is the functor which takes B
to A+B, and f to idA +f, exp is the exponentiation functor, and D is the diagonal functor, we
could be tempted to define
F = (A+_) ° exp ° D
Unfortunately, this is not possible since exp is contravariant in the first component and cannot be
composed with the diagonal function; in other words, since exp: Cop´ C®C , and D: C®C´ C, ´
the previous equation is ill typed.
We would like to have a way of transforming every functor F in an associated functor F* with
the same behavior on objects, but covariant on morphisms, in all its components.
Unfortunately this is not possible in general, but still there is a very simple way, as we will see,
to turn a contravariant endofunctor F: C®C into a covariant endofunctor F* in an associated
category C*, which has the same objects of C, and such that isomorphisms in C* give isomorphisms
in C.
Then, if C* is w-cocomplete and has a terminal object, and F* is w-continuous, we can apply
theorem 6.5.2, find a solution in C*, and then derive a solution in C. Note that the category C*
does not need to be cartesian closed, neither it must be closed under coproducts, since we already
know how to give a meaning to the constuctions of new objects in C.
We shall define C* as a suitable subcategory of the following category C+-.

10.1.1 Definition Given a category C, the category C+- has the same object of C and
f ÎC+-[A, B] iff f = (f+,f-) with f+ÎC[A, B] and f-ÎC[B, A].
Composition is defined by (f+,f-) ° (g+,g-) = (f+° g+, g-° f-).




242
10. Recursive Domain Equations


An intuitive way to regard the category C+- is the following. Consider the objects as data types;
there is a morphism from A to B if and only if a pair of ’coercions“ is given in order to go from
one to the other. Note also that two objects are isomorphic in C+- iff they are isomorphic in C.
We next show how to define covariant functors on C +- from arbitrary functors on C. For
simplicity, we reduce the definition to the case of a bifunctor F covariant in the first component and
contravariant in the second.

10.1.2 Definition Given a category C, and a functor F: CxC ® C contravariant in the first
component and covariant in the second, the covariant functor F+-: C+-xC+- ® C+- is defined by
F+-(A,B) = F(A,B).
F+-((f+,f-), (g+,g-)) = (F(f-,g+), F(f+,g-)).

One problem with the category C+- is that it is very unlikely to have colimits for all w-chains. The
interesting fact, though, is that the idea upon which definition 10.1.2 is based, works in every
subcategory C* of C+-, provided that only those functors F such that (F(f-,g+), F(f+,g-)) is still
a morphism in C* are considered.
Our goal, now, is to find a subcategory C* of C+- such that simple and common properties on
C (such as, for example, the existence of limits for all diagrams) are enough to guarantee the
existence of colimits for all w-chains in C*.
In the search for such a category C*, we can be helped by some intuition.
When in theorem 6.5.2 we considered the w-diagram ({Fi(0)}iÎw, {Fi(z)}iÎw ), we had in
mind that it is a chain of increasingly finer approximations of the limit. Thus, a morphism Fi(0), in
a sense, must explain why Fi(z) is less than Fi+1(z): no information must be lost passing from
Fi(z) to Fi+1(z). Reasonably, we may try to define a subcategory D of C +- whose morphisms
express this kind of relation between objects.
Among the subcategories of C+- that seem to satisfy this condition, an important one is CRet,
whose morphisms (f+,f-) have the property that f-° f+ = id (in C).
CRet is also very attractive becauseevery functor F on C may be still turned into a covariant
functor F+- on CRet by means of definition 10.1.2.
Indeed, consider for example a bifunctor F contravariant in the first component and covariant in
the second one. Then one has
F(f+,g-) ° F(f-,g+) = F( (f+,g-) ° (f-,g+) )
= F(f-° f+, g- ° g+) by composition in Cop´C
as (f+,f-), (g+,g-) are morphisms of CRet
= F(id, id)
= id.
Thus F+- ((f + ,f- ), (g+ ,g - )) = (F(f- ,g + ), F(f+ ,g - )) is well defined as (F(f- ,g + ), F(f+ ,g - )) is a
retraction pair.




243
10. Recursive Domain Equations


Unfortunately, CRet does not seem to suffice for our purposes. For example, up to now, there
is no known nontrivial Cartesian closed category C such that CRet has colimits for every w-chain.
Indeed, this is poses a very interesting problem: whether it is possible to find such a category, or
prove that it cannot exist.
It is very instructive to understand where the difficulty arises in general.
Suppose that the category C has limits for every diagram (this property holds in many interesting
CCC's; see chapter 6 for some examples) and let ({Di}iÎw , {fi}iÎw ) be an w-chain in C Ret.
Then ({Di}iÎw , {fi-}iÎw ) is an w-chain in C, and it has a limit (L,{gi}iÎw ). The object L
seems to be a good candidate as a limit also for the chain ({Di}iÎw , {fi}iÎw ) in CRet. Indeed,
the following theorem holds:

10.1.3 Theorem Let {Di}iÎw ,{fi}iÎw ) be a w-chain in C Ret. If (L, {gi} iÎw ) is a limit for
({Di}iÎw , {fi-}iÎw ) in C, then there is a cone ( L, {(di,gi)} iÎw ) for ({Di}iÎw , {fi}iÎw ) in
CRet (that is, every gi is a right member of a retraction pair).
Proof: Fix Dj. For every i define fj,i : Dj ® Di by:
fj,i = fi-° fi+1-° ... ° fj-1- if i < j
fi,i = id
fj,i = fi-1+° ... ° fj+1+° fj+ if i > j .
(Dj, {fj,i}iÎw) is a cone for ({Di}iÎw , {fi-}iÎw ), since fi- ° fj,i+1= fj,i as it is easy to check.
Thus there exists a unique morphism dj: Dj® L such that "iÎw gi ° dj = fj,i. In case i = j, gj ° dj
= fj,j = id.
We still have to check that "jÎw (fj+,fj-)°(dj+1,gj+1) = (dj,gj) .
Now, fj-° gj+1= gj by the definition of cone in C. In order to prove that dj+1°fj+= dj, note that
"iÎw gi ° dj+1° fi+ = fj+1,i ° fj+ = fj,j = gi ° dj, and the result follows by unicity.
By a diagram, for i > j :




¨




244
10. Recursive Domain Equations


Unfortunately, we have no way to prove that the cone (L, {di,gi}iÎw ) is universal. Indeed let (L',
{gi}iÎw ) be a cone for the w-chain ({Di}iÎw , {fi}iÎw ) in C Ret. Then (L',{gi-}iÎw ) is a
cone in C for ({Di}iÎw , {fi-}iÎw ) and there exists a unique morphism h in C from L' to L
such that "iÎw h ° gi = gi- and gi ° h = gi+. In other words:




However, there is in general no reasonable way to define a morphism k from L to L' such that
h ° k = id. In the next section, we will see a way out of this problem.



10.2 0-Categories
Consider the class of morphisms {gi+° gi}iÎw from L to L' defined by the diagram at the end of
the previous section. The morphism gi+ ° gi: L® L' describes how the approximation of L up to
the ith-level may be represented inside L'. Intuitively, one may expect that, in some sense, gi+ ° gi
£ gi+1+ ° gi+1. Moreover, if
1. the hom-sets in the category C are c.p.o.•s and
2. the class {gi+ ° gi}iÎw is an w-chain,
then we could soundly define k = ÈiÎw{gi+ ° gi}, and k would play the role required at the end of
the previous section. This takes us to the notion of ’0-category.“

10.2.1 Definition A category C is a 0-category iff
i. every hom-set C[a,b] is a cpo, with a least element 0a,b ;
ii. composition of morphisms is a continuous operation with respect to the partial order;
iii. for every fÎC[a,b] , 0b,c ° f = 0a,c .


Then, by definition, every 0-category satisfies (1) above. Our next problem is to ensure condition
(2). Note first that gi+ ° gi = gi+1+ ° fi+° fi- ° gi+1. Moreover, if fi+° fi- £ id, then gi+ ° gi £
gi+1+ ° gi+1. This suggests the refinement we need in the category CRet.




245
10. Recursive Domain Equations


10.2.2 Definition Let C be a 0-category, and let i: D®E, j: E®D be two morphisms in C.
Then (i,j) is a projection pair (from D to E ) iff j ° i = idD and i ° j £ idE . (If (i,j) is a
projection pair, i is an embedding and j is a projection.)


Exercises Prove the following statements:
1. If (i,j) is a projection pair from D to E, and (i',j') is another projection pair for the same two
objects, then i £ i' iff j ³ j'.
2. Every embedding i has a unique associated projection j = iR; conversely every projection j has
a unique associated embedding i = jL.


10.2.3 Definition Let C be a 0-category. The category C Prj has the same objects as C, and
projection pairs as morphisms.

Remark CPrj is a subcategory of CRet, and thus also of C+-. By the fact that every embedding
i has a unique associated projection j = iR (and, conversely, every projection j has a unique
associated embedding i = jL), CPrj is isomorphic to a subcategory CE of C that has embeddings as
morphisms (as well to a subcategory CP of C which has projections as morphisms). We prefer to
work in CPrj since it looks more natural and carries more explicit information. Note, however, the
following dualities: (CE)op @ CP @ (Cop)E (and, of course, (CP)op @ CE @ (Cop)P ).


Exercise Let C be a 0-category with terminal object t. Prove that t is terminal in CPrj too. (Use
property 10.2.1.(iii) in the definition of 0-category).

10.2.4 Theorem Let C be a 0-category with all wop-limits. Let ({Di}iÎw,{(fi+,fi-)}iÎw ) be an
w-chain in C Prj (and thus in C Ret ) and (L, {(d i,g i)} iÎw ) be the cone in C Ret defined by
theorem 10.1.3. Then (L, {(di,gi)} iÎw ) is a cone also in CPrj. Moreover it is universal in this
category.
Proof In order to prove that (L, {(di,gi)}iÎw ) is a cone in CPrj we must show that,"iÎw, di ° gi
£ id. Note that "iÎw di ° gi = di+1 ° fi+° fi- ° gi+1 £ di+1 ° gi+1. Thus, {di ° gi}iÎw is a chain
and its limit Q = ÈiÎw{di ° gi} must exist. We prove that Q = id and, thus, that "iÎw di ° gi £ Q
= id. Q = id since Q is a mediating morphism between (L, {gi}iÎw ) and itself in C. Indeed,
"jÎw,
gj ° Q = gj ° ÈiÎw{di ° gi}
= gj ° Èi ³ j{di ° gi}
= Èi ³ j{(gj ° di) ° gi}
= Èi ³ j{fi,j ° gi}




246
10. Recursive Domain Equations


= Èi ³ j{fi,j ° gi}
= g j.
We prove next that the cone (L, {(di,gi)}iÎw ) is universal in CPrj.
Let (L',{(gi+,gi-)}iÎw ) be another cone for ({Di}iÎw ,{(fi+,fi-)}iÎw ). That is,
"iÎw gi+° gi = gi+1+° fi+° fi- ° gi+1 £ gi+1+° gi+1
"iÎw di ° gi- = di+1 ° fi+° fi- ° gi+1- £ di+1 ° gi+1-.
Define then
h = ÈiÎw{gi+ ° gi} : L ® L'
k = ÈiÎw{di ° gi-} : L' ® L.
Observe that (h,k) is a projection pair, for
k ° h = ÈiÎw{di ° gi-} ° ÈiÎw{gi+ ° gi}
= ÈiÎw{di ° (gi- ° gi+) ° gi}
= ÈiÎw{di ° gi}
= Q = id
and
h ° k = ÈiÎw{gi+ ° gi } ° ÈiÎw{di ° gi-}
= ÈiÎw{gi+ ° (gi ° di ) ° gi-}
= ÈiÎw{gi+ ° gi-}
£ id.
Moreover, (h,k) is a mediating morphism between (L, {(di,gi)}iÎw ) and (L',{(gi+,gi-)}iÎw ),
since "jÎw
(h,k) ° (dj,gj) = (h ° dj , gj ° k )
= ( ÈiÎw{gi+ ° gi} ° dj , gj ° ÈiÎw{di ° gi-})
= ( Èi ³ j{gi+ ° gi ° dj} , È i ³ j { gj ° di ° gi-})
= ( Èi ³ j{gi+ ° fj,i} , È i ³ j { fi,j ° gi-})
= (gj+,gj-)
(h,k) is unique, because, if (h',k') is another mediating morhism, then
(h',k') = (h'° id, id ° k')
= (h'° Q, Q ° k')
= (h'° ÈiÎw{di ° gi}, ÈiÎw{di ° gi} ° k')
= (ÈiÎw{h'° di ° gi}, ÈiÎw{di ° gi ° k'})
= (ÈiÎw{gi+ ° gi}, ÈiÎw{di ° gi-})
= (h,k) . ¨

A useful characterization of w-colimits in the category CPrj is the following:




247
10. Recursive Domain Equations


10.2.5 Proposition The cone (L, {(d i,g i)} iÎw ) for the w-chain ({Di} iÎw , {(fi+ ,fi-)} iÎw )
in CPrj is universal iff Q = ÈiÎw{di ° gi} = id .
Proof Exercise. ¨


Up to now, we have shown that, if C is a 0-category with all wop-limits, then the category CPrj has
colimits for every w-chain.
The next point is to understand what we have lost with regard to the possibility of applying the
construction in definition 10.1.2, which turns contravariant functors into covariant ones. Indeed,
there is no reason to believe that the functor F+- of this definition transforms projection pairs within
projection pairs.
Recall now that a two-argument endofunctor F over C, which is contravariant in the first
argument and covariant in the second one, has type F: Cop´C ®C .

10.2.6 Definition Let C be a 0-category. A functor F: C op ´ C ®C is locally monotonic iff
it is monotonic on the hom-sets; that is, for f, f'ÎCop[A, B] and g, g'ÎC[C, D], one has
f £ f' , g £ g' Þ F(f,g) £ F(f',g').

10.2.7 Proposition If F: Cop´ C ®C is locally monotonic and (f+,f-) , (g+,g-) are projection
pairs, then also F+-((f+,f-),(g+,g-)) is also a projection pair.
Proof: By definition F+-((f+,f-),(g+,g-)) = (F(f-,g+), F(f+,g-)). Compute then
F(f+,g-) ° F(f-,g+) = F( (f+,g-) ° (f-,g+) )
= F( f-° f+, g- ° g+)
= F( id, id )
= id
and
F(f-,g+) ° F(f+,g-) = F( (f-,g+) ° (f+,g-) )
= F( f+° f-, g+ ° g-)
£ F( id, id )
= id. ¨

The last step is to see if we can find some simple condition on the functor F in C such that the
associated functor F+- in CPrj is w-continuous.


10.2.8 Definition Let C be a 0-category. A functor F: C op ´ C ® C is locally continuous
(0-functor) iff it is w-continuous on the hom-sets. That is, for every directed set {fi }iÎw in
Cop[A, B], and every directed set {gi }iÎw in C[C, D], one has
F(ÈiÎw{fi }, ÈiÎw{gi ) ) = ÈiÎw F(fi,gi ) .




248
10. Recursive Domain Equations




Of course, if F is locally continuous, then it is also locally monotonic.


Exercise Prove that the composition of two locally nonotonic (continuous) functors is still
monotonic (continuous).

10.2.9 Theorem Let C be a 0-category with all wop-limits. Let also F: Cop´ C®C be a locally
continuous functor. Then the functor F+-: CPrj´ CPrj®CPrj is w-continuous.
Proof Let ({Ai} iÎw , {(fi+ ,fi-)} iÎw ) and ( {Bi} iÎw , {(gi+ ,gi-)} iÎw ) be two w-chains in
CPrj and let (L, {(ri+,ri-)}iÎw ) and (M, {(si+,si-)}iÎw ) be the respective limits. Then, by
proposition 10.2.5,
Q = ÈiÎw{ri+ ° ri-} = id;
Y = ÈiÎw{si+ ° si-} = id.
We must show that
(F+-(L,M), {F+-((ri+,ri-), (si+,si-)) }iÎw ) = (F(L,M), {F(ri-,si+), F(ri+,si-))}iÎw )
is a limit in CPrj for the w-chain
( {F+-(Ai,Bi)}iÎw, {F+-((fi+,fi-), (gi+,gi-)) }iÎw ).
It is clearly a cone, by the property of functors. We show that it is universal by proving that
ÈiÎw{ F(ri-,si+) ° F(ri+,si-) } = id. The result then follows by proposition 10.2.5. We have the
following:
ÈiÎw{ F(ri-,si+) ° F(ri+,si-)} = ÈiÎw{ F( ri+ ° ri-, si+ ° si-) }
= F(ÈiÎw{ri+ ° ri-}, ÈiÎw{ si+ ° si- } )
= F( Q, Y )
= F( id, id )
= id. ¨

In conclusion, we have described a way to turn arbitrary functors into covariant functors on suitably
derived categories. Then we set the condition under which it is possible to obtain w-continuous
functors. The solution of equations, such as (*) at the beginning of this chapter, is thus immediately
found for these functors.

Example In the introduction to this section we mentioned the important categorical equation X @
A+(X®X). If we wish to find a solution to equations of this kind in some category C based on
c.p.o.s (such as CPO, CPOS, Scott Domains, and so on), we are generally forced to relax the
interpretation of at least one of the two symbols + and ®. Indeed, for their nature, all these categories
usually have fixpoints for all objects, and we know that this is inconsistent with having at the same
time coproducts and cartesian closedness. A typical way for avoiding the problem is to content




249
10. Recursive Domain Equations


ourselves with the interpretation of + as a weak coproduct. A weak coproduct is essentially defined
as a coproduct in definition 2.2.6, but no unicity is requested for the commuting arrow h.
The category CPO of c.p.o.•s with least (bottom) element and continuous functions for morphisms
is a 0-category with respect to the pointwise ordering of morphisms. CPO is a CCC with weak
coproducts A+B given by the coalesced sum (i.e. by identifying the two bottom elements of A and
B). Since it has coequalizers for every pair of objects, it has limits for every diagram.(see chapters 2
and 6). The functors A+_ : CPO®CPO and ® : CPO´ CPO®CPO, respectively defined by:
´
A+_ (B) = A+B, A+_ ( f ) = idA+ f,
®(A,B) = BA, ®( f, g) = lh. g ° h ° f,
are both locally continuous.
The diagonal functor D : CPO®CPO´ CPO, defined by D(A) = (A,A) and D(f) = (f,f) , is
´
locally continuous too. Thus we can apply theorem 10.2.9 and conclude that the associated functors
a. (A+_)+- : (CPO)Prj ® (CPO)Prj
(A+_)+-(f+, f-) = (idA+f+, idA+f-)
b. (®)+- : (CPO)Prj´ (CPO)Prj ® (CPO)Prj,
(®)+- ((f+, f-), (g+,g-)) = ( lh. g+ ° h ° f-, lh. g- ° h ° f+ )
c. (D)+- : (CPO)Prj ® (CPO)Prj´ (CPO)Prj
(D)+-(f+ , f-) = ( (f+ , f-) , (f+ , f-) )
are w-continuous. But composition of w-continuous functors is still a w-continuous functor; thus,
the functor F = (A+_)+-° (®)+- ° (D)+- : (CPO)Prj ® (CPO)Prj is w-continuous. Explicitly, F
is defined by
= A+XX
F(X)
F(f+,f-) = (idA+ lh. f+ ° h ° f-, idA+ lh. f- ° h ° f+).
Thus, for every A, there exists X such that X @ A+XX.



References For an early computer scientific introduction to recursive domain equations, the
reader should consult Stoy (1977). The first solution to the problem of finding a domain isomorphic
with its own function space, as required for the type-free l-calculus, was given in Scott (1972)
which basically started the mathematical discussion on recursive definitions of data types and, more
generally, the so called area of ’denotational semantics“. The categorical approach exposed in the
present chapter is a direct generalization of Scott•s method and is essentailly due to Wand (1979),
Lehmann and Smith (1981) and Smith and Plotkin (1982). An introductory presentation may be also
found in Plotkin (1978). Gunter (1985) investigates the notion of embedding as a particular case of
adjunction and, thus, sets the base for an interesting generalization of the categorial approach.




250
11. Second Order Lambda Calculus


Chapter 11


SECOND ORDER LAMBDA CALCULUS

The system l2, or second order l-calculus, has been introduced by Girard for the sake of Proof
Theory. It was meant to prove, in particular, a normalization theorem for second order arithmetic,
PA2 (also considered a sound formalization of analysis, by proof theorists). The key points are that
(second order) l-terms code proofs in (second order) systems based on natural deduction and, quite
generally, that cut elimination corresponds to b reduction for l-terms. Thus normal proofs for and
consistency of PA2 follow from the normalization theorem for l2 (see chapter 8 and references).

<<

. 8
( 10)



>>