Next: Relation to Other Formalisms Up: Properties of Computable Functions Previous: Formal Properties of Conditional

## Recursion Induction

Suppose a function f is defined recursively by

(1) { }

where is an expression that in general contains f. Suppose that is the set of n-tuples for which f is defined. Now let g and h be two other functions with the same domain as f and which are defined for all n-tuples in . Suppose further that g and h satisfy the equation which defined f. We assert that

for all in . This is so, simply because equation (1) uniquely determines the value that any function satisfying it has for arguments in which in turn follows from the fact that (1) can be used to compute for in .

We shall call this method of proving two functions equivalent by the name of recursion induction.

We shall develop some of the properties of the elementary functions of integers in order to illustrate proof by recursion induction. We recall the definitions

Only the definition of addition and the properties of conditional expressions were used in this proof.

Proof Define . It is easily seen that f(m,n) converges for all m and n and hence is completely defined by the above equation and is computable from it. Now

It is easily seen that the functions g and h defined by the equations g(m,n) =(m + n)' and h(m,n) = m' + n both satisfy the equation f. For example, it is clear that and Therefore, by the principle of recursion induction h and g are equivalent functions on the domain of where f is defined, but this is the set of all pairs of integers.

The fact that the above defined f(m,n) converges for all m and n is a case of the more general fact that all functions defined by equations of the form

converge. We are not yet able to discuss formal proofs of convergence.

In presenting further proofs we shall be more terse.

Proof Let Again f converges for all m, n, p. We have

Each of these forms satisfies the equation for f(m,n,p).

Setting m = 0 in Theorem 3 gives

so that if we had 0 + m = m we would have commutativity of addition.

In fact, we cannot prove 0 + m = m without making some assumptions that take into account that we are dealing with the integers. For suppose our space consisted of the vertices of the binary tree in figure 2, where #1#2#3#4#5@font#1#2pt#3#4#5

Fig. 2

m' is the vertex just above and to the left, and is the vertex just below, and 0 is the bottom of the tree. m + n can be defined as above and of course satisfies Theorems 1, 2, and 3 but does not satisfy 0+m = m. For example, in the diagram 0 + a = b although a + 0 = a.

We shall make the following assumptions:

1.

2.

3.

which embody all of Peano's axioms except the induction axiom.

Proof By 3 and 4 as remarked above.

Now we shall give some examples of the application of recursion induction to proving theorems about functions of symbolic expressions. The rest of these proofs depend on an acquaintance with the Lisp formalism.

Let us define the concatenation of two lists x and y by the formula

Our first objective is to show that concatenation is associative.

Th. 11.

Proof

We shall show that and satisfy the functional equation

First we establish an auxiliary result:

Now we write

and

From these results it is obvious that both and satisfy the functional equation.

Let

NIL satisfies this equation. We can also write for any list x

which also satisfies the equation.

Next we consider the function reverse[x] defined by

It is not difficult to prove by recursion induction that

and

Many other elementary results in the elementary theory of numbers and in the elementary theory of symbolic expressions are provable in the same straightforward way as the above. In number theory one gets as far as the theorem that if a prime p divides ab, then it divides either a or b. However, to formulate the unique factorization theorem requires a notation for dealing with sets of integers. Wilson's theorem, a moderately deep result, can be expressed in this formalism but apparently cannot be proved by recursion induction.

One of the most immediate problems in extending this theory is to develop better techniques for proving that a recursively defined function converges. We hope to find some based on ambiguous functions. However, Godel's theorem disallows any hope that a complete set of such rules can be formed.

The relevance to a theory of computation of this excursion into number theory is that the theory illustrates in a simple form mathematical problems involved in developing rules for proving the equivalence of algorithms. Recursion induction, which was discovered by considering number theoretic problems, turns out to be applicable without change to functions of symbolic expressions.

Next: Relation to Other Formalisms Up: Properties of Computable Functions Previous: Formal Properties of Conditional

John McCarthy
Wed May 1 17:18:52 PDT 1996