In this section 1 want to establish a relation between
the use of recursive functions to define computations,
the flow chart notation, and programs expressed as
sequences of ALGOL-type assignment statements,
together with conditional **go to**'s. The latter we shall
call *Algolic* programs with the idea of later extending
the notation and methods of proof to cover more of the
language of ALGOL. Remember that our purpose here
is not to create yet another programming language, but
to give tools for proving facts about programs.

In order to regard programs as recursive functions,
we shall define the *state vector* of a program at a given
time, to be the set of current assignments of values to the
variables of the program. In the case of a machine
language program, the state vector is the set of current
contents of those registers whose contents change
during the course of execution of the program.

When a block of program having a single entrance and exit is executed, the effect of this execution on the state vector may be described by a function giving the new state vector in terms of the old. Consider a program described by the flow chart of fig. 1.

Fig. 1 Flow chart for equations shown below.

The two inner computation blocks are described by
functions and , telling how these blocks affect
the state vector. The decision ovals are described by
predicates , , and that give the conditions
for taking the various paths. We wish to describe the
function that gives the effect of the whole block,
in terms of the functions f and g and the predicates
*p*, , and . This is done with the help of two auxiliary
functions *s* and *t*. describes the change in between
the point labelled *s* in the chart and the final exit from
the block; *t* is defined similarly with respect to the
point labelled t. We can read the following equations
directly from the flow chart:

In fact, these equations contain exactly the same information as does the flow chart.

Consider the function mentioned earlier, given by

It corresponds, as we leave the reader to convince himself, to the Algolic program

Its flow chart is given in fig. 2.

This flow chart is described by the function and the equation

where corresponds to the condition *n*=0, to
the statement *n* := *n* - 1, and to the statement
.

Fig. 2 Flow chart for as described by the following equations.

where

and so

We shall regard the state vector as having many
components, but the only components affected by the
present program are the *s*-component and the *n*-component.
In order to compute explicitly with the
state vectors, we introduce the function which
denotes the value assigned to the variable in the
state vector , and we also introduce the function
which denotes the state vector that results
when the value assigned to in is changed to
,
and the values of the other variables are left unchanged.

The predicates and functions of state vectors mentioned above then become:

We can prove by recursion induction that

but in order to do so we must use the following facts about the basic state vector functions:

The proof parallels the previous proof that

but the formulae are longer.

While all flow charts correspond immediately to
recursive functions of the state vector, the converse is
not the case. The translation from recursive function to
flow chart and hence to Algolic program is immediate,
only if the recursion equations are in *iterative* form.
Suppose we have a recursion equation

where is a conditional
expression defining the function *r* in terms of the
functions . is said to be in iterative form if *r*
never occurs as the argument of a function but only in
terms of the main conditional expression in the form

In the examples, all the recursive definitions except

are in interative form. In that one, (*n* - 1)! occurs as
a term of a product. Non-iterative recursive functions
translate into Algolic programs that use themselves
recursively as procedures. Numerical calculations can
usually be transformed into iterative form, but computations with symbolic expressions usually cannot, unless
quantities playing the role of push-down lists are
introduced explicitly.

Tue May 14 13:32:03 PDT 1996