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
displaymath1819
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
displaymath1833
displaymath1835
Only the definition of addition and the properties of conditional expressions
were used in this proof.
tex2html_wrap_inline1837
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.
tex2html_wrap_inline1875
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
displaymath1887
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.
tex2html_wrap_inline1911
tex2html_wrap_inline1913
Proof By 3 and 4 as remarked above.
tex2html_wrap_inline1915
tex2html_wrap_inline1917
tex2html_wrap_inline1919
tex2html_wrap_inline1921
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
displaymath1929
Our first objective is to show that concatenation is associative.
Th. 11. tex2html_wrap_inline1933
Proof
We shall show that tex2html_wrap_inline1935 and tex2html_wrap_inline1937 satisfy the functional equation
displaymath1939
First we establish an auxiliary result:
displaymath1941
Now we write
and
displaymath1943
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
displaymath1957
It is not difficult to prove by recursion induction that
displaymath1959
and
displaymath1961
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.
