Recursion and Induction: More Problems

**Problem 106. ** Here is a way to flatten a binary tree without using
an auxiliary function. Admit this definition.

(defun flatten! (x) (if (atom x) (cons x nil) (if (atom (car x)) (cons (car x) (flatten! (cdr x))) (flatten! (cons (caar x) (cons (cdar x) (cdr x)))))))

**Problem 107. ** Prove

**Problem 108. ** Here is a clever way to determine if two binary trees have the
same fringe. Admit this function (and its subroutine).

(defun samefringe (x y) (if (or (atom x) (atom y)) (equal x y) (and (equal (car (gopher x)) (car (gopher y))) (samefringe (cdr (gopher x)) (cdr (gopher y))))))

where

(defun gopher (x) (if (or (atom x) (atom (car x))) x (gopher (cons (caar x) (cons (cdar x) (cdr x))))))

**Problem 109. ** Prove

(equal (samefringe x y) (equal (flatten x) (flatten y)))

**Problem 110. ** The curious recursions in

**Problem 111. ** Below is a model of the functional behavior of QuickSort. Note
that

(defun rel (fn x y) (if (equal fn '<<=) (<<= x y) (if (equal fn '>>=) (<<= y x) (if (equal fn '<<) (and (<<= x y) (not (equal x y))) (and (<<= y x) (not (equal x y))))))) (defun filter (fn x e) (if (endp x) nil (if (rel fn (car x) e) (cons (car x) (filter fn (cdr x) e)) (filter fn (cdr x) e)))) (defun qsort (x) (if (endp x) nil (if (endp (cdr x)) x (app (qsort (filter '<< (cdr x) (car x))) (cons (car x) (qsort (filter '>>= (cdr x) (car x))))))))

Prove that `qsort` produces an ordered permutation of its
input.

**Problem 112. ** Prove that the length of a list of distinct natural numbers
is no greater than its maximum element plus one. This is sometimes
called the Pigeon Hole Principle.

**Problem 113. ** Imagine a simple list being treated as a “memory.” If

(defun deref-cnt (ptr mem seen) (if (addressp ptr mem) (if (mem ptr seen) 'infinite (inc (deref-cnt (nth ptr mem) mem (cons ptr seen)))) 0))

where

(defun len (x) (if (consp x) (+ 1 (len (cdr x))) 0)) (defun inc (x) (if (integerp x) (+ 1 x) 'infinite)) (defun addressp (ptr m) (and (natp ptr) (< ptr (len m))))

Admit `deref-cnt`.

**Problem 114. ** This is a fact every undergraduate knows. The number of times you can
dereference (without being in a loop) is bounded by the size of the memory
(plus one for the initial probe). Prove it.

(<= (deref-cnt ptr mem nil) (+ 1 (len mem)))

Since `deref-cnt` returns the non-number `infinite` if it
is a loop, and since ACL2 arithmetic treats non-numbers as `0`,
this theorem is trivial when the process loops. You may therefore
explicitly add the hypothesis `(integerp (deref-cnt ptr mem nil))`
if you are uncomfortable dealing with the non-numeric defaults.

**Problem 115. ** Here is the familiar definition of the Fibonacci function
and a more efficient one (“fast Fibonacci”).

(defun fib (i) (if (zp i) 0 (if (equal i 1) 1 (+ (fib (- i 1)) (fib (- i 2)))))) (defun ffib (i j k) (if (zp i) j (if (equal i 1) k (ffib (- i 1) k (+ j k)))))

Prove they are equal in the following sense

(equal (ffib n 0 1) (fib n))

**Problem 116. ** Prove

(equal (rotn (len x) x) x)

where

(defun rot (x) (if (endp x) nil (app (cdr x) (cons (car x) nil)))) (defun rotn (n x) (if (zp n) x (rotn (- n 1) (rot x))))

**Problem 117. ** In this problem we explore binary arithmetic. Let a

Next: