Section 4.2 began the semantics of formal languages with the unary case, for which plain categories were needed. The constructors of more complex languages will be interpreted using appropriate structure in categories, in particular products for multiary operations in this section and function-spaces for l-abstraction in the next. In general, appropriate structure is defined by universal properties, interpretation by a structure-preserving functor from the category of contexts to the semantics.
|
DEFINITION 4.6.1 A (finitary many-sorted) algebraic theory L has
DEFINITION 4.6.2 An L- algebra A in a category C with products is
such that the polygons (such as those in Example 4.6.3(f)) which express the laws commute.
A homomorphism A® B of L-algebras is an assignment to each sort X of a C-morphism fX:\typeAX® \typeBX between the corresponding objects which preserves each operation r in the sense that the squares of the following form commute.
omitted diagram environment
Note that we have already used the product functor (Proposition 4.5.13) in this definition, so we would now be stuck if we hadn't insisted on uniqueness of the mediator in the definition of product.
Algebras and homomorphisms in C form a category, called \ModC(L); the subscript is omitted if C = Set is understood.
For each sort there is a forgetful functor \ModC(L)® C, but it is usually not faithful: if it were, this one sort would suffice. There is a faithful functor to CS reflecting invertibility, where S is the set of sorts.
Examples It is clearer to fix the meaning of these widely applicable definitions by means of familiar examples than by formality. But note that, at present, we intend each of the sorts, operation-symbols and laws to be named concretely. Typical examples of theories in mathematics have one or two sorts, half a dozen operation-symbols (of arity zero, one, two, or occasionally three) and a dozen laws.
In Chapter VI we shall develop internal theories, whose linguistic classes may themselves be objects of the model, and there may be arbitrarily many sorts and operation-symbols. The arities will be allowed to be ``infinite,'' ie again objects of the model, but there will be no laws. As we shall see in Section 5.6, this is because, for laws to behave as intended, each operation must have a finitely enumerated family of arguments. Nevertheless, when there are laws, there may be as many as we please.
|
|
EXAMPLES 4.6.4 The following are not algebraic theories, as there are exceptional values at which the operations are not defined, but it is often profitable to apply algebraic ideas to them.
These theories involve conditional properties (``either ... or ...''), which we shall discuss briefly in Examples 5.5.9.
Semantics of expressions Now we shall extend Theorem 4.4.5 to algebraic theories. We have already seen several notations for the effect of a functor, and now we shall introduce yet another: Dana Scott's semantic brackets. These are convenient because the construction is applied to lengthy expressions; the brackets also draw attention to the difference between syntax and semantics. When more than one model A is under discussion, we write A[[X]], A[[G]] , A[[r]], A[[u]], etc .
REMARK 4.6.5 An algebra A in a category C gives the meaning of each sort X as an object \typeAX. This extends canonically to the contexts by
omitted eqnarray* environment
using the left-associated product (Remark 4.5.15) . A also gives the meaning of each operation-symbol \typeY1,¼,\typeYk\vdash r:Z and each constant c:Z as a morphism \oprA:\typeA\typeY1x···x\typeA\typeYk® \typeAZ or \opcA:\terminalobjC® \typeAZ. These extend uniquely to the \bnfname terms in the context G º [x1:\typeX1,¼,xn:\typeXn] by structural recursion, as follows, =2pt
omitted eqnarray* environment
where [[\argui]]:[[G]] ® \typeA\typeYi are the interpretations of the sub-expressions.
To illustrate this, consider the first line of Example 4.3.4,
|
omitted diagram environment
In general, the \bnfname programs are interpreted as follows:
omitted eqnarray* environment
To show that this is well defined we must show that the laws of the sketch (Remark 4.3.8) and of the theory L are respected. Those involving discard are easy. The Substitution Lemma itself holds because we used Remark 4.3.10(a) to give the interpretation of terms. Terms a and b which are shown to be equal by a single application of a law a¢ = b¢ in L correspond to programs
|
EXAMPLE 4.6.6 YACC generates a parser in C from a context-free grammar (Example 4.6.3(d)). The rule
/expr: expr '+' expr = addition (1, 2); /
states the syntax of the token /+/ in the program text, and defines its semantics to be the C subroutine /addition/.
Notice that the variables disappear in passing from syntax to semantics, so when we go the other way we must make an arbitrary choice of them ( cf Remark 4.3.14).
The classifying category The notions of functor and product exactly capture algebraic theories and their models. The single-sorted version is due to Bill Lawvere (1963, Exercise 4.29).
THEOREM 4.6.7 Let L be an algebraic theory. Then
PROOF: Recall that the objects of \CloneLx are contexts and the morphisms are programs or substitutions.
Theorem 3.9.1 found the classifying semilattice Cn\land\triangleright for a Horn theory, using induction on closure conditions to show that [[-]] is monotone, and Exercise 3.36 gave the saturated form of any closure condition. Now \CloneLx is the saturation as an algebraic theory, with all possible derived operations of every finite arity, modulo all provable equalities between them ( cf regarding expressions as operation-symbols in Remark 1.1.2). Hence the term clone, which was introduced by Philip Hall in 1963.
Example 4.8.2(e) extends the Theorem to homomorphisms.
The model is generic in the category Cn×L in the same way that the value x0 was generic in a proof box in Remark 1.5.6: inside this world it may be treated as an ordinary object, and there are special rules for importing and exporting it. Indeed, just as in Remark 1.5.10, given any such object in the outside world, there is a b-reduction of the generic object which reproduces it, namely the functor [[-]].
Hence algebra is complete (Remark 1.6.13, Corollary 3.9.2).
COROLLARY 4.6.8 Let f be a formula involving equations between terms of L, conjunction and universal quantification, and let G be some possibly infinite set of such formulae. We write G\satisfiesLf if every L-algebra satisfying all of the formulae in G also satisfies f. Then G\satisfiesLf iff G\provesLf.
PROOF: Without loss of generality f is a single equation and we may strip conjunctions and universal quantification from G. Let L¢ be the theory L together with the equations in G as additional laws. Then an ``L-algebra satisfying all of the formulae in G'' is just an L¢-algebra. If G\satisfiesLf then in particular Cn×L¢ satisfies f, but this model satisfies exactly those equations that are provable from L¢, so G\provesLf. The other direction is soundness. []
We shall give a generalisation of the universal property of products in Section 5.1. In the corresponding wider notion of algebraic theory, which includes categories themselves as an example, operations may be defined or laws imposed only when certain conditions hold. Remark 5.2.9 and Chapter VIII set out two ways of formulating such theories.