<< стр. 7(всего 10)СОДЕРЖАНИЕ >>

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
 << стр. 7(всего 10)СОДЕРЖАНИЕ >>