Lab 12 Problem Set.

In this lab we will do a variety of problems intended to help get you ready for Exam 2.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Termination and Measure Functions
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

For each of the following functions, determine whether it terminates. If it
does, provide a measure function m and prove that, on every recursive call,
m applied to the arguments to that recursive call decreases, under the
conditions that lead to the recursive call. If it doesn't, provide an input
on which the function runs forever.

(defunc z (l1 l2)
  :input-contract (and (listp l1) (listp l2))
  :output-contract (listp (z l1 l2))
  (cond ((endp l1)             ())
        ((< (len l1) (len l2)) (z (cons 1 l1) (rest l2)))
        (t                     (z (rest l1) (cons 2 l2)))))

...

---------------------------------------------------------------------------

(defunc h (a b)
  :input-contract (and (integerp a) (natp b))
  :output-contract (natp (h a b))
  (cond ((> b a)     b)
        ((equal b 0) (h (- a 1) b))
        (t           (h a (+ b 1)))))

...

---------------------------------------------------------------------------

(defunc g (n)
  :input-contract (natp n)
  :output-contract t
  (cond ((equal n 0) 0)
        ((> n 3)     (+ 1 (g (- n 1))))
        (t           (- 3 (g (* 2 n))))))

...

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Induction Schemes
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Consider function bar below.

If bar is not admissible, state so, and why. In particular, if it is not
terminating, give an input on which the function runs forever.

If bar is admissible, state so without proof. Then determine the induction
scheme the function gives rise to. Write down all claims that need to be
proved in order to prove some property phi. Do not omit any claim that you
consider "trivial".

You can assume the function evenp : Integer -> Boolean returns t exactly if
its integer argument is even.

Hint: first rewrite bar such that there is no nested conditionals inside
any of the cond branches.

(defunc bar (m n)
  :input-contract (and (natp m) (natp n) (evenp n))
  :output-contract (integerp (bar m n))
  (cond ((equal m 0) -3)
        ((evenp m)   (if (> n 2)
                       10
                       (bar (/ m 2) n)))
        (t           (bar (- m 1) (+ n 2)))))

...

---------------------------------------------------------------------------

The following is an incomplete induction scheme:

(natp n) /\ (evenp n) /\ n = 0 => phi
(natp n) /\ (evenp n) /\ n >= 1 /\ phi|((n n-2)) => phi

(a) Show that it is incorrect, by providing an *invalid* formula phi that
satisfies all the given clauses.

- invalid formula phi: ...

- counterexample for phi: ...

- proof that the above two clauses are satisfied for phi: ...

(b) Now complete the induction scheme, by adding any clauses that may be
missing. The resulting scheme should be as similar to the given scheme as
possible.

- missing clauses: ...

- an admissible function that gives rise to your complete induction scheme:

...

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Induction
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

Recall the standard definitions of app and rev, and consider:

(defunc del (x l)
  :input-contract (listp l)
  :output-contract (listp (del x l))
  (cond ((endp l)            ())
        ((equal x (first l)) (del x (rest l)))
        (t                   (cons (first l) (del x (rest l))))))

del deletes all occurrences of x from l.

(a) Prove the following conjecture phi by induction.
Think about which induction scheme to use.

You may need a lemma on the way.

phi : (listp l) => (rev (del x l)) = (del x (rev l))

...

(b) Now suppose we use instead the version of del that deletes only the
*first* occurrence of x in l. Is phi still valid? If yes, just state so. If
no, give a counterexample.

...

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Tail Recursion: append
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(I am including this here since we mostly didn't get to the proof part last week.)

Here is one way to implement app using tail recursion.

Given:

(defunc app (x y)
  :input-contract (and (listp x) (listp y))
  :output-contract (listp (app x y))
  (if (endp x)
    y
    (cons (first x) (app (rest x) y))))

Consider:

(defunc app-t (y acc)
  :input-contract (and (listp y) (listp acc))
  :output-contract (listp (app-t y acc))
  (if (endp y)
    (rev* acc)
    (app-t (rest y) (cons (first y) acc))))

Notice that app-t has only one of the original arguments x,y !

(defunc app* (x y)
  :input-contract (and (listp x) (listp y))
  :output-contract (listp (app* x y))
  (app-t y (rev* x)))

Here is a lemma relating app-t and app:

phi :: (listp y) /\ (listp acc) => (app-t y acc) = (app (rev acc) y)

Exercise 1: prove the following conjecture, assuming phi is true:

(listp x) /\ (listp y) => (app* x y) = (app x y)

...

Exercise 2: prove phi, using the IS of app-t.

...