The business of this section is to establish the connection between the symbolism of the l-calculus (l-abstraction, free variables, b-reduction 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 l-expressions.
We already have the notion of composition: it is given by substitution, as before, and is not something new involving l-abstraction, 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 l-calculus, 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 ad-equivalence classes, ie taking account of any algebraic laws between operation-symbols in the language, but not the bh-rules. 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 function-type. Our development (here and in Chapter IX) is based on how this type is used (application, abstraction and the bh-rules): any type-expression or semantic object is a priori eligible for the role .
REMARK 4.7.1 Application is a binary operation-symbol: every instance of it is obtained uniquely by substitution for f and x into
|
The raw calculus Abstraction, which is what the function-type 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 -in-context. It defines a bijection,
|
Categorically, the effect of an operation-symbol 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 meta-operation on hom-sets, 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 h-rules later. With or without these rules, substitution remains the notion of composition, and we shall refer to the categories composed of l-terms and of raw l-terms 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 l-calculus extends the language of algebra by some new types [X® Y] and operation-symbols \evX,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 operation-symbols of L have an assigned meaning. Then the language L+l has a unique interpretation, and this defines a functor [[-]]:\CloneL+lx® C.
PROOF: Building on Remark 4.6.5, by structural recursion,
By Theorem 4.6.7 this is a product-preserving functor, and by the present construction it also preserves the new structure. []
The b- and h-rules 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 h-rules.
EXAMPLES 4.7.7 The following are cartesian closed structures:
REMARK 4.7.8 Currying or l-abstraction gives an alternative way of handling (many-argument) operation-symbols 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 \typeX1,¼,\typeXk\vdash r:Y be an operation-symbol (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 b-rule.
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 l-application. 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 h-rules hold.
DEFINITION 4.7.9 An object F, with a morphism ev:Fx X® Y, is an exponential or function-space 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\idX). The exponential F is written [X® Y] or YX.
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 l-calculus 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 function-space 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 function-space share the same data and also the b- rule, so that lG,X,Y(p) serves for \expx p.
omitted diagram environment
If lG,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 b-rule follow from the universal property by uniqueness (as in Proposition 4.5.13). The h-rule 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 \CloneL® has a cartesian closed structure and a model of the l-calculus with base types and constants from L. Any other such interpretation in a category C is given by a unique functor [[-]]:\CloneL® ® 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 l-calculus; in particular the function-types 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 l-calculus, but it does not have the fixed point property (Proposition 3.3.11) needed for denotational semantics. During the 1970s and 1980s a veritable cottage-industry arose, manufacturing all kinds of domains with Scott-continuous maps, each with its own peculiar proof of cartesian closure. In fact these categories ( necessarily) share the same function-space 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 function-space.
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 Scott-continuous 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, L-domains and numerous other structures form cartesian closed categories with Scott-continuous 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. Function-spaces for dependent types are the subject of Section 9.4.