A system of closure conditions describes algebra at the propositional level, for example subalgebras and congruences within a fixed domain of discourse. Regarding the closure conditions themselves as introduction rules, Section 3.7 showed that the elimination rule is an induction scheme. Similarly, the type-theoretic elimination rules provide recursion. We had already treated both induction and recursion in our account of natural numbers and lists in Section 2.7, albeit as separate axiomatisations, which we now have to link together.
The algebraic theories for which we are able to study recursion do not have laws. The reason was in Example 3.7.9(f), which showed that a system \triangleright of closure conditions arises from a (well founded) relation \prec iff for each element t there is exactly one set K of preconditions (K\triangleright t). We shall provide free models for infinitary free theories in this section, and also give some applications of them. As for induction on closure conditions, it is a distortion of the theory to restrict the arities to be finite in advance.
We considered algebraic theories in general in Section 4.6, allowing laws and many sorts. But we insisted there that the arities were finite, since Theorem 5.6.9 fails for infinitary operations. The results of this chapter are still needed and useful, as the means whereby the algebras are constructed in Zermelo type theory. We shall develop this technique in Section 7.4, also using it to find colimits of algebras.
Infinitary algebraic theories without laws What do we mean by infinite? In classical mathematics, for any set K, either it can be finitely enumerated, or any attempt to do so is non- terminating and we have N\hookrightarrow K. Cantor and his followers developed transfinite numbers (ordinals, Section 6.7) to extend the counting idea. Constructively, this argument does not apply, and the enumeration may fail for many other reasons. For example the set in Exercise 2.16 with two ``overlapping'' elements is not finite in the strong sense required by Theorem 5.6.9. (We discuss finiteness in Section 6.6.)
Describing the arities and carrier as infinite simply means that we do not restrict them to being concrete enumerations. (Nor need the arities be ordinals or carry any other special structure.) In this setting we can treat internal theories, in which the collection of operation- symbols need no longer be {0,1,+,-,x,¸} or {^,T,Ù,Ú,Þ ,\lnot } but can be a type W in the object-language. For example W may be a topological space or an abstract data type. The arities ar[r] of the operation- symbols may also be internal objects instead of numbers such as 0 and 2.
For our purpose the arities must nevertheless be specified in advance of the models. The theory of complete semilattices - with operations of arbitrarily large arity - is therefore excluded, even though it happens to have free models (Proposition 3.2.7(b)). The apparently similar theory of complete Boolean algebras has no free algebra on N [Joh82, pp. 33-34].
DEFINITION 6.1.1 A free algebraic theory is given by a set W of operation- symbols together with an assignment to each r Î W of a set ar[r], called the arity of r. The disjoint union
k = \coprodr Î War[r] is known as the rank.
The aim is to construct and study the free model, which is also known as an absolutely free algebra. It is no loss of generality to consider only the free model without generators, ie the initial object of the category Mod(W) of algebras and homomorphisms. If we require the algebra generated by a set G, we consider instead the theory W¢ = W+G, where ar[x] = Æ for x Î G ( cf Remark 3.7.6 for closure operations).
As in Definition 4.6.2, a model or algebra of (W,ar) is a set A together with a multiplication table \oprA for each operation-symbol r Î W.
|
Similarly a homomorphism f:A® B is a function making the square on the left commute for each operation-symbol r Î W:
omitted diagram environment
These conditions too may be combined, as the single diagram on the right. Compare the role of the functor T here with that of the product functor in the diagram in Definition 4.6.2. Notice that W º T1, and ar[r] can also be recovered (Exercise 7.37), but we shall often forget that T has a power series expansion, assuming only that it preserves monos, their inverse images and arbitrary intersections. The lattice analogue of the functor T was given in Lemma 3.7.10, based on closure conditions.
This is quite a different notation from that in which algebraic theories were presented in Definition 4.6.1, so before reading any further you should convince yourself that we have merely presented the relevant data in a more concise form. We shall restore the sorts in Proposition 6.2.6, the generators in Section 6.5 and the laws in Section 7.4.
DEFINITION 6.1.2 Even though the arities are general types rather than numbers, it is useful to retain the notation [(a)\vec] for a typical element of Aar[r] and \argaj for the co-ordinate [(a)\vec](j) where j Î ar[r].
We call an algebra ev:TA\hookrightarrow A equationally free if ev is injective, so
|
EXAMPLE 6.1.3 Let W = {x,s} with ar[x] = Æ and ar[s] = {*} . Any W-algebra satisfies the first two of the Peano axioms for the natural numbers (Definition 2.7.1). The third and fourth axioms make it equationally free ( cf Exercise 2.47). N+Z with the obvious structure is parsable but not initial, since it fails Peano's fifth axiom. []
The following well known properties of initial T-algebras, due to Lambek and to Lehman and Smyth, give a taste of the rest of this chapter.
PROPOSITION 6.1.4 Let ev:TA® A be an algebra.
Let ev:TF® F be the initial T-algebra.
Let ev:TA\hookrightarrow A be an equationally free algebra. Then
omitted diagram environment
PROOF: [a] Obvious. [b] From (a), since F is initial, there is a unique homomorphism p:F® T F. Then p;ev:F® F is an endomorphism of the initial algebra, so by uniqueness p;ev = id. But as p is a homomorphism, ev;p = T p;Tev = id, so p = ev-1. [c] Similarly, p;m = \idF, but m is mono, so U º F [LS81 , §5.2]. [d] Cancellation of monos, which T preserves. [e] TA is a subalgebra by (a). []
Given any equationally free algebra, we obtain one which is parsable as the intersection of all subalgebras, by the Adjoint Function Theorem 3.6.9. We shall show in Section 6.3 that this is the initial algebra.
Natural numbers Being the free algebra for the functor (-)+1 captures the recursive properties of N, as set out in Remark 2.7.7.
DEFINITION 6.1.5 The diagram on the left below displays the data for any algebra (Q,\opzQ ,\opsQ ) and the homomorphism p:N® Q for the Peano operations. The second diagram re-expresses this in terms of the functor T = (-)+1.
omitted diagram environment
This universal property was identified by Bill Lawvere (1963), and such a structure is called a natural numbers object or simply an NNO.
Since N has a universal property, it is unique. But beware that this relies on second order logic (the induction scheme): there are non- standard structures which share all of the first order properties of N (Remark 2.8.1). Example 6.4.13 gives another characterisation of N.
REMARK 6.1.6 The Lawvere property provides the unique solution for any primitive recursion problem of the form
|
|
omitted diagram environment
In a cartesian closed category the parametric problem may be reduced to the simple one by putting Q¢ = QG , s¢Q :g®l[(x)\vec].s([(x)\vec],g([(x)\vec])) and p¢ = \expx p (Remark 4.7.8). Without these exponentials, G is essential to make the definition invariant under substitution. Similarly the target algebra for recursion over a general free theory must be expressed as
|
EXAMPLE 6.1.7 The recursive argument itself may also occur as a parameter, for example in the factorial function ( cf Example 2.7.8 ):
omitted diagram environment
Exercises 2.46, 6.24 and 6.25 show how to handle this case using pairs.
Finally, the theory (W,ar) may be parametric, but we shall not consider this possibility in this book. In fact we shall usually omit the parameters G and N as well.
Lists For any set (alphabet) G there is a free theory of lists, in which the set of operations is W = G+{x}, with ar[x] = 1 for x Î G and ar[x] = Æ, so TA = {x}+GxA (Definition 2.7.2ff). Here G and W are general (internal) types, and do not have to be concrete enumerations of symbols. The case G = {s} gives the natural numbers.
In a cartesian closed category, using N we can construct equationally free algebras for the theory of lists, and Exercise 6.10 shows (also using pullbacks) that all finitary free theories have free algebras.
LEMMA 6.1.8 There is an equationally free algebra of lists on any set.
PROOF: Put A º ({*} +G)N with
omitted eqnarray* environment
This is the set of streams, in which the symbol * is being used to indicate the end of a (finite) list. More categorically,
|
Infinitary conjunction and disjunction Using infinitary algebraic theories we can now define M\vDash f, the validity of a formula f of the predicate calculus in a model M, in the way sketched in Remark 1.6.12. The meaning of the quantifiers is defined, not by the proof rules, but by infinitary conjunction or disjunction of its instances in M. Note that this model is chosen before defining the infinitary theory below.
EXAMPLE 6.1.9 Let L be a collection of sorts U and relation-symbols r. The (closed raw) formulae of first order predicate calculus (Definition 1.4.1) over L form the free algebra for the free theory with
|
Thus if there are, for example, relation-symbols of arities U2 and Vx W in the theory then a summand [[U]]2+[[V]]x[[W]] is included in W. (The language and model may also have functions, but these do no more than add synonyms for the instances of the relations.)
The arities are given by
ar[T] = ar[^] = ar [r[(u)\vec]] = Æ ar[ Ù] = ar[Ú] = ar[ Þ ] = 2 ar[ $U] = ar["U] = [[U]],
where the arity of the symbols $U and "U also depends on M. The role played before by variable-binding is now taken by the infinite arities. We are interested, not in the free W- algebra, but in the particular structure ev:TW® W (Notation 2.8.2) for which
|
Note that fu is not a single formula with a free variable, but a U-indexed tuple of elements of W (a function U® W). Then a formula f is valid in M if its value in this algebra (calculated , as always with expressions in algebras, by structural recursion) is T. From this we may say what it means for M to obey certain first order axioms, or to satisfy some other property, as in Remark 1.6.13.
Proofs G\vdash f in the predicate calculus also form a free algebra, whose operation-symbols are named by the proof rules (but the formulation of this algebra is complicated by pattern matching and side- conditions which we shall discuss in the next section). By structural induction on the proof, we may show that if M\vDash G then M\vDashf, ie the interpretation is sound. For this structural induction, it is only necessary to verify the soundness of each proof rule individually. []
EXAMPLE 6.1.10 The same conjunctive interpretation, in which r([(f)\vec] ) = Ùjfj in W for every operation-symbol r Î W, is also the basis of strictness analysis. Instead of treating the data types in the program as sets or domains and the values as elements, the (base) types are all interpreted as W and the constructors as conjunction. The program may then be simplified to a conjunction of some of its inputs, namely those that need to be evaluated in order to execute the program. This subset may be found mechanically by the compiler, which may then detect which arguments actually need to be evaluated. []
Existence of equationally free models The following construction is applicable to any free theory; see Example 6.2.7 for the finitary case.
PROPOSITION 6.1.11 Any free theory has an equationally free algebra.
PROOF: Let k = \coprodrar[r] be the rank and A = P(List(k)xW) be the set of sets of lists of odd length. Such lists begin and end with an operation-symbol; each such symbol r (except the last) is followed by a position j Î ar[r] in its arity. In particular, a nullary operation-symbol can only occur at the end of the list.
Define ev(r,[(u)\vec]) = {r}È{[r,j];l|j Î ar[r], l Î \termuj}.
In list notation, l Î ev(r,[(u)\vec]) iff head(l) = r and
either tail(l) = [ ], or head(tail(l)) = j Î ar[r] and tail(tail(l)) Î \termuj.
Then r is characterised as the unique singleton list and
|
The idea of this construction is that the terms are (infinitely branching) trees, and are determined by the set of paths through them from the root. Imagine a term being processed by a program; at any moment it is at a certain point in the tree, with the path stored on its stack, ie as a list. Corresponding to the root there is an operation-symbol, \opr0, with a co-ordinate \numj0 Î ar[\opr0]; the next stage is a similar pair (\opr1,\numj1) with \numj1 Î ar[\opr1] and so on. At the last stage (which is the top of the stack or the head of the list) we have only an operation-symbol \oprn without any specified co-ordinate. Otherwise we would not be able to handle the nullary operations, without which the free algebra would be empty.
It still remains to show that the minimal equationally free T-algebra is initial, but we defer this to Section 6.3, devoting the next section to further, more complicated, examples.