However, we saw in the previous section that there are many applications in which the required structure is not the initial algebra - consisting of all terms - but a subset of ``well formed formulae.'' Wff-systems also have a direct computational meaning: they consist of the hereditary sub-arguments that are actually generated in the course of a particular recursive calculation. So they measure the stack space that it needs, and if an execution goes beyond the largest feasible wff-system then it overflows. This approach can also be used when T is a functor such as the powerset which has no initial algebra.
We shall characterise wff-systems as extensional well founded parse- coalgebras, using a new, categorical, definition of well- foundedness.
The proof of the main theorem - that induction implies recursion - works by pasting together attempts (partial solutions); it is similar to the fixed point theorem (Proposition 3.3.11), but without the need for Scott-continuity. In the infinitary case we want to reapply T after taking the colimit over infinitely many steps. Transfinite iteration can be done using ordinals (Section 6.7), but the soundness of that technique relies on the result we're about to prove.
Instead of doing this tedious and repetitive job ourselves, imagine (after John Conway) that we have a class of servants, who each do what they can before getting tired. Classically, we ask which servant claims to be the most (or maximally) hard-working and, by finding his shortcomings, show how he might have done better. Intuitionistically, the result is obtained by co-operation. It uses second order logic.
Behind this proof is the idea that wff-systems, like attempts, are built up from the empty set by iterating the functor T. The collection of all such coalgebras generalises the von Neumann hierarchy in set theory; the general recursion theorem also comes from that tradition, where it was originally stated for the ordinals. As in set theory, the hierarchy exists even when the initial algebra doesn't.
REMARK 6.3.1 In this section, T:Set® Set will denote any functor that preserves monos and inverse image diagrams, and therefore partial functions and their composition and order (Section 5.3). Extra structure is needed to handle parameters (Exercise 6.23). The functors P, Pf, List and år Î W(-)ar[r] have these properties; in fact they also preserve arbitrary intersections of monos.
Using various such functors, the following development is not absolutely restricted to free theories. Laws of certain forms can be handled, such as commutativity (permutation of maybe infinitely many sub-terms) and idempotence (in the sense of the law r(x,x) = r(x), again infinitarily). Adding these to the theory of lists, the list-forming operations such as cons and append make sets instead.
One can also generalise to a class of supports M (Definition 5.2.10) in categories other than Set with certain completeness conditions [Tay96b].
Well founded coalgebras Definition 6.2.1 captures the feature which was common to the examples of that section, using parse rather than ev.
DEFINITION 6.3.2 Any map parse:X® TX is called a T-coalgebra.
omitted diagram environment
Suppose that whenever the above diagram is a pullback, m is in fact an isomorphism; then we call X a well founded coalgebra. Proposition 6.3.9 and Theorem 6.3.13 are examples of arguments which use this as an idiom of induction.
Exercise 3.42 shows how this new notion of well- foundedness, reduced to its lattice form, relates to induction for well founded relations and for closure conditions (Definitions 2.5.3 and 3.7.8).
EXAMPLE 6.3.3 A coalgebra for the covariant powerset functor defines a binary relation \prec by u\prec t if u Î parse(t), so parse(t) = {u|u\prec t}. Well-foundedness agrees with the old sense (Definition 2.5.3) because
|
The relation is extensional in the set-theoretic sense (Remark 2.2.9),
|
REMARK 6.3.4 Let k:T® P be a cartesian transformation, ie a natural transformation whose naturality squares are pullbacks.
omitted diagram environment
Then parse:X® TX is a well founded T-coalgebra iff the composite parse;kX:X® PX is a well founded P-coalgebra (by Lemma 5.1.2).
There is a natural transformation k:T® P such that the naturality squares with respect to monos are pullbacks iff T preserves arbitrary intersections (as our examples do). Then kX:TX® P(X) by
|
From the point of view of induction (though not algebra) this allows us to identify each expression with its set of immediate sub-expressions, and to do so hereditarily. Certain ideas from set theory now become useful, where for the purposes of universal algebra in the previous chapter they were a nuisance.
REMARK 6.3.5 [Gerhard Osius [Osi74]] Inclusion Y Ì X between wff-systems, or between sets in the set-theoretic sense, is characterised by an (injective) coalgebra homomorphism, ie a function f:Y® X making the square on the left commute:
omitted diagram environment
First notice that the inequality \parseY;P(f) Ì f;\parseX holds iff f is strictly monotone (Definition 2.6.1 ) with respect to the associated \precX and \precY. Then the square commutes iff the lifting property
|
P-coalgebra homomorphisms are simulations (Exercise 3.53).
We write Coalg(T) for the category of T-coalgebras and homomorphisms.
COROLLARY 6.3.6 If there is a coalgebra homomorphism f:Y® X (or an initial segment) with X well founded then Y is well founded too.
PROOF: By Proposition 2.6.2 or Exercise 3.54. There is also a direct categorical proof [Tay96b], in which \funf* º [fop] (Remark 3.8.13(b)) is applied to the subset V Ì Y testing well-foundedness of Y. []
See Exercise 3.41 for the lattice version.
The recursion scheme Recall from Definition 2.5.1 that the three phases of the recursive paradigm say that p = parse;Tp;ev.
We use partial functions with the extension order \sqsubseteq (Definition 3.3.3).
DEFINITION 6.3.8 [Osius]Let \parseX:X® TX be a coalgebra and \evQ :TQ\rightharpoonup Q a (partial) algebra. Then p:X\rightharpoonupQ is an attempt if p\sqsubseteq \parseX;Tp;\evQ , and satisfies the recursion equation if these are equal as partial functions, ie have the same support.
omitted diagram environment
The coalgebra obeys the recursion scheme if for every such (Q,\evQ ) there is a unique p:X\rightharpoonup Q with p = parse;Tp;\evQ . In particular, if \parseX = \evX-1 and \evQ is total, this diagram says that \evX:TX® X is the initial T-algebra.
This is a very convenient diagrammatic form in which to present recursive programs, as we illustrate in Example 6.4.7 and Exercises 6.27ff.
LEMMA 6.3.9 Any partial attempt p:X\rightharpoonup Q is given by a total one p = (p¢;ev):Y® Q, the support i:Y\hookrightarrow X being an initial segment.
omitted diagram environment
If f:Z® Y is another coalgebra homomorphism then f;p:Z® Q (restriction along f) also satisfies the recursion equation.
PROOF: Expand and rearrange the diagram of partial functions. []
PROPOSITION 6.3.10 If \parseZ:Z® TZ is well founded then there is at most one total function p:Z® Q satisfying the recursion equation.
PROOF: Suppose p,q:Z\rightrightarrows Q both satisfy it. Then the two parallel rectangles on the right commute since p and q are total attempts. Let e:E\hookrightarrow Z\rightrightarrows V be the equaliser of p and q, and form the pullback H.
omitted diagram environment
The composites H\rightrightarrows TQ are equal by construction, and j is mono by hypothesis. Hence H\hookrightarrow Z\rightrightarrows V are equal, and H\hookrightarrow Z factors through the equaliser, so e:E º Z by well-foundedness of Z, whence p = q. []
Notice that once again we have uniqueness before existence (page 1.3.1).
REMARK 6.3.11 Using the conjunctive interpretation (Example 6.1.10), well-foundedness is also necessary for uniqueness. For T = P, Q = W and ev = Ù = ", the recursion equation reduces to
|
This result should be treated with circumspection: taking Q = W means that we are using higher order logic (a point which is obscured classically, where W = 2). Induction for the second order predicate f[x] º (x\not \prec x) shows that well founded relations in this sense are irreflexive, and so are too clumsy to analyse fixed points of iteration. By closer examination of the carrier and structure of the intended target of recursion, maybe we can restrict the class of subsets (predicates) to those that need to be considered, and thereby get a weaker notion of well-foundedness which admits more source structures X but remains sufficient for recursion.
The general recursion theorem It remains to show that well-foundedness is sufficient for recursion. There is a zero attempt, with Æ as support, and we now describe the successor.
LEMMA 6.3.12 Let parse:X® T X be a coalgebra and p:X\rightharpoonup Q be an attempt. Then Tparse:TX® T2X is also a coalgebra and (T p;ev):TX\rightharpoonup Q and p\sqsubseteq q º (parse;T p;ev):X\rightharpoonup Q are attempts.
omitted diagram environment
Note that this is a diagram of partial functions: Remark 6.3.1 says that T acts on such diagrams. []
Let's pause to look at this symbolically. In set theory, given an attempt
|
|
|
LEMMA 6.3.13 Let X be a well founded coalgebra and \polly0,\polly1:X\rightharpoonupQ be attempts. Then there is an attempt p with \polly0,\polly1\sqsubseteq p.
PROOF: Let \typeY0,\typeY1 Ì X be the supports of \polly0 and \polly1, so \typeY0 and \typeY1 are initial segments of X (Lemma 6.3.8). By Lemma 5.8.9, the union Y = \typeY0È\typeY1 Ì X is the pushout over the intersection Z = \typeY0Ç\typeY1. These are also initial segments: the structure map of Z mediates to T\typeY0ÇT\typeY1 = T(\typeY0Ç\typeY1), and that of Y from the pushout. Then Y and Z are well founded by Corollary 6.3.6. The restrictions of \polly0 and \polly1 to Z satisfy the recursion equation (Lemma 6.3.8), so agree by Proposition 6.3.9. Hence we may form the union p:Y® Q of the partial functions as a pushout mediator, and p = \parseY;Tp;ev because the right hand side also mediates from this pushout. []
THEOREM 6.3.14 Let X be a well founded coalgebra and Q a partial algebra. Then there is a greatest attempt p:X\rightharpoonup Q, and this satisfies the recursion equation, p = \parseX;Tp;ev. If Q is total then so is p.
PROOF: Attempts X\rightharpoonup Q form an ipo, which we have just shown to be directed as well, so let p:X\rightharpoonup Q be the greatest one (by the Adjoint Function Theorem 3.6.9), with support Y. As \parseX;Tp;ev is also an attempt (Lemma 6.3.11), by maximality we have p = \parseX;Tp;ev.
omitted diagram environment
Suppose now that Q is total. Form the pullback H, with \parseH = l;Tk and q = l;Tp;ev. Then k;q = k;l;Tp;ev = p and \parseH;Tq;ev = q. So q:H® Q is an attempt, but p:Y® Q is the greatest such, so H = Y, but then Y = X by well-foundedness. []
Exercise 3.40 gives the lattice analogue.
In applications such as Remark 6.2.10 and Proposition 6.2.6, we need the homomorphism p to be total on the hypothesis that \evQ is defined ``whenever it needs to be.'' It is still necessary to use methods of proof by induction, but now the issue is that the steps be well defined (partial correctness ) rather than that the whole process terminate.
Finally, we characterise wff-systems and the term algebra itself.