Practical Foundations of Mathematics

Paul Taylor

4.6  Algebraic Theories

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.

formallanguages         interpretation    functor [[-]]     semantics with    universal properties

DEFINITION 4.6.1 A (finitary many-sorted) algebraic theory L has

(a)
base types or sorts, X (there is as yet no need for a product type constructor, as many-variable contexts can handle products for us); we write S for the set of sorts;

(b)
an inexhaustible collection of variables xi:X of each sort;

(c)
operation-symbols, \typeX1,,\typeXk \vdash r:Y, each of which has an arity, ie a list of input sorts \typeXi, and an output sort Y; and

(d)
laws between terms (it is a free theory if there are none).

DEFINITION 4.6.2 An L- algebra A in a category C with products is

(a)
an object \typeAX of C for each sort X, together with

(b)
a multiplication table for each operation-symbol r, ie a map \oprA:\typeA\typeX1x···x\typeA \typeXk \typeAY in C from an appropriate product,

such that the polygons (such as those in Example  4.6.3(f)) which express the laws commute.

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.3

(a)
An internal algebra in Set is an algebra in the ordinary sense.

(b)
The propositional form of an algebraic theory is a Horn theory, ie a system of finitary closure conditions \triangleright on the set S of sorts (Sections 1.7, 3.7 and 3.9). A model in W is an assignment of a truth-value to each element of S, ie a subset A S, which is \triangleright -closed. A homomorphism is simply a containment A B .

(c)
Natural numbers (N), lists and trees are described by free theories (Sections 2.7 and 6.1 ). Zero, the empty list and the leaves of trees are nullary operations or constants. Successor and adding an item to a list are unary operations, and the node-types of a tree are operations of various arities. Bourbaki used the word magma for an algebra with one binary operation and no laws, ie the theory whose free algebra consists of binary trees. Remark 2.7.12 gave the continuation rule for lists in terms of homomorphisms.

(d)
The abstract syntax of a context-free language is the same thing as a free theory. In the design of programming languages the sorts are unfortunately called syntactic categories, eg \bnfname program, \bnfname term, \bnfname number . The keywords of the language are the operation-symbols, but these needn't be represented graphically. For example, in omitted eqnarray* environment 0,,9 are constants and +,- are unary operations, but there are an invisible binary operation \bnfname numberx\bnfname digit \bnfname number and two unary ones \bnfname digit\hookrightarrow \bnfname number\hookrightarrow \bnfname integer. The variables for each sort are called meta-variables, since \bnfname variable may itself be one of the sorts. We shall consider the meta-language of type theory (variables, terms, types, contexts, substitutions) in Section 6.2.

(e)
The specification for a program module consists of data-sorts, operations and laws; its implementations are algebras.

(f)
An internal monoid in a category C with finite products is an object M obC together with unit and multiplication maps,
e:1 M    and    m:MxM M
such that the following diagrams commute:
omitted diagram environment omitted diagram environment
The square and triangles marked Å , L and R express the substance of the associative and unit laws; the rest of the diagram specifies that M2 and M3 are products (Example  7.6.3). Similarly an internal group also has an inversion operation and corresponding laws.

(g)
Internal groups in the categories of topological spaces, manifolds and algebraic varieties are topological, Lie and algebraic groups.

(h)
A ring together with a module is an example of a two-sorted algebra.

(i)
The morphisms of a category with a fixed set O of objects form an algebra for a theory with OxO sorts, namely the hom-sets for each source-target pair. There are O constants (identity on each object), O3 binary operations (composition) and O2+O2+O4 (unit and associative) laws. When O = {*} this is just a monoid.

(j)
A particular model of a theory may be specified by generators and relations, ie as the free algebra for the theory augmented by constants and laws. List({a,b,c})/(ab ~ ba), for example, specifies the monoid with three generators, two of which commute (Section 7.4).

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.

(a)
Lists, with head and tail, because of the empty list (Section 2.7).

(b)
Number fields, because of division by zero.

(c)
An abstract projective plane consists of two sets (of ``points'' and ``lines'') and an (``incidence'') relation between them. Through any two distinct points a unique line passes, and any two distinct lines intersect in a unique point (Example  3.8.15(e)).

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,

1
9
a2- 1
3
b,
in the ring (R,+,*) in the category Set. The operation-symbols have been marked in the diagram, along with the product projections that show which variables and sub-expressions are the arguments. Using the universal property of each product, there is a unique way of filling in other maps which define the sub-expressions as (polynomial) functions of a,b,c R3. The last is the whole expression as a map R3 R.

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

u;putx = a;z     and    u; putx = b;z,
but these have the same interpretation because A is an algebra, ie it is given to satisfy [[a]] = [[b]]. []

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

(a)
\CloneLx has a choice of finite products, and a (``generic'') model of L.

(b)
Let C be another category with a choice of finite products and a model of L. Then the functor [[-]]:Cn×L C preserves (the choice of) finite products and the model, and is the unique such functor.

(c)
Any functor Cn×L C which preserves finite products also preserves the L-model.

PROOF: Recall that the objects of \CloneLx are contexts and the morphisms are programs or substitutions.

(a)
[[a]] Products are given by concatenation of contexts (Example  4.5.8(i) and its footnote). The model is as follows:

(b)
[[b]] The interpretation is given by Remark  4.6.5.

(c)
[[c]] The sorts and operation-symbols of the model are given by the effect of the functor, essentially as in part (a). []

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.