next up previous
Next: Recursion Induction on Algolic Up: Towards a Mathematical Science Previous: Proving Statements About Recursive

Recursive Functions, Flow Charts, And Algolic Programs

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 tex2html_wrap_inline559 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 tex2html_wrap_inline561 giving the new state vector in terms of the old. Consider a program described by the flow chart of fig. 1.

tex2html_wrap645

Fig. 1 Flow chart for equations shown below.

displaymath145

The two inner computation blocks are described by functions tex2html_wrap_inline563 and tex2html_wrap_inline565 , telling how these blocks affect the state vector. The decision ovals are described by predicates tex2html_wrap_inline567 , tex2html_wrap_inline569 , and tex2html_wrap_inline571 that give the conditions for taking the various paths. We wish to describe the function tex2html_wrap_inline573 that gives the effect of the whole block, in terms of the functions f and g and the predicates p, tex2html_wrap_inline577 , and tex2html_wrap_inline579 . This is done with the help of two auxiliary functions s and t. tex2html_wrap_inline585 describes the change in tex2html_wrap_inline559 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:

eqnarray157

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

Consider the function mentioned earlier, given by

displaymath483

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

eqnarray171

Its flow chart is given in fig. 2.

This flow chart is described by the function tex2html_wrap_inline593 and the equation

displaymath546

where tex2html_wrap_inline567 corresponds to the condition n=0, tex2html_wrap_inline563 to the statement n := n - 1, and tex2html_wrap_inline565 to the statement tex2html_wrap_inline605 .

tex2html_wrap647

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

displaymath186

where

eqnarray191

and so

displaymath193

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 tex2html_wrap_inline613 which denotes the value assigned to the variable tex2html_wrap_inline615 in the state vector tex2html_wrap_inline559 , and we also introduce the function tex2html_wrap_inline619 which denotes the state vector that results when the value assigned to tex2html_wrap_inline615 in tex2html_wrap_inline559 is changed to tex2html_wrap_inline625 , and the values of the other variables are left unchanged.

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

eqnarray201

We can prove by recursion induction that

displaymath547

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

  1. tex2html_wrap_inline627
  2. tex2html_wrap_inline629
  3. tex2html_wrap_inline631

The proof parallels the previous proof that

displaymath548

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

displaymath549

where tex2html_wrap_inline633 is a conditional expression defining the function r in terms of the functions tex2html_wrap_inline637 . tex2html_wrap_inline639 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

displaymath550

In the examples, all the recursive definitions except

displaymath551

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.


next up previous
Next: Recursion Induction on Algolic Up: Towards a Mathematical Science Previous: Proving Statements About Recursive

John McCarthy
Tue May 14 13:32:03 PDT 1996