Recursion and Induction: More Problems
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)))))))
Prove (equal (flatten! x) (flatten x)).
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))))))
(defun gopher (x) (if (or (atom x) (atom (car x))) x (gopher (cons (caar x) (cons (cdar x) (cdr x))))))
(equal (samefringe x y) (equal (flatten x) (flatten y)))
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.
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.
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.
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))
(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))))
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.
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))
(equal (rotn (len x) x) x)
(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))))
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.