|
|
|---|
|
|
|
|---|
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 IFs and the substitution built from each recursive call, whereas the Induction Principle talks about the tests in the ith formula and the substitution that created the jth induction hypothesis of the ith 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 (and (not (and (test1 x a) (test2 x a))) (not (and (test1 x a) (not (test2 x a))))), but that is propositionally equivalent to (not (test1 x a)).)
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: