This implies that in a model we expect

DA ° g = g„g ° DD (+)

that is the naturality of D .

8.6.5 Example Consider the derivation

B, A |- C E |- A C |- D

________ _____________

B |- AÞC (AÞC), E |- D

________________________________

B, E |- D

The last cut is eliminated by introducing two other cuts of lesser grade, namely

B, A |- C C |- D

________________

E |- A B, A |- D

______________________________

B, E |- D

At the semantic level this gives

h: B„A ® C f: E ® A g: C ® D

_____________ _____________________________

L(h): B ® AÞC g ° evalA,C ° id„f: (AÞC)„E ® D

________________________________________________

g ° evalA,C ° id„f ° L(h)„id: B„E ® D

that reduces to

h: B„A ® C g: C ® D

______________________

f: E ® A g ° h : B„A ® D

_______________________________________

g ° h ° id„f : B, E ® D

Note that in a Cartesian closed category, by the b-axiom of exponents, one has

g ° evalA,C ° id„f ° L(h)„id = g ° evalA,C ° L(h)„id ° id„f = g ° h ° id„f.

This completes the observation that the Cartesian closure may be described in terms of equivalence of

proofs, up to normalization.

190

8. Formulae, Types, and Objects

8.7 Categorical Semantics of the Simply Typed Lambda Calculus

In sections 8.3 and 8.4, we have investigated the relation between typed lambda calculus and

intuitionistic logic, and in sections 8.5 and 8.6 we have established the connection between

intuitionistic logic and Cartesian closed categories. In this section we want now to ’fill the triangle“

among typed lambda calculus, intuitionistic logic and Cartesian closed categories, studying the

missing edge - namely the categorical semantics of the Typed Lambda Calculus, over CCC's.

The main idea of the categorical semantics of the typed lambda calculus is to interpret types as

objects and terms as morphisms of a category C. In particular, the reader has probably noted some

analogy between the axioms of lbhpt and the axioms defining products and exponents in Cartesian

closed categories. The relation is quite evident in the case of products: fsts´t®s and snds´t®t

are easily understood as the projections associated with the categorical product of s and t. Apart

from the problem of switching from ’application“ to ’composition,“ the axioms of lbhpt regarding

the product are essentially identical to the axioms in definition 1.3.3 of categorical product. Less

immediate is the connection between b (and h) and the rules defining the exponents of a CCC: the

main problem is that the definition in the calculus is based on the process of substitution, for which

we do not have any immediate equivalent in Category Theory. Let us look a little closer at our

tentative interpretation: the intuitive idea is that a term Mt with free variables among x1s1, ...,xnsn

should be interpreted as a morphism M t from D = s1´...´sn to t. Suppose now that we have

two terms Mt and Ng, such that the free variables of [Ng/ xg]Mt are in D= s1´...´sn. Then

look at M t like an arrow from D´g to t, and at Ng like an arrow from D to g. The effect of

substituting Ng for xg in Mt is simply achieved by composing Mt with < idD, Ng >.

These considerations are formalized in substitution lemma 8.7.6 below, which plays a central role in

the semantics of functional languages. Note now that in every CCC, one has

(bcat) eval ° <L(f),g> = eval ° L(f)´id ° <id,g> = f ° <id,g>

which, by our interpretation of substitution, is just the categorical equivalent of b-conversion in l-

calculus.

191

8. Formulae, Types, and Objects

We now begin a formal discussion on the categorical interpetation of typed l-calculus, by

outlining a simple and very intuitive, set-theoretic definition of model for lbhpt. This is just a

definition and will be instrumental to the categorical characterization below. In particular, it will allow

us to relate the category-theoretic approach to the Tarskian view in semantics. For a more direct

connection between lbhpt and CCC's, see the references.

The collection Tp of types over a set At of ground types has been defined in section 8.2. As

types will be largely used as indexes (of terms), in this section we go back to the use of small greek

letters s,t.... as metavariables for types.

8.7.1 Definition Let C = {Ci | iÎAt} be a collection of sets. Then TS C = {Cs } sÎTp is a

type structure over C iff, for all s,tÎTp,

Cs®t Í Cs ® Ct (= Set[Cs,Ct])

Cs´t = Cs´Ct .

8.7.2 Definition A type structure TS A = ({As }sÎTp, [ ]) is a model of typed l-calculus (with

products) iff [ ] yields an interpretation for lbh(p)t. That is, for any environment h: Var ®

UsÎTp (As} with h(xs)ÎAs, one has [Mr] hÎAr, for each rÎTp and for [ ] defined by

[xs] h = h(xs)

Var.

[Ms®tNs]h = [Ms®t]h ([Ns]h)

App.

[lxs.Mt]h(a) = [Mt] h[a/xs] for a Î As

b.

[ fsts´t®st]h = p1 , [ snds´t®st]h = “p2

p.

where p1, p2 are the set-theoretic projections (of proper types).

This is a good definition of model, i.e., the axioms and rules are realized and, given a model TSA

lbh(p)t, one actually has

lbh(p)t |¾ Ms = Ns Þ TSA |= Ms = Ns.

Indeed, the reader will be asked to check the validity of axiom (b) in the exercise before 8.7.7.

Note also that, in a model, axiom (h) and rule (x) trivially hold, since l-terms are interpreted as

functions in extenso and, hence, one has

h. "a [lys.Ms®tys] h(a) = [Ms®t]h(a) , for ysÏFV(Ms®t), and

x. "a [Mt]h[a/xs] = [Nt]h[a/xs] Þ [lxs.Mt]h = [lxs.Nt]h ,

by (b) and by [lxs.Pt]hÎAs®t Í As®At.

The properties of projections and pairing, in case one considers lbhpt, are trivially realized by

the definition of product.

Thus a type-structure TSA is a model of lbh(p)t iff

lbh(p)t |¾ Ms = Ns Þ TSA |= Ms = Ns.

192

8. Formulae, Types, and Objects

Since the previous definition of model is set-theoretic, a suitable notion of ’concreteness“ for

categories can help in studying categories as models. The minor loss of generality, in this case, is

balanced by the gain in intuition.

In general, concrete categories are widely used in denotational semantics; they are (usually)

defined by an ’enough points“ requirement.

8.7.3 Definition. Let C be a category. tÎOb C is a generator iff for all a,bÎOb C and all

f,gÎC[a,b], f ¹ g Þ $hÎC[t,a] f°h ¹ g°h .

C has enough points if there exists a generator t that is terminal in the given category.

The terminology derives from the idea that the arrows in C[t,a], when t is terminal, may be

understood as the points (or elements) of a. Indeed, we can associate with each category C having

enough points a category of sets Cset as follows. For a,bÎObC and t terminal

objects: |a| = C[t,a]

morphisms: fÎCset[|a|,|b|] iff $f'ÎC[a,b] f = f'° _ .

Observe that f' is unique once f is given.

8.7.4 Proposition. If C is a CCC with enough points, then C set is also a CCC with enough

points.

Proof If cs®t and cs´t are the exponent and product objects, in C, of cs and ct, then |cs®t|

and |cs´t| are the exponent and product objects, in Cset, of |cs| and |ct|. As for the exponent, just

set evalset = eval°_ , and Lset(f) = L(f')°_ , where f' defines f as above. The rest is easy. ¨

Note that one obtains type structures from all categories with enough points That is, let K be a CCC

with enough points and C = {ki | iÎAt} Í ObK. Let also ks®t and ks´t be the exponent and

product objects, in K, of ks and kt . Then K C = {K[T,k s ] | sÎTp } is the type structure

generated by K and C.

Examples. The simplest type structures are the ’full“ type-structures and the ’term model“ of

lbh(p)t . That is, SetC, where C is a collection of sets, and Term = ({Terms}sÎTp, [ ] ), where

Terms is the set of terms of type s modulo bh convertibility.

8.7.5 Definition Let C be a CCC, with terminal object t and projections fst, snd. Suppose one

has a map I associating every atomic type A with an object of C. Then the categorical

interpretation is as follows:

- Types: [s] = I(s) if s is atomic

[s®t] = [t][s]

193

8. Formulae, Types, and Objects

[s´t] = [s] ´ [t]

- Terms: let Ms be a term of lbhpt, with FV(Ms) Í D = {xs1,É,xsn}, and assume that

A, A1 , É , A n interpret s, s1 , É , s n (we omit typing, when unambiguous, and write

p i ÎC[t´A 1 ´...´A n ,Ai ] for the projection pi : t´A 1 ´...´A n ® A i ). Then [M s ] D is the

morphism in C[t´A1´...´An,A] defined by

[xsi]D = pi

[MN]D = eval ° <[M]D, [N]D>

[lxt.M]D = L([M]DÈ{xt} )

[<M, N>]D = <[M]D , [N]D >

[fst (M)]D = fst ° [M]D

[snd (M)]D = snd ° [M]D .

8.7.6 Substitution Lemma

i. If ys ÏFV(N) , then [N]DÈ{ys } = [N]D ° fst

ii. [ [N/xs]M ]D = [M]DÈ{xs} ° <id,[N]D> (types are omitted when unambiguous).

Proof

i. By induction on M. The following is the typical case:

[lxt.P]DÈ{ys } = L([P]DÈ{ys, xt} )

= L([P]DÈ{xt,ys}°x) for x: (aD´as)´at @ (aD´at)´as

= L([P]DÈ{xt}°fst°x ) by induction

= L([P]DÈ{xt}°fst´id) as fst°x = fst´id

= L([P]DÈ{xt}) ° fst by the naturality of L.

ii. By induction on M:

M º xs

[xs ]DÈ{xs } ° <id,[N]D > = snd ° <id,[N]D >

= [N]D

= [ [N/ xs ] xs ]D

M º xs i

[xsi]DÈ{xs} ° <id,[N]D> = pi ° fstT´A1´...´An ,A ° <id, [N]D> (si¹s)

= pi

= [xs i]D

M º QP

[QP]DÈ{xs} ° <id,[N]D> = eval ° <[Q]DÈ{xs},[P]DÈ{xs} > ° <id,[N]D>

= eval ° <[Q]DÈ{xs }°<id,[N]D >,[P]DÈ{xs }>°<id,[N]D >

= eval ° <[ [N/xs] Q ]D,[ [N/xs]P ]D>

= [ [N/xs] PQ ]D

194

8. Formulae, Types, and Objects

M º lyt.P

[ [N/xs] lyt.P ]D = L([ [N/xs]P ]DÈ{yt})

= L([P]DÈ{yt,xs}° <id,[N]DÈ{yt}>) by induction

= L([P]DÈ{yt,xs}° <id,[N]D°fst>) by (i)

= L([P]DÈ{xs ,yt}) ° <id,[N]D > by naturality (as in (i))

= [ly t.P]DÈ{x s } ° <id,[N]D >.

As for pairing and projection, the computation is easy and is left for exercise. ¨

The lemma may suffice to give an interpretation of lbhpt over an arbitrary CCC. Indeed, nothing

else is required from a purely categorical perspective, i.e., adopting a more suitable notion of model.

In particular, it is worth noting that the previous categorical semantics of the typed lambda calculus

really ’fills the triangle“ we talked about at the beginning of this section. We leave it as an exercise for

the reader to verify that a term and its categorical interpretation with respect to the previous definition

are actually associated with the same derivation in intuitionistic logic.

However, as many, since Tarski, are used to interpreting formal systems into mathematical

structures by first assigning values to variables by means of environments as set-theoretic maps, we

complete the construction of models (as defined at the beginning of the section) with the following

exercise and theorem.

Exercise Prove a version of lemma 8.7.6 in the style of definition 8.7.2. That is, show that in any

model and for any environment h, one has (we omit types for simplicity)

[M]h[[N]h/xs] = [ [N/xs]M ]h .

This gives axiom (b) in the model.

8.7.7 Theorem Any CCC with enough points C and any collection {ai}iÎAt of objects in C

yield a model of lbhpt .

Proof Let C be the given category and let A = {|ai| / iÎAt} be the collection of sets in Cset that

interpret the atomic types. Then the model is given by the type structure TSA = CsetA, i.e., the

higher types are interpreted by |cs´t| and |cs®t| . As a matter of fact, let h : Var ® UsÎTp{|cs|}

be an environment. Fix Ms and let FV(Ms) Í D = {xs1,É,xsn} . By definition, h(xsi)Î|csi|,

then set hD = <id,h(xs1),...,h(xsn)>ÎC[t,t´cs1´...´csn] and define

[M s ]h = [M s]D°hDÎ |cs|.

It is now easy to check that the map Fh , defined by Fh (e) = h[e/x]D , for eÎ |c s |, is in

C set[|cs |,|cs1 ´...´csn | ]. Thus, there exists h'ÎC[cs ,cs1 ´...´csn ] such that Fh = h'°_ and,

hence, h[e/x]D = h'° e. This fact and the substitution lemma guarantee that [ _ ] is a well-defined

interpretation map and, thus, that CsetA is a model. ¨

195

8. Formulae, Types, and Objects

We now need to prove the converse and construct a CCC out of every model of lbhpt. Observe first

that by functional application, over a type structure, one may define algebraic functions as follows.

8.7.8 Definition Given a type-structure TS C = {Cs } sÎTp , the typed monomials over TS C

are defined by

asÎCs, ... are typed monomials, for all sÎTp

constants

xs, ys,.... are typed monomials, for all sÎTp

variables

Ms®t(Ns) is a typed monomial, when Ms®t and Ns are typed monomials.

application

A function f : Cs®Ct is algebraic if f(as) = [as/xs]Mt for some typed monomial Mt .

The intuition is that algebraic functions will give the morphisms of a ’rich enough“ category as to

interpret typed l-terms. It is clear, for example, that projections are algebraic functions: just set

send((xs, yt)) = xs, then snd : Cs´t ®Ct is the second projection.

8.7.9 Lemma Given a type-structure TSA = {As}sÎTp , one obtains a category with enough

points by taking the singleton set, the As 's as objects and the algebraic functions as morphisms.

Call this category CTSA.

Proof Exercise. ¨

8.7.10 Theorem Let TS A = {As } sÎTp x be a model of lbhp t and let CTS A be as in the

lemma. Then CTSA is a CCC.

Proof Products are defined by taking As´At = As´t. Then, if the typed monomial M defines f

and N defines g, <M,N> defines <f,g>, as the formal pairing and projections behave as required

in Cartesian categories.

As for exponents, set AtAs = As®t . Then

eval : At®r´At®Ar is defined by x |_ fst xt®r´t(snd xt®r´t).

Moreover, if f : As´At®Ar is defined by M,

L(f) : As®ArAt is defined by lxt.M.

Finally observe that axiom (b) gives (bcat) in definition 2.3.1, while (h) gives (hcat). ¨

By the following exercise we let the careful reader relate the two interpretations of l-terms given so

far.

Exercise Compare in detail the categorical and set-theoretic meanings of terms. Namely, start with

a TSA, which is a model, and construct a CTSA as in 8.7.9. (Note that in this construction, lots of

- irrelevant - morphisms may be lost). Then construct a new TS' A as in 8.7.7 (this will be a

’substructure“ of TSA, up to an obvious identification). Consider now an interpretation [ - ]h over

196

8. Formulae, Types, and Objects

TSA, where the range of h, though, is restricted to TS'A. Define [ - ]D as in 8.7.5 over CTSA

and, finally, give [ - ] 'h over TS' A by using h and [ - ]D as in 8.7.7. Prove then that [ - ] h

and [ - ] 'h coincide. Thus, we moved from TSA to CTSA and to TS'A, preserving the meaning

of terms.

Conversely, by an even longer and more tedious proof, go from an interpretation [ - ]D over a

Cartesian closed category C, to a model TS A , where the interpretation [ - ] h is given by 8.7.7.

Construct then a CTSA as in 8.7.9 and observe that it may be faithfully embedded into C. Relate by

this [ - ]D, over C, and the interpretation [ - ]'D, given as in 8.7.5, over CTSA. (The connection

between set-theoretic and categorical meaning of terms will be more closely investigated for the type-

free case in the next chapter).

8.8 Fixpoint Operators and CCCs

The typed lambda calculus is strongly normalizable, that is:

1. every computation terminates, and

2. the computation is independent from the evaluation strategy.

The latter property is surely very attractive for a computational language since it greatly simplifies its

semantics: the programmer, in the design of the code, does not have to fuss over the operational

evolution of reduction, but can concentrate on the denotation of the program in its strongest meaning.

Considered by itself, the first property also seems to be quite interesting, but it has the rather

annoying corollary that not all ’computable“ functions (e.g., Turing-computable) will be computable

in the language. The problem is not only related to the abstract expressiveness of the language; in

today•s computer science, the idea of ’general purpose“ language is no longer considered as central as

it was twenty years ago, and the loss of the ability to compute, for example, the Ackermann function,

does not worry anybody: primitive recursive functions are surely enough for most interesting

applications. What makes the general recursive formalism more attractive than the primitive recursive

one, is that it is much easier to write code in the general formalism (also for computing a primitive

recursive function).

Coming back to the typed lambda calculus, it is otherwise too poor for any application, so we face

the problem of extending the language with more powerful constructs. In chapter 11, we shall study

the ’second order“ or ’polymorphic“ extension, which still has the nice property of strong

normalization together with a great formal expressiveness (although, as a programming language, it

imposes on the programmer a completely new approach to the design of the code). We study for the

moment a simple extension by means of fixpoint operators, which enables us to write recursive

definitions of functions.

The reader should be aware, though, that a price must be paid when extending typed languages by

fixpoint operators. The problem is related to the Curry-Howard analogy (see section 8.3). Remember

197

8. Formulae, Types, and Objects

that a (constructive) proof of a formula A corresponds with a closed l-term of type A in type

theory, and, thus, a formula is provable in the logic if and only if the corresponding type is

’inhabited“ in type theory. The existence of fixpoint operators has as a consequence that all types are

inhabited, or, from the logical point of view, that all formulae are provable (see later). Thus fixpoint

operators have no logical correspondent; nevertheless, the calculus they originate is not inconsistent

from the point of view of the equational theory of programs (that is, not all terms happen to be

provably equal). This is shown by the models below.

In conclusion, the programmer, in the present context, must decide whether to acquire the full

expressive power and the elegance of programming by ’recursive definitions“ or to preserve the

advantages of the ’types as formulae“ paradigm. This choice depends on the specific applications he

or she has in mind.

8.8.1 Definition A fixpoint operator of type s is a term Qs of type (s®s)®s such that , for

every term Ms®s one has

Ms®s (Qs Ms®s) = Qs Ms®s.

By fixpoint operators one can simulate recursive definitions in the following way:

letrec fs be Ms[f] in Ng[f]

becomes

(lhs.Ng) ( Qs(l fs.Ms))

Note that for every type s we have at least an object of that type, obtained as a fixpoint of the

identity

Qs (lxs.xs).

We consider next the problem of giving an interpretation to fixpoint operators. As we need to

interpret typed l-calculi, this will be done in suitable CCC's.

8.8.2 Definition Let b be an object of a CCC C. A fixpoint operator for b is a morphism

Fixb : bb ®b such that Fixb = evalb,b° <id,Fixb >. A category has fixpoint operators if each

object b has a fixpoint operator Fixb .

In every CCC with fixpoint operators, it is easy to give meaning to the axiom

fix. Ms®s ( Qs Ms®s) = Qs Ms®s

by letting

{Qs}D = L( Fixs ° snd) ° !D,

where snd: t´ss®ss, and !D is the unique arrow from D to the terminal object t.

Indeed, one has the following:

198

8. Formulae, Types, and Objects

{ M(Qs M) }D = eval ° <{M}D, { (Qs M) }D>

= eval ° <{M}D, eval ° < L( Fixs ° snd) ° !D, {M}D> >

= eval ° <{M}D, Fixs ° {M}D >

= eval ° < id, Fixs > ° {M}D

= Fixs ° {M}D

= eval ° < L( Fixs ° snd) ° !D, {M}D>

= { (Qs M) }D.

It is not difficult to find CCC•s with fixpoint operators. The most well-known example is

probably the category CPO, with complete partial order for objects and continuous functions for

morphisms (remember that, in CPO, f: A®B is continuous if and only if f is monotonic and for

every directed subset D of A, f(È(D)) = Èf(D); every c.p.o.has a least element, ^ = ÈÆ ).

Observe that, given a c.p.o. C and a continuous function f , we can form a chain

{fn(^C)}nÎw = ^C £ f(^C) £ f(f(^C)) £ .... £ fn(^C) £ ....

starting from the bottom element ^C. The next two results develop this example.

8.8.3 Theorem Let C be a CPO, let ^C be its least element, and let f: C®C be a continuous

function. Then È{fn(^C)}nÎw is the least fixed point of f .

Proof: Note that È{fn(^C)}nÎw = È{fn+1(^C)}nÎw . Then

f(È{fn(^C)}nÎw) = Èf{fn(^C)}nÎw)

= È{fn+1(^C)}nÎw).

Moreover, if c is another fixed point, then we prove by induction that, for all n, fn (^ C ) £ c.

Indeed,

^C £ c

fn(^C) £ c •Þ fn+1(^C) £ f(c) = c.

Then, by definition of least upper bound, È{fn(^C)}nÎw £ c. ¨

8.8.4 Definition Let C be a c.p.o. Define then FixC : CC ®C the function that takes every

continuous function f: C®C to È{fn(^C)}nÎw .

8.8.5 Proposition FIX C : CC ®C is continuous.

Proof Exercise. ¨

In a more general setting, the existence of exponents, in CCC's, suggests the investigation of

those ’paradoxical“ objects that ’contain,“ as a retract, their own function space; namely, the reflexive

objects of section 2.3 (see also below). They will turn out to be rather relevant in the next chapter,

where examples are given, and in chapter 10, where the idea will be generalized to fixpoint

constructions over types, namely to the categorical counterpart of recursive definitions of data types.

199

8. Formulae, Types, and Objects

Remember (see definition 1.4.2) that in a category C, a < b via the retraction (i,j) iff j » i = ida.

In these assumptions, i turns out to be mono and j epic. Thus a retract a of b is a subobject of

b, up to isomorphisms. An object V is reflexive iff VV < V (see definition 2.3.5). We next show

how to construct another simple model of the typed lambda calculus with fixpoint operators, by using

the category RetV of retracts over a reflexive object V. Recall that, given an object V in a category

C, the category RetV is defined as follows (see definition 1.4.4):

ObRetV = { fÎC[V,V] | f ° f = f }

MorRetV = { (f, k, g) | f, gÎObRetV , kÎC[V,V] , k = g ° k ° f }

dom( (f, k, g) ) = f , cod( (f, k, g) ) = g

idf = (f, f, f)

(f, k, g) ° (g', k', f) = (g', k ° k', g)

Proposition 8.8.6 below proves that, if V is a reflexive object in a CCC C, then RetV is Cartesian

closed too. In theorem 8.8.8 we will prove that, given a reflexive object V in an arbitrary CCC,

every object f in RetV has a fixpoint operator Fixf .

8.8.6 Proposition If C is a CCC and V is a reflexive object in C, then RetV is a CCC.

Proof By proposition 2.3.6, we know that the terminal object t and V´V are both retracts of V

(by definition of reflexive object also VV<V ). Suppose the following:

t<V via in, out

V´V < V via in', out'

VV < V via in", out".

Let 1= in ° out : V®•V. 1 ° 1= in ° out ° in ° out = in ° out = 1. 1 is the terminal object of RetV . If

f is an object in RetV, then !f: f®1 is (f,1,1). Note that (f,1,1) is a well-defined morphism, since

1= 1 ° 1 ° f for the terminality of t. Moreover, if (f,g,1) is another morphism, then g = 1 ° g ° f =

1, again for the terminality of t .

Given two objects f and g in RetV , their product is f„g = in' ° f´g ° out': V®V. (In the

present proof only, „ has this meaning)

Note that

f„g ° f„g = in' ° f´g ° out'° in' ° f´g ° out'

= in' ° f´g ° f´g ° out'

= in' ° f´g ° out'

= f„g.

The projections are ( f„g, fst, f), ( f„g, snd, g) where

fst = p1 ° out' ° f„g : V®V

snd = p2 ° out'° f„g : V®V

and p1, p2 are the projections associated in C to the product V´V.

The pairing operation <,>ret is defined as follows: given two morphisms (c,h,f) and (c,k,g) set

200

8. Formulae, Types, and Objects

< (c,h,f), (c,k,g) > ret = (c, in'° <h,k>,f„g)

where <,> is the pairing in C.

This is a good definition, since

f„g ° in'° <h,k> ° c = in' ° f´g ° out' ° in'° <h ° c, k ° c > by def. of f„g

= in' ° f´g ° <h ° c, k ° c >

= in'° <f ° h ° c, g° k ° c >

= in'° <h, k >.

We have still to prove the equations associated with the product; we only prove that

( f„g, fst, f) ° < (c,h,f), (c,k,g) > ret = (c,h,f)

and leave the other proofs as an exercise for the reader. We have the following:

( f„g, fst, f) ° < (c,h,f), (c,k,g) > ret =

= ( f„g, fst, f) ° (c, in'° <h,k>,f„g)

= ( c, fst ° in'° <h,k>, f) by composition in RetV

= ( c, p1 ° out' ° f„g ° in'° <h,k>, f) by def. of fst

= ( c, p1 ° out' ° in' ° f´g ° out' ° in'° <h,k>, f) by def. of f„g

= ( c, p1 ° f´g ° <h,k>, f) = (c,h,f).

The functor „ is defined on morphisms in the usual way (namely, f´g = <p1 ° f, p2 ° g> ).

Specifically, given two morphisms (c,h,f) and (d,k,g):

(c,h,f) „ (d,k,g) = < (c,h,f) ° (c„d, fst , c), (d,k,g) ° ( c„d, snd, d) >ret

= < (c„d, h ° fst , f), ( c„d, k° snd, g) >ret by composition in RetV

= ( c„d, in' ° < h ° fst, k° snd >, f„g ) by def. of <,>ret

= ( c„d, in' ° < h ° p1 ° out' ° c„d, k ° p2 ° out'° c„d >, f„g ) by def. of fst, snd

= ( c„d, in' ° < h ° p1, k ° p2> ° out' ° c„d, f„g )

= ( c„d, in' ° h´k ° out' ° c„d, f„g ).

We are now in a position to define the exponents. If h, k : V®V, let [h,k] = L(k ° evalV,V °

(id´h)) : VV®VV. Given two objects f and g in RetV, their exponent is:

gf = in" ° [f,g] ° out": V®V.

This is a good definition, since

gf ° gf = in" ° [f,g] ° out" ° in" ° [f,g] ° out" by def. of gf

= in" ° [f,g] ° [f,g] ° out"

= in" ° L(g ° evalV,V ° (id´f)) ° L(g ° evalV,V ° (id´f)) ° out" by def. of [f,g]

= in" ° L(g ° evalV,V ° (id´f) ° L(g ° evalV,V ° (id´f))´id ) ° out"

= in" ° L(g ° evalV,V ° L(g ° evalV,V ° (id´f))´id ° (id´f) ) ° out"

= in" ° L(g ° g ° evalV,V ° (id´f) ° (id´f) ) ° out" by (b)

= in" ° L(g ° evalV,V ° (id´f) ) ° out" since g, f are retractions

= in" ° [f,g] ° out" by def. of [f,g]

= gf by def. of gf.

201

8. Formulae, Types, and Objects

The evaluation function is ( gf„f, ev, g) where

ev = evalV,V ° (out"´id) ° out' ° gf„f

The currying operation Lret is so defined: given a morphism (c„f,h,g),

L ret(c„f,h,g) = (c, in"° L(h ° in'), gf ).

This is a good definition of morphism in RetV; indeed

gf ° in"° L(h ° in') ° c =

by def. of gf

= in" ° L(g ° evalV,V ° (id´f) ) ° out" ° in"° L(h ° in') ° c

= in" ° L(g ° evalV,V ° (id´f) ) ° L(h ° in' ° c´id)out" ° in" = id

= in" ° L(g ° evalV,V ° (id´f) ° L(h ° in' ° c´id)´id)

= in" ° L(g ° evalV,V ° L(h ° in' ° c´id)´id ° (id´f) )

= in" ° L(g ° h ° in' ° c´id ° id´f ) by (b)

= in" ° L(g ° h ° in' ° c´f)

= in"° L( g ° h ° c„f ° in') by def. of c„f

= in"° L(h ° in').

We only prove the axiom b, and leave as an exercise for the reader to prove h .

(gf„f, ev, g) ° ( L ret(c„f,h,g) „ (f, f, f) ) =

= (gf„f, ev, g) ° ( (c, in"° L(h ° in'), gf ) „ (f, f, f) ) by def. of L ret

= (gf„f, ev, g) ° ( c„f, in' ° (in"° L(h ° in'))´f ° out' ° c„f , gf„f) by def. of „ on arrows

= (c„f, ev ° in' ° (in"° L(h ° in'))´f ° out' ° c„f , g) by composition in RetV

= (c„f, evalV,V ° (out"´id) ° out' ° gf„f ° in' ° (in"° L(h ° in'))´f ° out' ° c„f, g)

by def. of ev

= (c„f, evalV,V ° (out"´id) ° gf´f ° (in"° L(h ° in'))´f ° out' ° c„f , g) by def. of gf„f

= (c„f, evalV,V ° (out" ° gf ° in"° L(h ° in'))´f ° out' ° c„f , g ) as f ° f = f

= (c„f, evalV,V ° (L(g ° evalV,V ° (id´f)) ° L(h ° in'))´f ° out' ° c„f , g) by def. of gf

= (c„f, evalV,V ° ( L(g ° evalV,V ° L(h ° in')´id ° (id´f) )´f ° out' ° c„f , g)

= (c„f, evalV,V ° L(g ° h ° in'° id´f )´f ° out' ° c„f , g) by b

= (c„f, g ° h ° in'° id´f ° c´f ° out' , g) by b

= (c„f, g ° h ° c„f , g)

= (c„f,h,g).

This completes the proof that RetV is a CCC. ¨

8.8.7 Lemma If V is a reflexive object in a CCC C, then there is a fixpoint operator Fix:

V V ®V.

Proof Let

F = eval ° <id, in"> : VV®V

H = L( eval ° (id´(F°out")) ) : VV®VV

Fix = F°H is a fixpoint operator for V; indeed,

202

8. Formulae, Types, and Objects

F°H = eval ° <id, in"> ° L( eval ° (id´(F°out")) )

= eval ° L( eval ° (id´(F°out")) )´id ° <id, in" ° L( eval ° (id´(F°out")) ) >

= eval ° id´(F°out") ° <id, in" ° L( eval ° (id´(F°out")) ) >

= eval ° <id, F ° L( eval ° (id´(F°out")) ) >

= eval ° <id, F°H >. ¨

8.8.8 Theorem Every object f in RetV has a fixpoint operator Fixf .

Proof Let Fix: VV®V be a fixpoint operator for V. Define

Fixf = (ff, Fix ° out" ° ff , f).

We leave it to the reader to prove that this is a good definition, that is:

(*) Fix ° out" ° ff = f ° Fix ° out" ° ff ° ff.

We must prove that

Fixf = ( ff„f, ev, f) ° < (ff, ff, ff), Fixf>,

where ev = evalV,V ° (out"´id) ° out' ° ff„f.

Compute then

Fixf = (ff, evalV,V° <id,Fix> ° out" ° ff, f) by def. of Fixf

= (ff, evalV,V ° < out" ° ff, f ° Fix ° out" ° ff>, f) by (*)

= (ff, evalV,V ° (out"´id) ° ff´f ° < ff, Fix ° out" ° ff>, f)

= (ff, evalV,V ° (out"´id) ° out' ° ff„f ° in' ° < ff, Fix ° out" ° ff>, f -) by def. of ff„f

= (ff, ev ° in' ° < ff, Fix ° out" ° ff>, f) by def. of ev

= ( ff„f, ev, f) ° (ff, in' ° < ff, Fix ° out" ° ff>, ff„f) by composition in RetV

= ( ff„f, ev, f) ° < (ff, ff, ff), (ff, Fix ° out" ° ff, f) > by pairing <,> in RetV

= ( ff„f, ev, f) ° < (ff, ff, ff), Fixf >. ¨

References. For an introduction to Proof Theory, natural deduction, and intuitionisitic logic, the

reader can consult Prawitz (1965) and Takeuti (1975). In particular, the latter inspired our

presentation of the cut-elimination theorem. The ’formulae as types“ analogy is explained in Howard

(1980), but the main ideas go back to work of Curry. The connections between l-calculus and

CCC•s were first explored by Lambek. The equivalence is shown in Lambek (1980) and Scott

(1980). A full account of the relation between l-calculus, CCC•s, and Proof Theory may be found in

Lambek and Scott (1986). We tried here to complement that work by relating it to Tarskian semantics

and emphasizing the role of ’structures,“ for the convenience of the reader who may begin with our

approach and continue with further, more abstract readings. In section 8.7, we dealt only with

CCC's, i.e., with the models of l b h p t. Weaker calculi, that is, typed combinatory logic and l b p t,

are discussed in Hayashi (1985) and Martini (1988), which introduce various notions of ’weak

Cartesian closedness“ for this purpose.

203

9. Reflexive Objects and the Type-Free Lambda Calculus

Chapter 9

REFLEXIVE OBJECTS AND

THE TYPE-FREE LAMBDA CALCULUS

The main aim of this book is to present category theoretic tools for the understanding of some

common constructions in computer science. This is largely done in the perspective of denotational

semantics, in particular in this second part of the book. It is commonly agreed that a fruitful area of

application of denotational semantics has been the understanding and, in some cases, the design of

functional languages. This is exactly because the theory of the intended structures is a ’theory of

functions,“ indeed Category Theory.

Functional languages are based on the notion of application and functional abstraction. That is

programs are ’applied,“ like functions, to data and, given the formal, algebraic definition of a

function, it may be turned into an applicative program by ’functional completeness“ or ’lambda

abstraction.“ Observe that the expressive power is mostly based on recursive definitions, even though

a different approach is suggested by the higher order calculi discussed in chapter 11.

The aim of this chapter is to clarify the categorical significance of the quoted expressions in the

previous paragraph, e.g., ’applied“, ’functional completeness“, ’lambda abstraction“, ’uniform“,

’recursive definition“, in the context of a ’type-free“ programming style. In the previous chapter we

dealt with the typed l-calculus, and we discussed typed functional ’application“ and ’abstraction“

which have an immediate interpretation in CCC's. As already mentioned, it is easy to conceive a

variant of the previous calculus by just erasing all type restrictions in the term formation rules. This

defines the (type-free or un(i)typed) l -calculus, where there is no distinction between functions

and data. (In remark 9.5.12 we will suggest some good reasons by which one may better like to

consider the type-free l-calculus as a typed calculus with just one type: a unityped calculus). The set

L of terms of the l-calculus is thus defined by means of the following rules, starting by a given set

of (type-free) variables V:

Variables if xÎV, then xÎL;

Application if MÎL, and NÎL then MNÎL;

Abstraction if MÎL, then lx.MÎL.

Free and bound occurences of a variable in a term, and the substitution [N/x]M of a term N for a

variable x in M, are defined as for the typed calculus. As usual, we identify terms that differ from

each other only for the names of bound variables (a-conversion).

The l -theory deals with the convertibility M = N of two terms M and N. It is axiomatized

by the rules

b. (lx.M)N = [N/x]M , for x free for N in M

h. ly.My = M , for y not free in M (write yÎFV(M) )

204

9. Reflexive Objects and the Type-Free Lambda Calculus

toghether with the axioms and rules needed for turning ’=“ into a congruence relation.

The l-calculus is the prototype of every untyped functional programming language. Many

functional languages were directly derived from the l-calculus, from Landin's ISWIM (a notational

variant of l-calculus with an explicit recursive operator) to Edinburgh ML. Even McCarthy•s

language LISP, the first running functional programming language, and still one of the most used in

several applications of computer science, is greatly endebted to the l-calculus. Besides the l-

notation, LISP inherits from l-calculus both the formal elegance and the concise syntax, essentially

adding only a few primitives for list manipulation. The main difference is in the binding strategy for

variables, which is static for l-calculus and dynamic for LISP. For example, without taking into

account the inessential syntactic differences between the two formalisms, let us see how the following

expression is evaluated in the two languages:

(lz. (ly. (lz.yM)N ) (lx.xz) )P

In l-calculus, we have the following reduction sequence of reductions:

(lz. (ly. (lz.yM)N ) (lx.xz) )P ® ly. (lz.yM)N ) (lx.xP)

® lz. (lx.xP)M)N

® (lx.xP)M

® MP

In contrast to this, LISP will first bind z to P, then bind y to lx.xz; next z will be rebound to

N, and finally yM will be evaluated. This means that x will be bound to M, and then Mz is

evaluated. Since LISP uses dynamic binding, the latest active bindings of the variable z is used,

i.e., the evaluation of (lz. (ly. (lz.yM)N ) (lx.xz) )P is reduced to the evaluation of MN.

This has been often considered as an anomaly of LISP: in many LISP dialects, there are syntactic

constructs for defining functions that guarantee a static binding for their formal parameters and,

moreover, some recent LISP-like languages have completely converted to static binding (e.g.,

Scheme). A first consequence of dynamic binding is that the rule of a-conversion does not hold any

more: in the example above, if we replace z with another variable in lz.yM, we obtain a different

behavior. LISP violates referential transparency, while l-calculus does satisfy it. This is not only a

merely theoretical property: in programming terms, referential transparency means that, in order to

understand a structured program, we need only to understand the denotation of the subprograms, and

not their connotations (for example, we do not need to be concerned with the naming of variables

used within the programs). These ideas are expressed in the philosophy of modular programming,

that is of the programming style that requires the construction of program segments as self-contained

boxes, or modules, with well-defined interfaces. We shall discuss in the last chapters of this book

how this philosophy applies so well to strongly typed polymorphic languages.

The current treatment of both programming concepts of referential transparency and modularity

provides a relevant example of an area that is greatly indebted to twenty-odd years work of in

denotational semantics. We present in this chapter the categorical understanding of the semantics of

205

9. Reflexive Objects and the Type-Free Lambda Calculus

type-free Combinatory Logic and l-calculus, whose challenging mathematical meaning actually

started that work. In section 9.4, we hint at how the categorical approach suggested a new set of

combinators and a simple abstract machine for implementig head reduction (CAM).

9.1 Combinatory Logic

Combinatory Logic (CL) is based on an even simpler language than l-calculus: it just contains

variables and two constant symbols K and S. Their operational behaviour is axiomatized by the

rules for equality and

k. Kxy = x

s. Sxyz = xz(yz)

where, as for the l-calculus, M1M2...Mn stands for (...(M1M2)...Mn).

The expressive power of l-calculus and CL is due to their combinatorial completeness. That is,

for any variable x and term M in their languages, there exists <x>M such that

abs. (<x>M)N = [N/x]M , and xÏFV(<x>M).

For the l-calculus, this comes with the definition: just set <x>M = lx.M. As for CL, define

inductively

<x>x = I º SKK;

<x>M = KM, if M does not contain x;

<x>MN = S(<x>M)(<x>N).

(In general, for x = x1, ...,xn, set <x>M = <x1>...(<xn>M) ).

As a matter of fact, CL is the simplest type-free language which is functionally complete;

moreover, and surprisingly enough, in 1936 Kleene proved that CL is powerful enough to compute

all partial recursive functions.

Note that in type-free universes, there is no distinction between data and functions. In set-

theoretic terms, this means that it is possible to apply one to the other in an undistinguished

applicative structure (X,.), i.e., a set X with a binary operation . .

9.1.1 Definition A model (X,., K, S) of CL, called Combinatory Algebra, is an applicative

structure (X,.) with two distinguished elements K, SÎX such that

(K .x).y = x

"x,y

"x,y,z ((S .x) .y) .z = (x.z).(y .z) .

As usual, we suppose that the operation . of the applicative structure associate to the left; moreover

we shall usually omit it when writing terms. For instance, (K.x).y will be simply written as Kxy.

206

9. Reflexive Objects and the Type-Free Lambda Calculus

9.1.2 Definition Given an environment x , that is a map from the set of variables of CL to X, the

interpretation [M]x of a combinatory term M in x, is inductively defined as follows:

[K]x = K

[S]x = S

[x]x = x(x)

[MN]x = [M]x[N]x .

An interesting semantic consequence of (abs) is the following lemma which will be used later on.

9.1.3 Lemma Let ( X,., K, S) be a Combinatory Algebra. For any combinatory term M, any

environment x and any aÎX,

[<x>M]x .a = [M]x(x=a)

where x(x=a) is the environment defined by : x(x=a)(z) = if x=z then a else x(z) .

Proof [<x>M] x . a = [<x>M]x .[x]x(x=a)

= [<x>M]x(x=a) .[x]x(x=a) since x do not occur in <x>M

= [(<x>M)x]x(x=a)

= [M]x(x=a) by (abs). ¨

Clearly, the l-calculus is at least as expressive as CL, since Kl º lxy.x and Sl º lxyz.xz(yz)

represent K and S in l-calculus (and do the same job). By this definition of K and S we obtain a

sound translation form CL to l-calculus, i.e., a translation which preserves term equalities. In the

other direction, the abstraction mechanism <x>M described above naturally suggests the following

translation.

9.1.4 Definition Given a l-term M, the associated term M CL in Combinatory Logic is

inductively defined by

xCL = x

(MN)CL = MCLNCL

(lx.M)CL = <x>MCL.

Unfortunately, this translation is not sound, that is, not all the equations provable in the l-theory still

hold after the translation. Consider for example the two equal terms M º ly.x and N º ly.(lz.z)x.

Their translation by means of combinators is, respectively:

MCL = (ly.x)CL

= <y>xCL

= <y>x

= Kx

207

9. Reflexive Objects and the Type-Free Lambda Calculus

NCL = (ly.(lz.z)x)CL

= <y>((lz.z)x)CL

= <y>((lz.z)CLxCL)

= <y>((SKK)x)

= S((<y>(SKK)) <y>x )

= S((K(SKK))Kx)

and Kx ¹ S((K(SKK))Kx).

The problem derives from the fact that in Combinatory Logic M = N does not imply <x>M =

<x>N. This fact is independent from the particular abstraction mechanism adopted and it is actually

related to the absence of a ’canonical“ choice for <x>M (see references).

From the point of view of computer science, the interest in Combinatory Logic derives more from

implementation then from semantics. Indeed, b-conversion, as it is formulated in the l-calculus, give

rise to the well-known, conceptually simple, but syntactically fastidious problem of name clashes.

For instance, M º (lxy.x)y does not reduce to ly.y, but to lz.y. This kind of problems does not

sussist in Cominatory Logic, which thus provides a convenient intermediate code where the l-

calculus can be compiled before execution. For example, the previous term M is compiled as:

MCL = ((lxy.x)y)CL

= (lxy.x)CL (y)CL

= (<x>Kx)y

= S(KK)(SKK)y

and its reduction, using, say, an innermost-leftmost strategy, yields:

S(KK)(SKK)y = (KKy)(SKKy)

= K(SKKy)

= K((Ky(Ky))

= Ky .

9.2 From Categories to Functionally Complete Applicative Structures

In this section, we suggest how to understand, in categorical terms, the difference between

’functional completeness“ and ’lambda abstraction“ and, later, characterize both notions, in absence

of type constraints. As mentioned in the introduction, CL is the simplest type-free language that is

functionally complete, since, for every term M, there exists <x>M that satisfies (abs). In case the

choice of <x>M is ’uniform in M“, one has lambda abstraction and l-calculus: i.e., <x>M is

canonically given by lx.M.

In order to give categorical meaning to this complex situation, we proceed as follows: we start

with recovering applicative structures, in particular functionally complete ones, in Cartesian

208

9. Reflexive Objects and the Type-Free Lambda Calculus

categories (see 9.2.1-9.2.5); then we shift to the realm of Cartesian closed categories, where the

existence of function spaces (exponents) allows a better understanding of the notion of functional

completeness (9.2.6-9.2.7) and lambda-abstraction (9.2.8-9.2.12). In section 5, we will give a fully

categorical characterization of models of these type-free calculi.

9.2.1 Definition Let C be a Cartesian category, T its terminal object, and U an object in C,

with T < U and uÎC[U´U,U]. The applicative structure associated to u, A(u), is given

by A(u) = (C[T,U],.), where a.b = u° <a,b>.

In a category with a terminal object T, T < U simply generalizes the set-theoretic notion that U is

’not empty“. Clearly, A(u) is nontrivial (i.e., it contains at least two elements) iff T < U is strict,

i.e., is not an isomorphism.

9.2.2 Definition Let C be a cartesian category. Then uÎC[X´Y,Z] is Kleene-universal (K-

universal) if "fÎC[X´Y,Z] $sÎC[X,X] f = u° (s´id) , i.e.,

Kleene-universality is a weak (co)universality property, since no unicity of s is required. It has an

obvious recursion-theoretic meaning: indeed K-universality generalizes the s-m-n (iteration) theorem,

with X = Y = Z = w and with f a (total) recursive function, i.e., a morphism from (w,id)´(w,id)

to (w,id), in the category EN of numbered sets.

9.2.3 Definition Let C be Cartesian and uÎC[X´X,X]. Then u(n)ÎC[X´X n,X] is inductively

defined by u(0) = id, u(n+1) = u(n)° (u´idn), that is,

u´idn u(n)

u(n+1): X´X´Xn _______> X´Xn ______> X , where Xn+1 = X´Xn.

It is easy to observe that u(n) corresponds exactly to the application of n+1 arguments, from left to

right, e.g. u(2)°<a,b,c> = u°(u´id)°<a,b,c,> = u°<u°<a.b>,c>. We write a.b.c for (a.b).c .

9.2.4 Lemma Let C be Cartesian. Assume that, for some U in C, U´U < U and there is a K-

universal uÎC[U´U,U]. Then "n u(n)ÎC[U´Un,U] is K-universal.

209

9. Reflexive Objects and the Type-Free Lambda Calculus

Proof By assumption, this is true for n = 1. Let U´U < U via (i,j) and fÎC[U´U n+1 ,U].

Then, by the inductive hypotesis, for some s(n)ÎC[U,U] the following diagram commutes:

By assumption, for some sÎC[U,U] one also has

f ° (j ´ idn ) ° (i ´ idn )

Then compute f=

u(n) ° (s(n) ´ idn) ° (i ´ idn)

= by (1)

u(n) ° (u ´ idn) ° (s ´ idn+1)

= by (2)

u(n+1) ° (s ´ idn+1). ¨

=

9.2.5 Theorem Let C be a Cartesian category. Assume that, for some object U, one has T < U,

U´U < U and there exists a K-universal uÎC[U´U,U]. Then A(u) is a combinatory algebra.

Proof Let T < U via (iT ,jT ). Then, by lemma 9.2.4, "n, "fÎC[Un,U] $sÎC[U,U] such that

the following diagram commutes, with [f] = s ° iT (we write i and j for iT and jT):

Thus, u(n)°[f]´dn = idT´f = f. Since u(n) is the application, from left to right, of its n+1 arguments,

[f] ’represents“ f, with respect to application. By 9.2.1, we only need to define fÎC[U2,U] and

gÎC[U3,U] such that [f] and [g] represent K and S, respectively. For this purpose, take f =

pr21ÎC[U2,U] and g = u°<u°<pr31,pr33>,u°<pr32,pr33>>ÎC[U3,U]. ¨

Theorem 9.2.5 provides sufficient conditions in order to construct ’functionally complete“ objects.

Theorem 9.5.6 will show that these conditions are also necessary.

210

9. Reflexive Objects and the Type-Free Lambda Calculus

A further insight, though, into functional completeness may be given in CCC's. The advantage of

dealing with CCC's is that for any object X one may consider its ’function space“ or exponent XX,

as an object. As a matter of fact, functional completeness, in its various forms of increasing strength

(combinatory algebras, l-algebras, l-models (see below)), expresses some sort of privileged relation

between an object in a category and its ’function space“: its representability, say, in the sense

expressed in the proof of theorem 9.2.5. In CCC's K-universal morphisms and principal morphisms

are related as follows:

9.2.6 Proposition Let C be a CCC and L be the isomorphism C[X´Y,Z] @ C[X,Z Y ]. Then

uÎC[X´Y,Z] is K-universal iff L(u)ÎC[X,ZY] is principal.

Proof The isomorphism L implies, by definition, the equivalence of the following diagrams:

and we are done. ¨

The connection between K-universal and principal morphisms should remind the reader that the latter

correspond to (acceptable) Gšdel numberings from w to PR, the partial recursive functions, when

these are viewed as objects in the category EN of numbered sets (see section 2.2). Note though that

Kleene•s (w, .) is a partial combinatory algebra and does not yield a model of Combinatory Logic.

Total combinatory algebras turn out to be nontrivial constructions and may be obtained, for instance,

in higher types, as it will be shown later. The categorical description, in terms of K-universal maps or

principal morphisms, sheds some light on the connections between Gšdel numberings and

combinatory completeness. As a matter of fact, by proposition 9.2.6 one may then restate theorem

9.2.5 in terms of CCC's and principal morphisms.

9.2.7 Proposition Let C be a CCC. Assume that, for some U in C, T < U, U´U < U and

there exists a principal pÎC[U,UU]. Then A(L-1(p)) is a combinatory algebra.

The previous proposition suggests more explicitly the connection between the definition of

application and the morphism eval in CCC's. Just observe that, by definition of ’.“, one has in a

CCC

a.b = L-1(p)°<a,b> = eval°(p´id)°<a,b> = eval°((p°a)´b).

211

9. Reflexive Objects and the Type-Free Lambda Calculus

Informally, the equation above means ’transform a into a morphism, by p, then apply it to b.“

This process generalizes the way Gšdel numberings associate functions to numbers. Similarly as

for the partial recursive functions, there is in general no ’canonical“ way to go backwards, that is to

choose uniformely and effectively a representative for each representable function. That is, this

representative does not need to be unique and it is not possible to choose a representative for each

representable function in a ’uniform“ way, i.e., by a morphism in the category. This is, though,

possible in l-models. We define them here in a first order manner, as particular combinatory

algebras, with a suitable ’choice“ operator.

9.2.8 Definition Let A = (X, .) be an applicative structure. Then

i. A is a l -model if for some k,s,eÎX one has:

k. "x,y kxy = x ;

s. "x,y,z sxyz = xz(yz) ;

e1. "x,y exy = xy ;

e2. "x,y ("z xz = yz) Þ ex = ey ;

e3. ee = e .

ii. A is an extensional l-model if one also has "x ex = x .

e has to be understood as a choice operator that picks up a canonical representative for each

representable function. e coincides with the canonical representative of the function it represents, by

axiom (e3). In extensional l-models, there is just one representative and (’e1), (’e3) are derived.

Note that A = (X, .) is an extensional l-model iff A is a combinatory algebra and "x,y ("z xz =

yz) Þ x = y .

There exists an obvious formal system of combinators K, S, e associated to the previous notion

of l-model, which we shall call CLe (we gave priority to the notion of model because we mainly

e

focus here on semantical aspects). The interpretation of CLe in l-models is straighforward. Note

also that CLe may be easily and soundly translated into l-calculus, by taking e to lxy.xy.

Conversely, the combinator e can be used to ’clean“ the translation of a lambda term by means of

combinators described in definition 9.1.4 :

9.2.9 Definition Given a l-term M, the associated term MCLe in CLe is inductively defined by

e

xCLe = x

(MN)CLe = MCLeNCLe

(lx.M)CLe = e .<x>MCLe.

This ’refinement“ is completely worthless from an implementative point of view, since the reduction

process is essentially unaffected by the combinator e, as it is stated by equation (e1). On the contrary,

212

9. Reflexive Objects and the Type-Free Lambda Calculus

it is relevant in semantics, since it allows a simple definition of a sound interpretation of l-terms in

l-models, as follows:

9.2.10 Definition Let A = (X, .,k,s,e) be a l-model. The interpretation [M]x of a l-term M

]

in A with respect to an environment x is the semantics of the associated combinatorial term MCLe,

i.e.,

[M]x = [MCLe ]x.

]

We omit the soundness proof, which is technically straightforward and almoust evident from the

previous discussions.

In the next two results we show how to derive l-models from reflexive objects in categories with

enough points.

9.2.11 Theorem Let C be a CCC with enough points. Assume that, for some U in C, one

has UU < U via (y, f). Then, for e = y°L(y°f°snd) , A = (A(L-1(f)),e) is a l-model.

Proof fÎC[U,U U] is principal; moreover by 2.3.6, T < U and U´U < U. Thus, for a.b =

eval ° <(f ° a),b> = eval° (f´id) ° <a,b>) and some suitable K and S, (A(L -1 (f)),.,K,S) is a

combinatory algebra, i.e. (k) and (s) in 9.2.8 hold. Define now e = y°L(y°f°snd) : T®U (that is,

informally, e = y(y°f) ). Note first that, for any a,

e.a= y°f°a

()

indeed:

e.a = (y°L(y°f°snd)).a by def. of e

by def. of ’.“

= eval°<(f°y°L(y°f°snd)),a>

= eval°<(L(y°f°snd)),a> since f°y = id

= eval°(L(y°f°snd)´id)°<id´a>

= y°f°snd°<id´a>

= y°f°a

Then one has:

e.a.b = (y°f°a).b by ( )

e1.

by def. of ’.“

= eval°<(f°y°f°a),b>

= eval°<(f°a),b> since f°y = id

= a. b by def. of ’.“

e2. Suppose that "z az = bz. Then, since

a.z = eval°<(f°a),z> = eval°((f°a)´id)°<id,z>,

b.z = eval°<(f°b),z> = eval°((f°b)´id)°<id,z>,

and since C has enough points, we have eval°((f°a)´id) = eval°((f°b)´id), and thus f°a = f°b.

Then e.a = y°f°a = y°f°b = e.b.

213

9. Reflexive Objects and the Type-Free Lambda Calculus

e.e = y°f°y°L(y°f°snd) =y°L(y°f°snd) = e. ¨

e3.

The definition of e should be clear. Just note that y°f : U®UU®U, i.e., f gives a morphism for

each point a in U and y chooses a ’canonical“ one, representing f(a), as f°y = id. Then e =

y°L(y°f°snd): T®U , internalizes y°f as a point in U.

9.2.12 Corollary Let C be a CCC with enough points.

i. If, for some U in C, UU < U via (i,j) and there exists uÎC[U´U,U] K-universal, then also

A(u) can be turned into a l-model.

ii. If UU @ U via (y,f), then A(u) is an extensional l-model.

Proof

i. By theorems 9.2.6 and 9.2.11 and the definiton of principal morphism.

ii. e.a =y°f°a = a. ¨

9.3 Categorical Semantics of the l -Calculus

In theorem 9.2.11 we proved that if C is a CCC with enough points, and UÎObC is a reflexive

object (i.e., UU<U via (y, f) ) then, for e=y°L(y°f°snd) : T®U, (A(L-1(f)),e) is a l-model.

We can thus give an interpretation of the lambda calculus as in definition 9.2.10.

In this section we define a more direct interpretation of the lambda calculus over such an object

U, and relate the two interpretations.

9.3.1 Definition Let C be a CCC with terminal object T. Let UÎObC be a reflexive object via

the retraction pair (y: UU®U, f: U®UU) . Let M be a l-term with FV(M) Í D = {x1,É,xn}.

Define then [M]D ÎC[U n ,U], where Un = (...(T´U)´...)´U with n copies of U, as follows

(we use the two projections fst and snd in a polymorphic fashion, and we omit the indexes):

[xi]D = snd ° fstn-i = prni

[MN]D = eval ° < f ° [M]D, [N]D>

[lx.M]D = y ° L([M]DÈ{x} ).

We do not prove the soundness of the interpretation; the reader interested in this result may consult

the references.

Examples

1. Let M = lx.xx.

[lx.xx] = y ° L([xx]{x})

214

9. Reflexive Objects and the Type-Free Lambda Calculus

= y ° L( eval ° < f ° [x]{x}, [x]{x}> )

= y ° L( eval ° < f ° snd, snd > ) : T®U .

2. Consider the term Y = lx.(ly.x(yy)(ly.x(yy)). This is a fixpoint operator, since for every M,

YM = (lx.(ly.x(yy)(ly.x(yy)))M

= (ly.M(yy)(ly.M(yy))

= M( (ly.M(yy))(ly.M(yy)) )

= M(YM)

Let us interpret Y. We proceed by stages

[ ly.x(yy) ]{x} = y ° L([x(yy)]{x,y} )

= y ° L( eval ° < f ° [x]{x,y}, [yy]{x,y}> )

= y ° L( eval ° < f ° snd ° fst, eval ° < f ° [y]{x,y}, [y]{x,y} > >

= y ° L( eval ° < f ° snd ° fst, eval ° < f ° snd, snd > >

Let P = y ° L( eval ° < f ° snd ° fst, eval ° < f ° snd, snd > > .

Then we have

[Y] = [ lx.(ly.x(yy)(ly.x(yy)) ]

= y ° L( [(ly.x(yy)(ly.x(yy)) )]{x})

= y ° L( eval ° < f ° P ° snd, P ° snd > ): T®U

It is not difficult to prove that L -1(f ° [Y] ) ° <!UU, y> = eval ° < f ° P ° y, P ° y > : UU®U is

a categorical fixpoint operator (see definition 8.8.2).

We now relate the two notions of categorical semantics given in 9.2.10 and 9.3.1. As a matter of fact

they are essentially equivalent, the only difference being that the one in definition 9.3.1 does not need

the concept of environment.

9.3.2 Definition Let x: Var® A(L -1(f)) be an environment . Let D = {x1,É,xn} be a finite

set of variables. Then

x'D = <...<idT, x(x1)>É ,x(xn)> : T ® T´U...´U

We shall usually omit the subscript D in x'D when it will be clear from the context.

9.3.3 Theorem Let C be a CCC with enough points, UU < U via (y, f) ), and A be the

associated l-model as in proposition 9.2.11. Let [ ] and [ ] be the interpretations respectively

defined in 9.2.10 and 9.3.1. Then, for any term M with free variables in D = {x1,É,xn} and any

environment x: Var® A(L-1(f)) , one has

[M]D ° x'D = [ M] x .

]

Proof The proof is by induction on the structure of M.

- case M = x. Suppose x(x) = a : T®U. Then x'D = < idT, a >. We have:

[x ] { x } ° x ' D = snd ° < idT, a >

215

9. Reflexive Objects and the Type-Free Lambda Calculus

=a

= x(x)

= [ x] x

]

- case M = PQ

[PQ]D ° x'D = eval ° < f ° [P]D , [Q]D > ° x'D

= eval ° < f ° [P]D ° x'D , [Q]D ° x'D >

= eval ° < f ° [P]x , [Q]x > by induction hypothesis

] ]

= [ P] x [ Q] x

] ] by def. of application

= [ PQ]x]

- case M = lxn+1.N

Note first that, for any a : T®U,

[<xn+1>NCLe]x . a = [N]DÈ{x n+1 }° < x'D , a >.

(*)

Indeed:

[<xn+1>NCLe]x . a = [NCLe]x(xn+1=a) by lemma 14.1.3

= [N]x(xn+1 =a)

] by definition of [ ]

= [N]DÈ{xn+1}° < x'D , a > by induction hypothesis.

Note now that:

[<xn+1>NCLe]x . a = eval ° < f ° [<xn+1>NCLe]x, a >

= eval ° ( (f ° [<xn+1>NCLe]x)´id) ° < idT, a >,

and

[N] DÈ{x n+1 } ° < x'D , a > = [N]DÈ{xn+1}° x'D´id ° < idT, a >.

Since C has enough points, and all the points in T´U are of the kind < idT, a >, from (*) we have:

[N]DÈ{xn+1}° x'D´id = eval ° ( (f ° [<xn+1>NCLe]x)´id).

Applyng L to both the members, and composing with y, we get:

y ° L([N]DÈ{xn+1}° x'D = y ° f ° [<xn+1>NCLe]x.

By definition, y ° L([N]DÈ{xn+1}° x'D = [lx.N]D° x'D

Moreover,

[ lx.N] x = [(lxn+1.N)CLe]x

]

= [e . <xn+1>NCLe]x

= e . [<xn+1>NCLe]x

= y ° f ° [<xn+1>NCLe]x.

This conludes the proof. ¨

216

9. Reflexive Objects and the Type-Free Lambda Calculus

9.4 The Categorical Abstract Machine

The categorical interpretation in definition 9.3.1 suggests a very simple and nevertheless efficient

implementation of the lambda calculus. The implementation is based on a call-by-value, leftmost

strategy of evaluation, and it is performed by an abstract environment machine called CAM (see

refernces). The first step toward the implementation is the compilation of lambda calculus in a

language of categorical combinators.

Note that [MN]D = eval ° < f ° [M]D, [N]D> = L-1(f) ° < [M]D, [N]D>. L-1(f): U´U®U is

just the application u of the underlyng combinatory algebra. We shall write app instead L-1(f).

Moreover, let cur(f) = y ° L(f), and write f ; g instead of g ° f. Then the equations which define

the semantic interpretation of the lambda calculus are rewritten as follows:

[xi]D = fst; . . . ; fst; snd where fst appears n-i times

[MN]D = < [M]D, [N]D> ; app

[lx.M]D = cur([M]DÈ{x} ).

This provides a ’compilation“ of the l-calculus in a language where all the variables have been

replaced with ’access paths“ to the information they refer to (note the use of the ’dummy“ enviroment

D during the compilation).

One of the main characteristic of the categorical semantical approach is that we can essentially use

the same language for representing both the code and the environment. An evaluation of the code C

in an environment x is then the process of reduction of the term x ; C. The reduction is defined by a

set of rewriting rules. The general idea is that the environment should correspond to a categorical term

in some normal form (typically, a weak head normal form). The reductions preserve this property of

the environment, executing one instruction (i.e. one categorical combinator) of the code, and updating

at the same time the program pointer to the following instruction.

For fst and snd we have the following rules, whose meaning is clear:

<a,b> ; (fst ; C1) • Þ a ; C1

<a,b> ; (snd ; C1) Þ b ; C1

In the left hand side of the previous rules, <a,b> is the environment and the rest is the code. We

shall use parenthesis in such a way that the main semicolon in the expression will distinguish between

the environment at its left, and the code at its right.

For cur(C1) we use the associative law of composition and delay the evaluation to another time:

x ; (cur(C1); C2) Þ (x ; cur(C1) ) ; C2

The structure (x ; cur(C1) ) corresponds to what is usually called a closure.

The right time for evaluating a term of the kind cur(C) is when it is applied to an actual parameter a.

We then have:

<(x ; cur(C1)), a > ; (app; C2) Þ <x, a> ; (C1; C2)

The previous rule is just a rewriting of the equation

L-1(f) ° <y ° L(C1) ° x, a > = eval ° <L(C1) ° x, a > = C1 ° <x, a>

217

9. Reflexive Objects and the Type-Free Lambda Calculus

that proves the semantical soundness of the previous rule.

Finally, we must consider the evaluation of a term of the kind <C1,C2>; C3. We have the formal

equation:

x ; (<C1,C2>; C3) = < x ; C1, x ; C2> ; C3

but we cannot simply use it for defining a reduction, since we want also to reduce x ; C1 and x ;

C2. We must first carry out independently the reductions of x ; C1 and x ; C2 , and then put them

together again building the new environment.

A simple solution on a sequential machine may be given by using a stack and working as follows:

first save the actual environment x by a push operation, then evaluate x ; C1 (that yields a new

environment x1); next swap the environment x1 with the head of the stack (i.e. with x); now we

can evaluate x ; C2 obtaining x2; finally build a pair <x1,x2> with the head of the stack x1 and

the actual environment x2 (that is a cons operation). An interesting and elegant property is that, if

we just write at compile time <C1,C2> as ’push; C1; swap; C2; cons“, then the above behaviour is

obtained by a sequential execution of this code.

9.4.1 Definition The compilation by means of categorical combinators of a l-term M in a

’dummy“ environment D = (...(nil, x1),É), xn ) is inductively defined as follows:

[x](D,x) = snd

[y](D,x) = fst; [y]D

[MN]D = push; [M]D; swap; [N]D; cons; app

[lx.M]D = cur([M](D,x)) .

Examples

1. The closed term M = lx.xx has the following compilation:

[lx.xx]nil = cur([xx](nil,x) )

= cur(push; [x](nil,x); swap; [x](nil,x); cons; app)

= cur(push; snd; swap; snd; cons; app).

2. The term (lx.x)(lx.x) is so compiled:

[(lx.x)(lx.x)]nil = push; [lx.x]nil; swap; [lx.x]nil; cons; app

= push; cur([x](nil,x) ); swap; cur([x](nil,x) ); cons; app

= push; cur(snd); swap; cur(snd); cons; app.

9.4.2 Definition The reduction of the compiled code is summarized by the following table:

218

9. Reflexive Objects and the Type-Free Lambda Calculus

BEFORE AFTER

Environment Code Stack Environment Code Stack

<a,b> fst; C S C S

a

<a,b> snd; C S C S

b

cur(C1); C2 S x; cur(C1) C2 S

x

<x;cur(C1),a> app; C2 S <x,a> C1;C2 S

push; C S C

x x x.S

swap; C x 2 .S C x 1 .S

x1 x2

cons; C x 2 .S <x2, x1> C S.

x1

Example The code ’push; cur(snd); swap; cur(snd); cons; app“ corresponding to the l-term

(lx.x)(lx.x) gives rise to the following computation:

ENV. = nil

CODE = push; cur(snd); swap; cur(snd); cons; app

STACK = nil

ENV. = nil

CODE = cur(snd); swap; cur(snd); cons; app

STACK = nil . nil

ENV. = nil; cur(snd)

CODE = swap; cur(snd); cons; app

STACK = nil . nil

ENV. = nil

CODE = cur(snd); cons; app

STACK = nil; cur(snd) . nil

ENV. = nil; cur(snd)

CODE = cons; app

STACK = nil; cur(snd) . nil

ENV. = <nil; cur(snd), nil; cur(snd) >

CODE = app

STACK = nil

219

9. Reflexive Objects and the Type-Free Lambda Calculus

ENV. = <nil, nil; cur(snd) >

CODE = snd

STACK = nil

ENV. = nil; cur(snd)

CODE =

STACK = nil

Note that ’cur(snd)“ is the compilation of lx.x.

9.5 From Applicative Structures to Categories

We want now to ’go backwards“, with respect to section 9.2, where we described how to find

models of a type-free language within type structures, i.e., within CCC. Namely, we will see how to

construct typed models, in particular a CCC, out of type-free structures. This has an important

motivation from Programming Language Theory, since it is the semantic counterpart of the following

relevant methodology in functional languages.

We already mentioned, as an example, that one of the main features of Edinburgh ML is its

automatic treatment of type assignment. That is, the programmer may write programs without taking

care of the tedious details of assigning types. The type checker decides whether the given program is