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 functionspaces for labstraction in the next. In general, appropriate structure is defined by universal properties, interpretation by a structurepreserving functor from the category of contexts to the semantics.

DEFINITION 4.6.1 A (finitary manysorted) 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 Lalgebras is an assignment to each sort X of a Cmorphism f_{X}:\typeA_{X}® \typeB_{X} 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 \Mod_{C}(L); the subscript is omitted if C = Set is understood.
For each sort there is a forgetful functor \Mod_{C}(L)® C, but it is usually not faithful: if it were, this one sort would suffice. There is a faithful functor to C^{S} 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, operationsymbols and laws to be named concretely. Typical examples of theories in mathematics have one or two sorts, half a dozen operationsymbols (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 operationsymbols. 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 \typeA_{X}. This extends canonically to the contexts by
omitted eqnarray* environment
using the leftassociated product (Remark 4.5.15) . A also gives the meaning of each operationsymbol \typeY_{1},¼,\typeY_{k}\vdash r:Z and each constant c:Z as a morphism \opr_{A}:\typeA_{\typeY1}x···x\typeA_{\typeYk}® \typeA_{Z} or \opc_{A}:\terminalobj_{C}® \typeA_{Z}. These extend uniquely to the \bnfname terms in the context G º [x_{1}:\typeX_{1},¼,x_{n}:\typeX_{n}] by structural recursion, as follows, =2pt
omitted eqnarray* environment
where [[\argu_{i}]]:[[G]] ® \typeA_{\typeYi} are the interpretations of the subexpressions.
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 contextfree 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 singlesorted 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 \Clone_{L}^{x} 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 \Clone_{L}^{x} 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 operationsymbols 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 x_{0} 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 breduction 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\satisfies_{L}f if every Lalgebra satisfying all of the formulae in G also satisfies f. Then G\satisfies_{L}f iff G\proves_{L}f.
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 ``Lalgebra satisfying all of the formulae in G'' is just an L¢algebra. If G\satisfies_{L}f then in particular Cn^{×}_{L¢} satisfies f, but this model satisfies exactly those equations that are provable from L¢, so G\proves_{L}f. 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.