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

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

(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,

(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

(equal (rmb x) (rev x))

Next: