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).