next up previous
Next: Recursive FunctionsFlow Charts, Up: Towards a Mathematical Science Previous: Using Conditional Expressions to

Proving Statements About Recursive Functions

In the previous section we presented a formalism for describing functions which are computable in terms of given base functions. We would like to have a mathematical theory strong enough to admit proofs of those facts about computing procedures that one ordinarily needs to show that computer programs meet their specifications. In [McC63] we showed that our formalism for expressing computable functions, was strong enough so that all the partial recursive functions of integers could be obtained from the successor function and equality. Now we would like a theory strong enough so that the addition of some form of Peano's axioms would allow the proof of all the theorems of one of the forms of elementary number theory.

We do not yet have such a theory. The difficulty is to keep the axioms and rules of inference of the theory free of the integers or other special domain, just as we have succeeded in doing with the formalism for constructing functions.

We shall now list the tools we have so far for proving relations between recursive functions. They are discussed in more detail in [McC63].

1. Substitution of expressions for free variables in equations and other relations.

2. Replacement of a sub-expression in a relation by an expression which has been proved equal to the sub-expression. (This is known in elementary mathematics as substitution of equals for equals.) When we are dealing with conditional expressions, a stronger form of this rule than the usual one is valid. Suppose we have an expression of the form


and we wish to replace b by d. Under these circumstances we do not have to prove the equation b = d in general, but only the weaker statement


This is because b affects the value of the conditional expression only in case tex2html_wrap_inline495 is true.

3. Conditional expressions satisfy a number of identities, and a complete theory of conditional expressions, very similar to propositional calculus, is thoroughly treated in [McC63]. We shall list a few of the identities taken as axioms here.

  1. tex2html_wrap_inline497
  2. tex2html_wrap_inline499
  3. tex2html_wrap_inline501
  4. tex2html_wrap_inline503

4. Finally, we have a rule called recursion induction for making arguments that in the usual formulations are made by mathematical induction. This rule may be regarded as taking one of the theorems of recursive function theory and giving it the status of a rule of inference. Recursion induction may be described as follows:

Suppose we have a recursion equation defining a function f, namely


where the right hand side will be a conditional expression in all non-trivial cases, and suppose that

  1. the calculation of tex2html_wrap_inline507 according to this rule converges for a certain set A of n-tuples,
  2. the functions tex2html_wrap_inline511 and tex2html_wrap_inline513 each satisfy equation (1) when g or h is substituted for f. Then we may conclude that tex2html_wrap_inline521 for all n-tuples tex2html_wrap_inline525 in the set A.

As an example of the use of recursion induction we shall prove that the function g defined by


satisfies tex2html_wrap_inline529 given the usual facts about n!. We shall take for granted the fact that g(n, s) converges for all non-negative integral n and s. Then we need only show that tex2html_wrap_inline539 satisfies the equation for g(n, s). We have


and this has the same form as the equation satisfied by g(n, s). The steps in this derivation are fairly obvious but also follow from the above-mentioned axioms and rules of inference. In particular, the extended rule of replacement is used. A number of additional examples of proof by recursion induction are given in [McC63], and it has been used to prove some fairly complicated relations between computable functions.

next up previous
Next: Recursive FunctionsFlow Charts, Up: Towards a Mathematical Science Previous: Using Conditional Expressions to

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