The previous section gave a categorical generalisation of the recursive paradigm (Definition 2.5.1), where the way in which a program calls itself was controlled by a certain functor. Now we shall consider the special case in which the functor is of the form TX = X+N, where N Ì X is the set of base cases or exit states.
DEFINITION 6.4.1 In a tail-recursive program,
In the functional style this is
|
Operationally, the sub-argument s(x) may be assigned to the variable x, and the continuation z from the (most deeply) nested call is just that from the main program, so the functional idiom of tail recursion translates directly into the imperative while program
|
DEFINITION 6.4.2 The simple imperative language extends the conditional declarative language of Definition 5.3.7 by the \bnfname program
|
EXAMPLE 6.4.3 The following program computes the highest common factor (y) of two integers a,b Î Z by Euclid's algorithm.
omitted program environment
where
|
REMARK 6.4.4 Notice that both parts of Definition 6.4.1 are needed for the translation into a while program. The definition of the factorial function, read as a program, is not tail-recursive because the argument must be saved for the multiplication with the sub-result. Unary recursion (satisfying just the first condition) can, however, be translated into tail recursion by using an accumulator (Exercise 6.26).
It is unlikely that there is such a uniform way of reducing the arity of a recursion, though it can sometimes be done. For example, the Fibonacci function is defined by
|
Semantics Fixed points in order structures (Sections 3.3- 3.5) give the semantic treatment of recursion which is perhaps the best known, but they take no notice of the recursive paradigm, let alone the special case of tail recursion. After setting up notation like that in Section 5.3, we shall use various categorical techniques to axiomatise the naive understanding of iteration. There are several threads in our treatment, describing the data and results in terms of partial functions, relational algebra, recursion for a functor as in the previous section, and the categorical structure of Section 5.8, so you should feel free to skip some parts.
REMARK 6.4.5 We shall consider the program
|
omitted diagram environment
Let X = Y+N be the partition induced by the loop condition and S Ì Y Ì X the support of the partial function which represents the body s of the loop, so SÇN = Æ.
omitted diagram environment
Together with the code G\rightharpoonup X and N\rightharpoonupQ before and after the loop, the whole program is illustrated by the staircase diagram, in which the S step may be repeated any number of times. The letters of course stand for successor and zero, but notice that they count backwards: comparing tail recursion with Remark 2.7.7, s is the predecessor. (This is the reason for using the letter z for continuations.) Because of the exit condition, N is the target of the partial function W which represents the whole loop.
REMARK 6.4.6 Rearranging the data, the span
omitted diagram environment
defines a partial map parse:X\rightharpoonup X+N, which is a coalgebra for the functor T = (-)+N. The algebra is ev º [id,z]:Q+N® Q, or just the codiagonal Ñ:N+N® N with no continuation z:N® Q after the loop. The two conditions for tail recursion are respectively that the functor and algebra be of these forms; Exercise 6.26 deals with arbitrary algebras ev º [a,z]:QxX+N® Q. As the functor is always the same, we drop the use of T for it and use this letter for something else.
Recall from Lemma 6.3.8 that a partial attempt X\rightharpoonup Q is a total attempt on a subcoalgebra, X\hookleftarrow W® Q. The rectangle on the right below says that \nearrow = if cthen s;\nearrow elsezfi.
omitted diagram environment
In particular the loop w itself (with trivial continuation z = id) satisfies
|
EXAMPLE 6.4.7 For the Euclidean algorithm N = {0}xZ\hookrightarrow X = ZxZ and we define parse:X® TX = (ZxZ)+Z by
|
omitted diagram environment
The loop terminates since |x| Î N, the loop measure, strictly decreases ( cf Remark 2.5.13, Proposition 2.6.2 and Corollary 6.3.6). []
REMARK 6.4.8 Barry Jay observed that any map f:X® Q with m;f = s;f is invariant in the strict sense that its value is restored after each iteration, so it is the same when the loop terminates (if it does) as at the beginning. Such a map factors through the coequaliser Q, which Jay called the universal loop invariant.
omitted diagram environment
The correctness of while loops is always shown by finding an appropriate invariant. Indeed every competent programmer writes ``the state of the variables at the point of the loop test is ...'' or similar. This is vital, as the commonest error is to be out by 1 in an array suffix.
However, the established usage of the term loop invariant is for a predicate (so Q = W) such that, if it holds before execution of the body then it holds afterwards. In other words, f may become valid when it had not been before, and the converse implication is not relevant. (The heredity operation, Definition 2.5.4, turns such a lax invariant into one in Jay's strict form, cf Theorem 3.8.11(a) and Exercise 6.2.) The coequaliser must also be modified to account for the exit condition N.
In fact we shall show that, in the diagram
omitted diagram environment
both composites are \idN and w is the coequaliser of the parallel pair. It follows that the recursion equation for any z:N® Q has a unique solution, since z is the unique mediator from the coequaliser .
We shall use relational algebra to investigate this coequaliser in terms of the associated equivalence relation. The results do not apply to arbitrary categories, but rely on certain exactness properties of Set, and our aim, as in the previous chapter, is to find out what these are: we need stable coequalisers not just of congruences but of functional relations. Recall that general coequalisers are computed in several steps (Lemma 5.6.11), not all of which are needed this case, but we still need to consider stable directed unions in order to form the transitive closure.
The coequaliser is also peculiar to this situation in another respect, namely that it only works for unary recursion, cf the special properties of unary algebra in Section 3.8. In an arbitrary coalgebra, an element is well founded iff all of its children (Remark 6.3.4) are well founded. If there is just one child, the parent is well founded iff the child is, so the well founded elements are exactly those that are related to childless (base) cases by the equivalence generated by the transition relation. It is like König's Lemma, except that there is no choice to be made.
Transitive closure The partial function s will now be treated as a binary relation S:X\leftharpoondown \rightharpoonup X and the subset N Ì X as a subrelation of the diagonal D ( cf the virtual objects in Proposition 5.8.7). These relations should be thought of as transition graphs on the set X of states; evaluation of the whole program W consists in following the relation S, or rather its transitive closure T, until we arrive inside the subset N, so W = T;N. (The letter T is no longer a functor.)
We take up the story of the transitive closure from Proposition 3.8.7, where it was defined by a unary induction scheme. Frege (1879) showed that the transitive closure of any functional relation S is trichotomous (classically). We shall show instead that it is confluent (Definition 1.2.5), so the equivalence closure is K = T;Top . Working backwards, K is the kernel of a coequaliser, and also gives enough information to allow us to investigate T and W. Exercise 3.60 instead considers the transitive closure as a list of steps, capturing the imperative idiom directly.
Let R = SÈD be the reflexive closure of S, and E = (S+N)ÇD the equaliser of (S+N)\rightrightarrows X, so N Ì E. Note that A+B denotes the union AÈB of two relations, but also signifies that they are disjoint, ie AÇB = Æ ( cf the use of Ú in Notation 3.4.3).
LEMMA 6.4.9 Let S:X\leftharpoondown \rightharpoonup X be a relation in a prelogos with countable stable unions, or in a logos, or in a division allegory (Lemma 5.8.8(c)).
If S:X\rightharpoonup X is functional then
PROOF: In a prelogos with stable countable unions,
|
They may also be proved in a finitary way using the universal properties in a logos. We show, in the notation of Lemma 5.8.8(c), that
|
displaymath omitted prooftree environment
It is curious that we need two forms (a) and (b) of the inductive principle.
The recursion and induction schemes Now we are equipped to justify Remarks 6.4.6 and 6.4.8 and see how the categorical induction and recursion schemes from Section 6.3 restrict to tail recursion.
THEOREM 6.4.10 The relation W = K;N is functional; it is the least solution ( cf Section 3.3) of the recursion equation
|
PROOF: Since N = Nop = E;N = N;T by Lemmas 6.4.9(c) and (f),
|
|
|
Finally let V:X\leftharpoondown \rightharpoonup X be another solution, so N Ì V É S;V. Then T;V Ì V by Lemma 6.4.9(a), and W = T;N Ì T;V Ì V. []
The discussion of the transitive closure above completes the investigation of the stability of the steps in the construction of general coequalisers in Lemma 5.6.11. The fact that K;N is functional can be restated in terms of coequalisers, and is of interest in itself. It relies on stability of unions: see Example 5.8.2(d) for a counterexample in Gp. Without loss of generality (by adding a loop counter), the body always changes the state, ie N = E.
PROPOSITION 6.4.11 Let U\rightrightarrows X be a functional endo-relation in a logos or a pretopos with stable countable unions. Let E and Q be the equaliser and coequaliser. Then the common composite shown is mono:
omitted diagram environment
This says that there is at most one fixed point in each component of the transition graph of a functional relation.
PROOF: Two elements x,y:G\rightrightarrows E of the equaliser become identified in the coequaliser Q º X/K iff x,y Î K, since Q is effective. Then
|
REMARK 6.4.12 The construction of W is shown in the diagram below. As a rule, pullbacks of parallel pairs need not have the same vertex, but they do here because, as the composites S+N\rightrightarrows X® Q are equal, we may form the pullbacks rooted at Q (Lemma 5.1.2, Exercise 5.53).
omitted diagram environment
With the same assumptions as before (and in particular in Set), W\twoheadrightarrow N is the coequaliser of the pair shown. For suppose that V:X\rightharpoonup Q with support W has equal composites; then N;V Ì V and S;V Ì V, so
|
EXAMPLE 6.4.13 [Peter Freyd [Fre72]] Consider the following special case, with x:N, which always terminates:
|
omitted diagram environment
where N® N+1 is the usual coalgebra structure, which is well founded by Peano induction. (Beware that we have re-indexed this diagram: the above discussion actually gives id,pred:{n|n ³ 1}\rightrightarrows N.)
PROPOSITION 6.4.14 In the sense of Definition 6.3.2, W is the largest well founded subcoalgebra of X.
omitted diagram environment
PROOF: Treat V Ì W as a subrelation, so the pullbacks are relational composites as shown. The diagrammatic induction scheme says that
|
COROLLARY 6.4.15 W is the unique well founded solution to the fixed point equation in Theorem 6.4.10. []
Partial correctness Recall the difference between total and partial correctness, expressed in terms of modal logic in Example 3.8.3.
REMARK 6.4.16 For a partial program u:X\rightharpoonup Y, the triple
|
Let A = {x,x¢|x = x¢Ùf[x]} and B = {y,y¢|y = y¢Ùq[y]} be subdiagonal relations as before.
omitted diagram environment
Then A;U Ì A Ì X consists of those states for which f holds and u terminates; the effect of u is the composite A;U\hookrightarrow U® Y. The partial Floyd triple says that this factors through B Ì Y. Hence there is a pullback mediator A;U® U;B as shown, or, in terms of relations, A;U Ì U;B:X\leftharpoondown\rightharpoonup Y.
THEOREM 6.4.17 w satisfies the partial correctness Floyd rule
|
PROOF: With A = {x,x¢|x = x¢Ùq[x]}, the premise says that
|
|
By Corollary 6.4.15, the behaviour of a while program is captured by proving partial correctness like this, together with termination, ie well-foundedness of the coalgebra W, which is done by finding a loop measure.
Discussion Although we have used properties of Set, in particular the transitive closure, to prove correctness of the interpretation, it can be stated using pullbacks, coproducts and coequalisers alone. This means that any ( exact) functor which preserves finite limits and finite colimits also preserves the interpretation.
REMARK 6.4.18 Correctness is reflected if the functor F:C\hookrightarrow S is also full and faithful. For suppose that both categories have the limits and colimits needed to draw the diagrams in this section (so F makes these agree) and that in S we have shown that FW\rightrightarrows FX is a functional relation satisfying
Then F preserves composition and intersection of relations, and reflects their containment, so these properties restrict to C. In particular, Freyd's characterisation of N (Example 6.4.13) says that exact functors between toposes, such as inverse images of geometric morphisms, preserve N. []
When can a category without infinite unions be embedded in one with them, thereby generalising the interpretation?
Stability of the coequaliser is clearly necessary, but unfortunately seems not to be sufficient. But if the coequaliser of S+N\rightrightarrows X and its kernel K exist then the cocone (DÈSÈSop)n\hookrightarrow K indexed by n Î N is always colimiting, even though we have not asked for a general infinitary union operation. Then a pretopos C can be embedded in a topos of sheaves on C preserving (finite limits, coproducts, quotients of equivalence relations and) the coequaliser iff this union is stable under pullbacks in C.
Using this condition there is a simpler way to extend the proof: we only need unions of relations, not the virtual objects in this sheaf topos.
THEOREM 6.4.19 The language is correctly interpreted in any pretopos such that each functional relation has an equivalence closure which is stably the union of powers. Any functor which preserves finite limits and colimits also preserves the interpretation.
PROOF: Define an ideal relation A:X\leftharpoondown \rightharpoonup Y to be a set of relations B Ì Xx Y which is closed downwards and under whatever stable unions already exist ( cf Theorem 3.9.9). For example
|
|
|