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.