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.'' Wffsystems also have a direct computational meaning: they consist of the hereditary subarguments 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 wffsystem 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 wffsystems 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 Scottcontinuity. 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) hardworking and, by finding his shortcomings, show how he might have done better. Intuitionistically, the result is obtained by cooperation. It uses second order logic.
Behind this proof is the idea that wffsystems, 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, P_{f}, 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 subterms) and idempotence (in the sense of the law r(x,x) = r(x), again infinitarily). Adding these to the theory of lists, the listforming 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 Tcoalgebra.
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) = {uu\prec t}. Wellfoundedness agrees with the old sense (Definition 2.5.3) because

The relation is extensional in the settheoretic 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 Tcoalgebra iff the composite parse;k_{X}:X® PX is a well founded Pcoalgebra (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 k_{X}: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 subexpressions, 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 wffsystems, or between sets in the settheoretic 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 \parse_{Y};P(f) Ì f;\parse_{X} holds iff f is strictly monotone (Definition 2.6.1 ) with respect to the associated \prec_{X} and \prec_{Y}. Then the square commutes iff the lifting property

Pcoalgebra homomorphisms are simulations (Exercise 3.53).
We write Coalg(T) for the category of Tcoalgebras 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_{*} º [f^{op}] (Remark 3.8.13(b)) is applied to the subset V Ì Y testing wellfoundedness 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 \parse_{X}:X® TX be a coalgebra and \ev_{Q} :TQ\rightharpoonup Q a (partial) algebra. Then p:X\rightharpoonupQ is an attempt if p\sqsubseteq \parse_{X};Tp;\ev_{Q} , 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,\ev_{Q} ) there is a unique p:X\rightharpoonup Q with p = parse;Tp;\ev_{Q} . In particular, if \parse_{X} = \ev_{X}^{1} and \ev_{Q} is total, this diagram says that \ev_{X}:TX® X is the initial Talgebra.
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 \parse_{Z}: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 wellfoundedness 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), wellfoundedness 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 wellfoundedness which admits more source structures X but remains sufficient for recursion.
The general recursion theorem It remains to show that wellfoundedness 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® T^{2}X 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 \polly_{0},\polly_{1}:X\rightharpoonupQ be attempts. Then there is an attempt p with \polly_{0},\polly_{1}\sqsubseteq p.
PROOF: Let \typeY_{0},\typeY_{1} Ì X be the supports of \polly_{0} and \polly_{1}, so \typeY_{0} and \typeY_{1} are initial segments of X (Lemma 6.3.8). By Lemma 5.8.9, the union Y = \typeY_{0}È\typeY_{1} Ì X is the pushout over the intersection Z = \typeY_{0}Ç\typeY_{1}. These are also initial segments: the structure map of Z mediates to T\typeY_{0}ÇT\typeY_{1} = T(\typeY_{0}Ç\typeY_{1}), and that of Y from the pushout. Then Y and Z are well founded by Corollary 6.3.6. The restrictions of \polly_{0} and \polly_{1} 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 = \parse_{Y};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 = \parse_{X};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 \parse_{X};Tp;ev is also an attempt (Lemma 6.3.11), by maximality we have p = \parse_{X};Tp;ev.
omitted diagram environment
Suppose now that Q is total. Form the pullback H, with \parse_{H} = l;Tk and q = l;Tp;ev. Then k;q = k;l;Tp;ev = p and \parse_{H};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 wellfoundedness. []
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 \ev_{Q} 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 wffsystems and the term algebra itself.