In this section we extend the principle of recursion induction so that it can be applied directly to Algolic programs without first transforming them to recursive functions. Consider the Algolic program

We want to prove it equivalent to the program

Before giving this proof we shall describe the principle of recursion induction as it applies to a simple class of flow charts. Suppose we have a block of program represented by fig. 3a. Suppose we have proved that this block is equivalent to the flow chart of fig. 3b where the shaded block is the original block again. This corresponds to the idea of a function satisfying a functional equation. We may now conclude that the block of fig. 3a is equivalent to the flow chart of fig. 3c for those state vectors for which the program does not get stuck in a loop in fig. 3c.

Fig. 3 Recursion induction applied to flow charts.

This can be seen as follows. Suppose that, for a
particular input, the program of fig. 3c goes around the
loop *n* times before it comes out. Consider the flow
chart that results when the whole of fig. 3b is substituted
for the shaded (or yellow) block, and then substituted into this
figure again, etc. for a total of *n* substitutions. The state
vector in going through this flow chart will undergo
exactly the same tests and changes as it does in going
through fig. 3c, and therefore will come out in *n* steps
without ever going through the shaded (or yellow) block. Therefore,
it must come out with the same value as in fig. 3c.
Therefore, for any vectors for which the computation
of fig. 3c converges, fig. 3a is equivalent to fig. 3c.

Thus, in order to use this principle to prove the equivalence of two blocks we prove that they satisfy the same relation, of type 3a-3b, and that the corresponding 3c converges.

We shall apply this method to showing that the two programs mentioned above are equivalent. The first program may be transformed as follows:

from

to

The operation used to transform the program is simply to write separately the first execution of a loop.

In the case of the second program we go:

from

to

to

to

The operations used here are: first, the introduction
of a spurious branch, after which the same action is
performed regardless of which way the branch goes;
second, a simplification based on the fact that if the
branch goes one way then *n* = 0, together with rewriting
one of the right-hand sides of an assignment statement;
and third, elimination of a label corresponding to a
null statement, and what might be called an anti-simplification
of a sequence of assignment statements.
We have not yet worked out a set of formal rules
justifying these steps, but the rules can be obtained
from the rules given above for substitution, replacement
and manipulation of conditional expressions.

The result of these transformations is to show that
the two programs each satisfy a relation of the form:
*program* is equivalent to

The program corresponding to fig. 3c in this case, is precisely the first program which we shall assume always converges. This completes the proof.

Tue May 14 13:32:03 PDT 1996