|
|
|---|
|
|
|
|---|
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 (equal (flatten! x) (flatten x)).
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 gopher and samefringe are due to John
McCarthy, who viewed gopher as a model of a co-routine. Explain what
he was thinking.
Problem 111.
Below is a model of the functional behavior of QuickSort. Note
that rel is defined as a “higher order” function that can
apply any of four relations.
(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 a is a natural
number less than the length of the memory, then a is an “address” and we
can use nth to fetch the contents. This is “dereferencing” a. If
a is not an address, we will say it is “data.” Now consider the idea of
taking an object and a memory and dereferencing until we get to data. The
following function counts the steps; it returns the symbol infinite if a
loop is detected.
(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 bit vector be a
list of Booleans; it is convenient to suppose that the least significant bit
is the car. A bit vector represents a natural number in the usual binary
encoding. Define (vadd x y) to return a bit vector representing the
sum of the numbers represented by the bit vectors x and y.
Formally specify and prove that vadd is correct.
Obviously, this problem can be expanded to include other binary arithmetic
operations and implementations.
Next: