next up previous
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) tex2html_wrap_inline1785 { tex2html_wrap_inline1787 }

where tex2html_wrap_inline1789 is an expression that in general contains f. Suppose that tex2html_wrap_inline1793 is the set of n-tuples tex2html_wrap_inline1797 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 tex2html_wrap_inline1793 . Suppose further that g and h satisfy the equation which defined f. We assert that


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

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 tex2html_wrap_inline1841 . 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 tex2html_wrap_inline1859 and tex2html_wrap_inline1861 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 tex2html_wrap_inline1877 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


Fig. 2

m' is the vertex just above and to the left, and tex2html_wrap_inline1895 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. tex2html_wrap_inline1905

2. tex2html_wrap_inline1907

3. tex2html_wrap_inline1909

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.

We start with the basic identities.


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


Our first objective is to show that concatenation is associative.

Th. 11. tex2html_wrap_inline1933


We shall show that tex2html_wrap_inline1935 and tex2html_wrap_inline1937 satisfy the functional equation


First we establish an auxiliary result:


Now we write




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


Let tex2html_wrap_inline1949

tex2html_wrap_inline1951 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




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 up previous
Next: Relation to Other Formalisms Up: Properties of Computable Functions Previous: Formal Properties of Conditional

John McCarthy
Wed May 1 20:03:21 PDT 1996