Practical Foundations of Mathematics

Paul Taylor

6.4  Tail Recursion and Loop Programs

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,

(a)
there is at most one sub-argument to each recursive call, and

(b)
its sub-result is immediately passed out as that of the whole program (in particular the original argument is not needed).

In the functional style this is

p(x) = omitted casearray environment
Subordinate clauses, in which the reader (or listener) must remember what's going on in the surrounding text, illustrate recursion in grammar; a tail- recursive version would put them at the end of the sentence.

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

\nearrow while c(x) dox: = s(x) od; z.

DEFINITION 6.4.2 The simple imperative language extends the conditional declarative language of Definition 5.3.7 by the \bnfname program

while \bnfname Boolean expression do \bnfname program od
As in the conditional, the test has type 2 ( not W), and the same variables must be in scope at the end of the body of the loop as at the beginning.

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

y[u,v] "m.m| am| b m| um| v
is the (strict) loop invariant. From the last comment we can deduce immediately that y| ay| b, so y is the highest common factor. []

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

fib(n+2) = fib(n)+fib(n+1)        fib(0) = fib(1) = 1,
so is a binary recursion, ie it makes two nested calls at each level, and the functor is T = (-)2+N. This program therefore has exponential complexity, but there is also a tail-recursive program that calculates the same function in linear or even logarithmic time (Exercise 6.27).

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

\nearrow = w;z     where w = while cdosod,
subject to Assumption 5.3.8, that the condition c always terminates without side-effect, but now the assignment puty = c must be inserted at the end of the body of the loop, as well as before the loop.

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 SN = .

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

w = if cthen s;w else skipfi
The semicolons arise from the relational algebra which we shall use.

EXAMPLE 6.4.7 For the Euclidean algorithm N = {0}xZ\hookrightarrow X = ZxZ and we define parse:X TX = (ZxZ)+Z by

parse(x,y) = omitted casearray environment
the diagram:

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 = SD 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 AB of two relations, but also signifies that they are disjoint, ie AB = ( 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)).

(a)
For any relation  V:X\leftharpoondown \rightharpoonup Q, if S;V V then T;V V.

(b)
For any relation A:X\leftharpoondown \rightharpoonup X, if A;S S;A then A;T T;A.

(c)
E;T = E.

If S:X\rightharpoonup X is functional then

(d)
R = SD is confluent (Definition  1.2.5), ie Rop;R R;Rop;

(e)
T is also confluent ( cf Lemma  1.2.4);

(f)
K = T;Top.

PROOF: In a prelogos with stable countable unions,

T =

n = 0 
Sn =

 
Rn        T;N = \coprod n = 0 (Sn;N) =

 
Rn;N
from which the results follow by brute force.

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

Q = V\V,     A\(T;A) and E\E
satisfy the premises of the unary induction scheme in Definition  3.8.6, and so contain T. (In the present notation, we used T/T there to show that T;T T.)

(a)
[[a]]

displaymath omitted prooftree environment

(b)
[[b]] Transitivity of A\(T;A) is similar; also A;S S;A T;A, so S A\(T;A) and T A\(T;A). Hence A;T T;A.

(c)
[[c]] E;S E, so by (aop), E;T E = E;D E;T.

(d)
[[d]] Sop;S D, so Rop;R = D SSopSop;S = DSSop R;Rop.

(e)
[[e]] As in (b), A;R R;A A;T T;A; with Rop for A, by (d), Rop;T T;Rop. By the same principle for the opposite relations, now with Top for A, we have Top;T T;Top.

(f)
[[f]] T;Top;T;Top T;T;Top;Top T;Top. []

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

w = ifcthens;welse skipfi,
and satisfies c = no on exit.

PROOF: Since N = Nop = E;N = N;T by Lemmas  6.4.9(c) and (f),

W = K;N = T;Top;N = T;N.
Then by Lemma 6.4.9(e),
Wop;W = N;Top;T;N N;T;Top;N = N D,
and by Proposition 3.8.7(b) and Lemma  5.8.8(b),
W = T;N = (DS;T);N = NS;T;N = N+S;W,
which is the recursion equation. This condition is no on exit from w because W = K;N = K;N;N = W;N.

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

x,y E;K;Eop = E;T;Top;Eop = E;Eop = E D
by Lemmas 6.4.9(c) and (f) with S = U, so x = y as claimed. []

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

W;N;V = T;N;V T;V V :X\rightharpoonup Q,
but these are functional relations with the same support, so are equal. So N;V is a coequaliser mediator; it is unique as W\twoheadrightarrow N is epi. []

EXAMPLE 6.4.13 [Peter Freyd [Fre72]] Consider the following special case, with x:N, which always terminates:

whilex > 0 dox: = x-1 od.
The partition is N = {0} and Y = {n|n 1}; this and the interpretation of the program are then the coproduct and coequaliser diagrams

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

omitted prooftree environment
which we have already deduced from Lemma 6.4.9(a). The way that W was constructed, as a pullback, makes it the largest well founded subcoalgebra by Exercise 6.17. []

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

{f} u {q}
is redefined to mean that, if u terminates and f holds beforehand, then q holds afterwards.

Let A = {x,x|x = xf[x]} and B = {y,y|y = yq[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

omitted vchbox environment        omitted vchbox environment
for any predicate q on X.

PROOF: With A = {x,x|x = xq[x]}, the premise says that

(YA);S = A;Y;S = A;S S;A
(since S is only defined on Y anyway), so by Lemma  6.4.9(b),
A;W = A;T;N T;A;N = T;N;A = W;(AN)
(since A,Y,N D), which is the conclusion. []

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

(a)
FW = F N+FS;FW = FW;FN,

(b)
"V.  FN V FS;V FW V , and

(c)
"A.  A;FS FS;A A;FW FW;A.

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 (DSSop)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

(A) = {B|B A}    {B|B;E E}     {B|V;B V}.
Ideal relations can be shown to form a division allegory (Proposition  5.8.7). The second and third examples are transitive, as is
{B|(A;B) \cat T;A}
for any transitive ideal relation \cat T, by the same argument as for Lemma 6.4.9. The crucial point is that
(K) = \cat T;\cat Top,
where we return from the ideal transitive closure \cat T to the real equivalence closure K. For this we need that the latter be a stable union. []