Recursion and Induction: Relations Between Recursion and Induction

Informally speaking, a recursive definition is “ok” if there is an ordinal measure that decreases in every recursive call. Thus, the recursion cannot go on forever. In a simple recursion on naturals down to 0 by -1, the value of the function on 5 is determined recursively by its value on 4, which is determined recursively by its value on 3, which is determined recursively by its value on 2, which is determined recursively by its value on 1, which is determined recursively by its value on 0, which is specified explicitly in the definition.

An inductive proof is “ok” if there is an ordinal measure that decreases in every induction hypothesis. Thus, any concrete instance of the conjecture could be proved by “pumping” forward a finite number of times from the base cases. Given a simple inductive proof over the naturals, the conjecture is true on 0 because it was proved explicitly in the base case, so it is true on 1 by the induction step, so it is true on 2 by the induction step, so it is true on 3 by the induction step, so it is true on 4 by the induction step, so it is true on 5 by the induction step.

Clearly these two concepts are duals. The formal statements of the two
principles look more different than they are. They both require us to prove
that a measure returns an ordinal and that some substitutions make the
measure decrease under some tests. But there seems to be a lot less indexing
going on in the Definitional Principle than in the Induction Principle. That
is due to language and the two different uses of the principles. The
Definitional Principle is designed to tell us whether a definitional equation
is ok. The Induction Principle is designed to tell us whether a set of
formulas is an ok inductive argument. So the Definitional Principle talks
about the tests in `IF`s and the substitution built from each recursive
call, whereas the Induction Principle talks about the tests in the *i*th
formula and the substitution that created the *j*th induction hypothesis
of the *i*th formula.

But the key insight is: *Every ok definition suggests an ok induction*!
We call this the induction *suggested by* the definition. It is easiest
to see this by considering a particular, generic definition and thinking
about what had to be proved to admit it, what induction it suggests,
what has to be proved for that induction to be legal, and when the suggested
induction might be useful.

Suppose the following definition has been admitted, justified by measure term
`(m x a)`. Note that the body is an `IF`-tree, and there are three tips in
the `IF`-tree; the first tip contains two recursive calls, the second tip
contains one recursive call, and the third tip contains no recursive calls.

(defun f (x a) (if (test1 x a) (if (test2 x a) (h ; tip 1 (f (d1 x a) (a1 x a)) ; rec call 1,1 (f (d2 x a) (a2 x a))) ; rec call 1,2 (g ; tip 2 (f (d3 x a) (a3 x a)))) ; rec call 2,1 (b x a))) ; tip 3

To admit this definition we had to prove:

Ordinal Conjecture(o-p (m x a))Measure Conjecture 1,1(implies (and (test1 x a) (test2 x a)) (o< (m (d1 x a) (a1 x a)) (m x a)))Measure Conjecture 1,2(implies (and (test1 x a) (test2 x a)) (o< (m (d2 x a) (a2 x a)) (m x a)))Measure Conjecture 2,1(implies (and (test1 x a) (not (test2 x a))) (o< (m (d3 x a) (a3 x a)) (m x a)))

Suppose we want to prove `(p x a)`, by induction according to
the scheme “suggested” by `(f x a)`. Here is the scheme:

Base Case; for tip 3 (implies (not (test1 x a)) (p x a))Induction Step 1; for tip 1 (implies (and (test1 x a) (test2 x a) (p (d1 x a) (a1 x a)) ; for rec call 1,1 (p (d2 x a) (a2 x a))) ; for rec call 1,2 (p x a))Induction Step 2; for tip 2 (implies (and (test1 x a) (not (test2 x a)) (p (d3 x a) (a3 x a))) ; for rec call 2,1 (p x a))

This induction is produced by the following parameter choices in the Induction Principle:

ψ |
(p x a) |

m |
(m x a) |

q_1 |
(and (test1 x a) (test2 x a)) |

q_2 |
(and (test1 x a) (not (test2 x a))) |

σ_{1,1} |
{x ← (d1 x a), a ← (a1 x a)} |

σ_{1,2} |
{x ← (d2 x a), a ← (a2 x a)} |

σ_{2,1} |
{x ← (d3 x a), a ← (a3 x a)} |

It should be obvious to you how these choices are determined from the
definition of `f` with measure `(m x a)`. For example, *q_1* is
the conjunction of the tests leading to the first tip containing recursive
calls of `f`, and the substitutions *σ_{1,j}* are the
substitutions derived from the recursive calls in that tip.

The measure conjectures required by the Induction Principle for this
choice of parameters are exactly
the same as the measure conjectures verified when the Definitional Principle
was used to admit `f`!
That is, to use an induction suggested by an
already-admitted recursive function, no additional measure conjectures have to be proved.

(Remark on ``exactly the same'' above. We have propositionally simplified
the defining condition for the Base Case. The Induction Principle says it is
`(and (not q_1) (not q_2))` and the literal instantiation
of that here would be

But why might this induction be interesting or useful for proving `(p x
a)`? The answer depends on `(p x a)`, of course. But the most
common situation is that we choose the induction scheme suggested by some
recursive function used in the conjecture to be proved. So suppose `(f
x a)` occurs in `(p x a)`. Why is the suggested induction likely
to be helpful? Consider the Base Case and the two Induction Steps.

In the Base Case, the `(f x a)` occurring in `(p x a)` can be
replaced by tip 3 of the definition of `f`, `(b x a)` because the
test in the Base Case of the induction is the test leading to the
non-recursive exit from the definition. So `f` has been eliminated
from the proof of the Base Case.

Now consider Induction Step 1. The `(f x a)` occurring in `(p x a)`
can be replaced by tip 1 of the definition of `f`, namely

(h ; tip 1 (f (d1 x a) (a1 x a)) ; rec call 1,1 (f (d2 x a) (a2 x a))) ; rec call 1,2

because the tests in Induction Step 1 are the tests leading to tip 1 of the definition.
But notice that the induction hypothesis labeled “for rec call 1,1” in
Induction Step 1 gives us a hypothesis about recursive call 1,1 — because
the occurrence of `(f x a)` in `(p x a)` becomes an occurrence of
`(f (d1 x a) (a1 x a))` when we apply the substitution *σ_{1,1}*
to it. Similarly, the induction hypothesis labeled “for rec call 1,2”
gives us a hypothesis about call 1,2. Thus, the proof of Induction Step 1
boils down to proving, “if the two recursive calls in this tip have the
property we're proving, then `h` of those two calls has the
property.” While not exactly eliminating `f` from the proof, it
provides us with all the information that we have a right to suppose about
`f` in this case. Usually the proof of this step requires a lemma
about `p` and `h`, e.g., “if `a` and `b` have
property `p`, then so does `(h a b)`.” Such a lemma would
eliminate `f`, and if we had that lemma the proof of Induction Step 1
would be done. The proof of Induction Step 2 is analogous.

Thus, we see that there may well be some heuristic value in using the
induction suggested by `(f x a)` whenever you are trying to prove a
property of `(f x a)`. Occasionally it is necessary to use an
induction suggested by a function not appearing in the conjecture, but when
that occurs it is usually some easily recognized “mash up” of other
functions appearing in the conjecture.

**Problem 102. ** Recall the previously admitted

(defun f1 (i j) (if (and (natp i) (natp j) (< i j)) (f1 (+ 1 i) j) 1))

Prove `(equal (f1 i j) 1)`.

**Problem 103. ** Recall the previously admitted

(defun f2 (x) (if (equal x nil) 2 (and (f2 (car x)) (f2 (cdr x)))))

Prove `(equal (f2 x) 2)`.

**Problem 104. ** Recall the previously admitted

(defun f3 (x y) (if (and (endp x) (endp y)) 3 (f3 (cdr x) (cdr y))))

Prove `(equal (f3 x y) 3)`.

**Problem 105. ** Recall the previously admitted

(defun f4 (x y q) (if (p x) (if q (f4 y (dn x) (not q)) (f4 y (up x) (not q))) 4))

Prove `(equal (f4 x y q) 4)`.

These simple inductive exercises drive home the point that once a function
has been admitted (proved to terminate) then we can do inductions to
“unwind” it. Students so frequently see induction limited to “*p(n)*
implies *p(n+1)* ” that it is easy to forget that every total recursive
function gives rise to an induction that is appropriate for it.

Next: