|
|
|---|
|
|
|
|---|
Recursion and Induction: Problematic Nested Recursion
Problem 124.
The following function cannot be admitted. Explain why.
(defun f5 (x)
(if (zp x)
0
(+ 1 (f5 (f5 (- x 1))))))
When the function being defined, f, is called recursively on the value of a nested recursive call, e.g., (f … (f … )), we say the definition exhibits nested recursion. We have already seen some examples of nested recursion:
(defun mcflatten (x a)
(if (consp x)
(mcflatten (car x)
(mcflatten (cdr x) a))
(cons x a)))
(defun ack (x y)
(if (zp x)
1
(if (zp y)
(if (equal x 1) 2 (+ x 2))
(ack (ack (- x 1) y) (- y 1)))))
Problem 125.
What makes the recursion in f5, which cannot be admitted,
different from that in mcflatten and ack, which can
be admitted?
It is often possible to deal with problematic nested recursion, by admitting a different but related definition and then proving that it is equivalent to the one you wanted. The next few problems illustrate this.
Problem 126.
Admit the following
(defun f5 (x)
(if (zp x)
0
(if (< (nfix (f5 (- x 1))) (nfix x))
(+ 1 (f5 (f5 (- x 1))))
'undef)))
Problem 127.
Prove
(implies (natp x) (<= (f5 x) x))
Problem 128.
Prove
(equal (f5 x)
(if (zp x)
0
(+ 1 (f5 (f5 (- x 1))))))
You may think that problematic nested recursion never arises in actual formal models. Think again! Consider a graph reachability algorithm, as might be implemented in the mark phase of a garbage collector. Suppose a memory location can hold a pair of addresses, a single address, or data. Given an initial address, mark all the reachable addresses, avoiding any possible cycles in the data. When the mark algorithm arrives at an address, ptr, containing a pair, it marks that address, explores and marks one of the addresses, and then explores and marks the other. The algorithm terminates because marking increases the number of marked addresses in memory and the number of addresses is bounded. But note that when the algorithm explores and marks the second address it does so on the memory produced by exploring and marking the first address and the parent. This is problematic nested recursion: if the inner recursion unmarked some of the marked addresses, the outer sweep might get caught in a cycle. But we cannot prove that the algorithm does not unmark things until we have admitted the model!
Problem 129.
Let m be a list representing a RAM, with 0-based addressing modeled
by nth. An address is legal if it is a natural less than the length of
the memory. If an address contains a pair, we explore both the car and
the cdr. If an address contains an address, we explore that address.
Cycles may be present.
The function below collects the list of all addresses reachable from a
given one. This definition exhibits problematic nested recursion.
(defun reachables (ptr m seen)
(if (addressp ptr m)
(if (mem ptr seen)
seen
(if (consp (nth ptr m))
(reachables (car (nth ptr m))
m
(reachables (cdr (nth ptr m))
m
(cons ptr seen)))
(reachables (nth ptr m) m (cons ptr seen))))
seen))
Use the method suggested by the f5 problems to define a function satisfying the equation above.
Problem 130.
Consider the problem of reversing a list. Our standard definition,
rev, uses an auxiliary function, app. The tail-recursive
version, rev1, uses an additional formal parameter. Below is a
definition of reverse that has only one parameter and no auxiliary functions.
This definition was proposed by Rod M. Burstall in the early 1970s as an
entertaining puzzle. It exhibits problematic nested recursion.
(defun rmb (x)
(if (consp x)
(if (consp (cdr x))
(cons (car (rmb (cdr x)))
(rmb (cons (car x)
(rmb (cdr (rmb (cdr x)))))))
(cons (car x) nil))
nil))
Show how this definition can be derived from an admissible one.
Problem 131.
Suppose rmb is known to satisfy the “defining equation”
that would be added by the defun above had it been admissible.
That is, suppose that is the only equation known for rmb.
Prove
(equal (rmb x) (rev x))
Next: