Practical Foundations of Mathematics

Paul Taylor

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.

 Aar[r] ®     \oprA    A            T A = \coprodr Î WAar[r] ®  \evA  A
As there is only one sort, these may be combined into one function \evA, called the structure map, as shown on the right. As there are no laws, any such map defines an algebra ( cf Proposition  7.5.3(b) for monads).

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

 \oprA( ®u ) = \opsA( ®v )   Þ   r º s   Ù  "j:ar[r].\termuj = \termvj,
and parsable if \evA is an isomorphism, so every u Î A is r([(v)\vec]) for some unique r Î W and [(v)\vec] Î Aar[r]. Compare Example 3.7.9(f), where we needed "t.$!K.K\triangleright t. Note that algebraic theories with laws usually have no equationally free models. 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. (a) Then Tev:T2 A® TA is also an algebra and ev:T A® A is a homomorphism. Let ev:TF® F be the initial T-algebra. (b) Then it is parsable, ie ev:TF º F; (c) and any T-subalgebra U Ì F is the whole of F. (Out of classical habit, we say that F has no proper subalgebra.'') Let ev:TA\hookrightarrow A be an equationally free algebra. Then (d) if T preserves monos, any subalgebra U Ì A is also equationally free, (e) but if A has no proper subalgebra then it is parsable. 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  p(0) = \opzQ p(n+1) = \opsQ (p(n)), but the elimination rule in Remark 2.7.7,  omitted prooftree environment allowed \opzQ and \opsQ to be expressions with parameters from a context G. Incorporating them, the diagram becomes 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  GxTQ º Gx\coprod \nolimitsr Q ar[r] º \coprod \nolimitsr æè Gx Q ar[r] öø ® evQ, where the sums have to be stable (Section 5.5) as shown. For a general abstract functor T to admit parametric recursion, additional structure, known as a strength, is needed; see Exercise 6.23. The polynomial functors arising from free theories and the other functors over which we shall consider recursion all admit this structure in an obvious way. 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,  {x}+Gx A\hookrightarrow A+GxA º ({*} +G){0}+N \hookrightarrow ({*} +G)N, ie ev:TA\hookrightarrow A, for any N such that N\twoheadrightarrow {0}+N. [] 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  W = {T,^,Ù,Ú,Þ } + {r[(u)\vec]} + {$U,"U}.
The last term adds two copies of the set S of sorts to W. The set of symbols of the form r[(u)\vec] contributed to W depends on the model M in which we aim to interpret L, specifically the sets [[U]] denoted by the sorts U: r[(u)\vec] ranges over the instances of each relation-symbol at each tuple in the interpretation of its arity.

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

 ev(\$U, ®f ) Ú u Î [[U]] fu        ev("U, ®f ) Ù u Î [[U]] fu
and each nullary operation r[(u)\vec] is a propositional constant [[r[\vec] u]] Î W (which is again prescribed by the model M). The constants T and ^ and binary operation- symbols Ù, Ú and Þ have the usual meanings in  W.

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

 \termuj = {l| æè [r,j];l öø Î ev (r, ®u )},
so this algebra is equationally free. []

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.