The business of this section is to establish the connection between the symbolism of the lcalculus (labstraction, free variables, breduction and so on) and its semantics, involving sets, Scott domains and cartesian closed categories. On the face of it, these are very different beasts. Usually, some kind of translation is defined, which takes one system to the other. Such an approach tends to exaggerate the separation in order to make a greater triumph of the reconciliation.
In this chapter, we already have a technique which brings both parties together on the same categorical platform. Then the ways in which they each express the same essential features can be compared directly.
The syntactic category was constructed in Section 4.3. Its objects are lists of \bnfname typed variables and its morphisms are lists of \bnfname terms, where we left the notions of \bnfname type and \bnfname term undefined. In Section 4.6, these meant sorts (base types) and algebraic expressions respectively. Now we shall allow the types to be expressions built up from some given sorts using the binary connective ® , and the terms to be lexpressions.
We already have the notion of composition: it is given by substitution, as before, and is not something new involving labstraction, which we do not yet understand. The Normal Form Theorem 4.3.9 for substitutions still holds  not to be confused with that for the lcalculus, Fact 2.3.3. The category has specified products, given by concatenation.
As the raw syntax is now a category, we can already ask about any universal properties it might have. We begin by defining the \bnfname terms to be adequivalence classes, ie taking account of any algebraic laws between operationsymbols in the language, but not the bhrules. These take the form of equations between morphisms of the category, and we shall argue from them towards cartesian closure. The technique is a generic one, and will be applied to binary sums, dependent sums and dependent products in Sections 5.3ff, 9.3 and 9.4 respectively.
It is easy to be fooled by syntactic treatments into thinking that for a type to be called [X® Y] is necessary and sufficient for it to behave as a functiontype. Our development (here and in Chapter IX) is based on how this type is used (application, abstraction and the bhrules): any typeexpression or semantic object is a priori eligible for the role .
REMARK 4.7.1 Application is a binary operationsymbol: every instance of it is obtained uniquely by substitution for f and x into

The raw calculus Abstraction, which is what the functiontype is about, is much more interesting. In Sections 1.5 and 2.3 sequent rules were needed: l is not an operation on terms but a meta operation on terms incontext. It defines a bijection,

Categorically, the effect of an operationsymbol is by postcomposition, affecting only the target of a morphism; invariance under substitution is automatic as that works by precomposition, at the source. Abstraction, however, affects the source as well as the target, so it must be defined as a metaoperation on homsets, cf the indirect transformations of trees on page 1.1.2. An extra condition must be added to handle substitution; this requires a new concept, naturality, which we shall study in the next section (Example 4.8.2(h)).
So first we shall concentrate on the meaning of the new operation l in the raw calculus, and in particular on its invariance under substitution, adding the b and hrules later. With or without these rules, substitution remains the notion of composition, and we shall refer to the categories composed of lterms and of raw lterms respectively.
DEFINITION 4.7.2 Let C be a category with a specified terminal object and for which each pair of objects has a specified product together with its projections. Then a raw cartesian closed structure assigns to each pair of objects X and Y

In defining products we didn't reserve any special treatment for base (atomic) types  nor do we here. In the semantic case they are not special anyway, but in the syntactic category an object is a list of types. We use Currying (Convention 2.3.2) to exponentiate by a list.
EXAMPLES 4.7.3 The following have raw cartesian closed structures:
Interpretation The raw lcalculus extends the language of algebra by some new types [X® Y] and operationsymbols \ev_{X,Y}. As yet these have no special significance, and they can be handled as if they were algebra: hence the notation Cn^{×}_{L+l} (in contrast to Cn^{® }_{L} below).
REMARK 4.7.4 Let C be a category together with a raw cartesian closed structure, in which the base types, constants and operationsymbols of L have an assigned meaning. Then the language L+l has a unique interpretation, and this defines a functor [[]]:\Clone_{L+l}^{x}® C.
PROOF: Building on Remark 4.6.5, by structural recursion,
By Theorem 4.6.7 this is a productpreserving functor, and by the present construction it also preserves the new structure. []
The b and hrules We have constructed Cn^{×}_{L+l} from the syntax, so it has names for its objects and morphisms. But it is also a category, so we may compare these two modes of expression, from which we shall derive a universal property.
LEMMA 4.7.5 The interpretation satisfies the rules iff

PROOF: These are the interpretations of

DEFINITION 4.7.6 A cartesian closed structure on a category is a raw cartesian closed structure which satisfies the b and hrules.
EXAMPLES 4.7.7 The following are cartesian closed structures:
REMARK 4.7.8 Currying or labstraction gives an alternative way of handling (manyargument) operationsymbols as constants, in the same way that Hilbert's implicational logic (Remark 1.6.10) eliminated all of the rules apart from (Þ E ) in favour of axioms.
omitted diagram environment
Let \typeX_{1},¼,\typeX_{k}\vdash r:Y be an operationsymbol (of type Y and arity k). Then \expx r º l[(x)\vec]:[(X)\vec].r([(x)\vec]):[[(X)\vec]® Y] is a constant (of exponential type), from which the original operation is recovered by the brule.
In the unary case, r(a) is an operation applied to a value. In a cartesian closed category this equals ev(\expx r,a) = \expx ra in the sense of lapplication. The former uses composition by substitution (which we treat as the standard notion), whilst the l calculus provides gof = lx.g(fx). These coincide iff the b and hrules hold.
DEFINITION 4.7.9 An object F, with a morphism ev:Fx X® Y, is an exponential or functionspace if for every object G Î obC and morphism p:Gx X® Y there is a unique morphism f:G® F such that p = evo(fx\id_{X}). The exponential F is written [X® Y] or Y^{X}.
The notation \expx p for the exponential transposition is commonly found in category theory texts, but it is clearly inadequate to name all of the morphisms of a cartesian closed category. So they frequently go without a name. All too often, proofs are left to rely on verbal transformations of unlabelled diagrams, without regard to the categorical precept that morphisms are at least as important as objects. The lcalculus gives the general notation we need.
PROPOSITION 4.7.10 A cartesian closed structure on a category is given exactly by the choice of a product and a functionspace for each pair of objects, together with the projections and evaluation.
PROOF: Suppose we have the structure of Definition 4.7.2 and Lemma 4.7.5. The two definitions of functionspace share the same data and also the b rule, so that l_{G,X,Y}(p) serves for \expx p.
omitted diagram environment
If l_{G,X,Y} satisfies h and the naturality law, whilst \expx p obeys b, then
omitted eqnarray* environment
so \expx p is unique, ie the universal property holds. Conversely, naturality and the brule follow from the universal property by uniqueness (as in Proposition 4.5.13). The hrule holds as id serves for l(ev), and the naturality law holds because its right hand side serves for the left. []
Example 7.2.7 gives an alternative proof.
COROLLARY 4.7.11 The exponential object [X® Y] is unique up to unique isomorphism. It defines a functor which is contravariant in the first or raised argument and covariant in the other.
PROOF: Loosely speaking, [u® z](f) = u;f;z. []
THEOREM 4.7.12 The category \Clone_{L}^{® } has a cartesian closed structure and a model of the lcalculus with base types and constants from L. Any other such interpretation in a category C is given by a unique functor [[]]:\Clone_{L}^{® }® C that preserves the cartesian closed structure and the model. Conversely, any such functor is an interpretation.
PROOF: As in Theorem 4.4.5 and Remark 4.6.5. Remark 4.7.4 extends the interpretation to the lcalculus; in particular the functiontypes have to be preserved. By Proposition 4.7.10, these must be exponentials. []
Cartesian closed categories of domains The category of sets and total functions is the fundamental interpretation of the typed lcalculus, but it does not have the fixed point property (Proposition 3.3.11) needed for denotational semantics. During the 1970s and 1980s a veritable cottageindustry arose, manufacturing all kinds of domains with Scottcontinuous maps, each with its own peculiar proof of cartesian closure. In fact these categories ( necessarily) share the same functionspace as in Dcpo: what is needed in each case is not a repetition of general theory, but the verification that the special semantic property is inherited by the function space.
THEOREM 4.7.13 Pos has a cartesian closed structure.
PROOF: The universal property tells us what the exponential [X® Y] must be. Taking G = {*} , it is the set of monotone functions, whilst for ev to be monotone we must have f £ gÞ "x.f(x) £ g(x). Now consider G = {^ < T}, cf Example 4.5.5(b). If f £ g pointwise then there is a monotone function Gx X® Y by ^,x® f(x) and T,x® g(x). The exponential transpose is ^® f and T® g, so f £ g as elements of the functionspace.
For this to give a cartesian closed structure we must verify that
The first three parts were proved in Propositions 3.5.1 and 3.5.5, but it is the notion of cartesian closed category which makes sense of the collection of facts in Section 3.5. The laws in part (d) are inherited from the underlying sets and functions. []
The result for Scottcontinuous functions (redefining [X® Y]) is proved in the same way.
THEOREM 4.7.14 Dcpo has a cartesian closed structure.
PROOF: For similar reasons, [X® Y] must be the set of Scott continuous functions with the pointwise order. Propositions 3.5.2 and 3.5.10 gave the details, based on a discussion of pointwise joins, and in particular Corollary 3.5.13 about joint continuity of ev. []
Algebraic lattices, boundedly complete posets, Ldomains and numerous other structures form cartesian closed categories with Scottcontinuous functions as their morphisms. The issue of making ev preserve structure jointly in its two arguments may be resolved in a different way, as Exercise 4.51 shows.
At the end of the next section we shall show that categories themselves may be considered as domains and form a cartesian closed category. First we need to introduce the things which will be the morphisms of the exponential category; this turns out to be the abstract notion which we needed for substitution invariance of l. Section 7.6 returns to the relationship between syntax and semantics, bringing the term model into the picture. Functionspaces for dependent types are the subject of Section 9.4.