#| CS 2800 Homework 8 - Fall 2017


This homework is to be done in a group of 2-3 students.

If your group does not already exist:

 * One group member will create a group in BlackBoard
 
 * Other group members then join the group
 
 Submitting:
 
 * Homework is submitted by one group member. Therefore make sure the person
   submitting actually does so. In previous terms when everyone needed
   to submit we regularly had one person forget but the other submissions
   meant the team did not get a zero. Now if you forget, your team gets 0.
   - It wouldn't be a bad idea for group members to send confirmation
     emails to each other to reduce anxiety.

 * Submit the homework file (this file) on Blackboard.  Do not rename
   this file.  There will be a 10 point penalty for this.

 * You must list the names of ALL group members below, using the given
   format. This way we can confirm group membership with the BB groups.
   If you fail to follow these instructions, it costs us time and
   it will cost you points, so please read carefully.


Names of ALL group members: FirstName1 LastName1, FirstName2 LastName2, ...

Note: There will be a 10 pt penalty if your names do not follow
this format.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

For this homework you will NOT need to use ACL2s, though you can use it as
a text editor to typeset your solution.

Technical instructions:

- open this file as hw08.lisp

- insert your solutions into this file where indicated (usually as "...")

- when done, save your file and submit it as hw08.lisp

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; I. ADMISSIBILITY
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
For each of the definitions below, check whether it is admissible, i.e. it
satisfies all rules of the definitional principle. You can assume that Rule
1 is met: the symbol used in the defunc is a new function symbol in each
case.

If you claim admissibility,

1. Explain in English why the body contracts hold.
2. Explain in English why the contract theorem holds.
3. Suggest a measure function that can be used to show termination.
   (You DO NOT have to prove the measure function properties in this problem.)

Otherwise, identify a rule in the Definitional Principle that is violated.

If you blame one of the purely syntactic rules (variable names,
non-wellformed body etc), explain the violation in English.

If you blame one of the semantic rules (body contract, contract theorem or
termination), you must provide an input that satisfies the input contract, but
causes a violation in the body or violates the output contract or causes
non-termination.

Remember that the rules are not independent: if you claim the function does
not terminate, you must provide an input on which the function runs forever
*without* causing a body contract violation: a body contract violation is
not a counterexample to termination. Similarly, if you claim the function
fails the contract theorem, you must provide an input on which it
terminates and produces a value, which then violates the output contract.

Assume that these functions are being given to ACL2s in sequence. If a
function is not admitted by ACL2s, you delete that function and begin to
write the next one.
|#
#|
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
1.
(defunc f1 (a b)
  :input-contract  (and (posp a) (posp b))
  :output-contract (posp (f1 a b))
  (cond ((or (equal a 1) (equal b 1)) 1)
        ((< a b)                       (f1 (- a 1) b))
        (t                             (f1 b a))))

;No: Does not terminate on, for example (f1 3 3)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2.
(defunc f2 (x n)
  :input-contract (and (listp x) (posp n))
  :output-contract (listp (f2 x n))
  (if (equal n 0)
    (list n)
    (f2 (cons (list (first x)) (rest x)) (- n 1))))

;No: Violates input contract of first/rest on (f2 nil 1)
; or on (f2 '(1 2 3) 1) (contract violation for f2)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3.
(defunc f3 (x)
  :input-contract (natp x)
  :output-contract (integerp (f3 x))
  (if (equal x 1)
    0
    (+ 2 (f3 (- x 1)))))

;No: Does not terminate on (f3 0)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
4.
(defunc f4 (x y)
  :input-contract (and (listp x) (posp y))
  :output-contract (listp (f4 x y))
  (if (equal y 1)
    nil
    (f4 (list (first x)) (- y 1))))

;No: Contract violation on first if x is nil, and y<>1, e.g., (f4 nil 4)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
5.
(defunc f5 (l)
  :input-contract (listp l)
  :output-contract (listp (f5 l))
  (if (endp l)
    nil
    (f5 (rest f))))

;No: f is an undefined variable in (rest f)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
6.
(defunc f6 (z y z)
  :input-contract (and (posp z) (listp y) (posp z))
  :output-contract (posp (f6 z y z))
  (if (endp y)
    0
    (f6 z (rest y) z)))

;No: The formal argument z appears twice
; Notice this is NOT a contract violation despite returning 0.
; The redundant variable name is found first.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
7.
(defunc f7 (x y)
  :input-contract (and (integerp x) (integerp y))
  :output-contract (integerp (f7 x y))
  (if (equal x 0)
    0
    (+ (* 2 y) (f7 (- x 1) y))))

;No: Does not terminate, e.g., on (f7 -1 0)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
8.
(defunc f8 (x y)
  :input-contract (and (listp x) (listp y))
  :output-contract (posp (f8 x y))
  (if (endp x)
    (len y)
    (f8 (rest x) y)))

;No: (f8 nil nil) = 0 and violates the output contract

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
9.
(defunc f9 (x)
  :input-contract (posp x)
  :output-contract (integerp (f9 x))
  (if (equal x 1)
    1
    (- 10 (f9 (- x 2)))))

;No: Contract violation for call to f9. Counterexample: (f9 2)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
10.
(defunc f10 (x)
  :input-contract (posp x)
  :output-contract (integerp (f10 x))
  (if (equal x 1)
    4
    (- (f10 (- x 1) 1) 2)))

;No: Wrong number of arguments for f10

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
11.
(defunc f11 (x)
  :input-contract (posp x)
  :output-contract (natp (f11 x))
  (if (equal x 1)
      1
    (f11 (+ 1 (f11 (- x 1))))))

;No: Does not terminate, e.g., on (f11 2)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
12.
(defunc f12 (x)
  :input-contract (listp x)
  :output-contract (natp (f12 x))
  (cond ((endp z)  0)
        (t         (f12 (rev x)))))

;No: Free variable z

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
13.
(defunc f13 (x)
  :input-contract (listp x)
  :output-contract (listp (f13 x))
  (cond ((endp x)  x)
        (t         (cons x (f12 (rev x))))))
        
;; No. F12 (if we consider it to be defined) outputs a nat and thus the
;; contract axiom would fail since f13 wouldn't output a list. If f12
;; is not defined (both answers are right) then there is a syntax error
;; in the second condition since function symbol f12 is undefined.
|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; II. GUESSING A MEASURE
;; For each of the following functions, determine if the function terminates.
;; If it does not, give an input on which it doesn't terminate. If it does
;; terminate, write THE SIMPLEST measure function you can - you DO NOT need 
;; to prove that it is a measure - just write one that satisfies all 
;; requirements of a measure function.
;; Simplest will mean the measure function body with the fewest function calls.
;; Also, please ignore the fact all the functions are named f.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
1.
(defunc f (x y)
  :input-contract (and (posp x) (posp y))
  :output-contract (integerp (f x y))
  (cond (((equal x 1) 10)
        (< x 1)     (f x y))
        (t           (+ 2 (f (- x 1) y)))))

Yes: Measure is
(defunc f (x y)
  :input-contract (and (posp x) (posp y))
  :output-contract (integerp (f x y))
  x)
  
; Notice that x-1 or x+17 (for example) could be used BUT it isn't 
; as simple as possible.

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
2.
(defunc f (x y)
  :input-contract (and (listp x) (posp y))
  :output-contract (posp (f x y))
  (if (endp x)
    y
    (+ 1 (f (rest x) y))))

Yes: Measure is
(defunc f (x y)
  :input-contract (and (listp x) (posp y))
  :output-contract (posp (f x y))
  (len x))

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
3.
(defunc f (x y)
  :input-contract (and (listp x) (posp y))
  :output-contract (listp (f x y))
  (cond ((endp x)    (list y))
        ((equal y 1) nil)   
        (t           (f (cons (+ y 1) x) (- y 1)))))

Yes: Measure is
(defunc f (x y)
  :input-contract (and (listp x) (posp y))
  :output-contract (listp (f x y))
  y)
  
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
4.
(defunc f (x y)
  :input-contract (and (listp x) (posp y))
  :output-contract (natp (f x y))
  (if (equal y (len x))
    y
    (if (< (len x) y)
      (f x (- y (len x)))
      (f (rest x) y))))

No: Does not terminate for (f nil 1).

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
5.
(defunc f (x)
  :input-contract (lonp x)
  :output-contract (natp (f x))
  (if (endp x)
    (f (cons 10 x))
    (if (equal (first x) 0)
      0
      (f (cons (- (first x) 1) x)))))

Yes: Measure is
(defunc f (x)
  :input-contract (lonp x)
  :output-contract (natp (f x))
  (if (endp x)
    11
    (first x)))
|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; III. PROVING A MEASURE
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|

For the following problems, whenever you are asked to prove termination of
some function f, provide a measure function m such that

Condition 1. m has the same arguments and the same input contract as f.
Condition 2. m's output contract is (natp (m ...))
Condition 3. m is admissible.
Condition 4. On every recursive call of f, given the input contract and
   the conditions that lead to that call, m applied to the arguments in
   the call is less than m applied to the original inputs.

You should do this proof as shown in class (which is also the way we will
expect you to prove termination in exams):

- Write down the formalization of condition 4 (above).
- Simplify the formula (if possible).
- Use equational reasoning to conclude the formula is valid.

Unless clearly stated otherwise, you need to follow these steps for EACH
recursive call separately.

Here is an example.

(defunc f (x y)
  :input-contract (and (listp x) (natp y))
  :output-contract (natp (f x y))
  (if (endp x)
    (cond ((equal y 0) 0)
          (t           (+ 1 (f x (- y 1)))))
    (+ 1 (f (rest x) y))))

The measure is

(defunc m (x y)
  :input-contract (and (listp x) (natp y))
  :output-contract (natp (m x y))
  (+ (len x) y))

Formalization of condition 4 (above) for the first recursive call:
(implies (and (listp x) (natp y) (endp x) (> y 0)) (< (m x (y-1)) (m x y)))
Proof of Condition 4 for the first recursive call:
Context:
C1. (listp x)
C2. (natp y)
C3. (endp x)
C4. y > 0

(m x y-1)
= { Def m, C3, Arithmetic }
y-1
< { Arithmetic }
y
= { Def m, C3, Arithmetic }
(m x y)

QED

Formalization of condition 4 (above) for the second recursive call:
(implies (and (listp x) (natp y) (not (endp x))) (< (m (rest x) y) (m x y)))
Proof of Condition 4 for the second recursive call:
Context:
C1. (listp x)
C2. (natp y)
C3. (not (endp x))

(m (rest x) y)
= { Def m, C3, len theorem for rest }
(len x) - 1 + y
< { Arithmetic }
(len x) + y
= { Def m }
(m x y)

QED

(defdata lor (listof rational))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; 1. Prove termination for the following function:

(defunc foo1 (l2 l1)
  :input-contract (and (lorp l2) (lorp l1))
  :output-contract (lorp (foo1 l2 l1))
  (cond ((endp l1)   l2)
        ((endp l2)   (foo1 (rest l1) nil))
        (t          (foo1 (cons (first l1) l2) (rest l1) ))))

Provide a measure function
(defunc m (l2 l1)
  :input-contract (and (lorp l2) (lorp l1))
  :output-contract (natp (m l2 l1))
  (len l1))

And then prove that it is indeed a measure function.

;PART OF SOLUTION:
The proof obligations are:
(lorp l1)/\(lorp l2)/\~(endp l1)/\(endp l2) => (m l2 l1) > (m (rest l1) nil)
and
(lorp l1)/\(lorp l2)/\~(endp l1)/\~(endp l2) => (m l2 l1) > (m (cons (first l1) l2) (rest l1))

Proof of Condition 4 for the first recursive call:
Context:
C1. (lorp l1)
C2. (lorp l2)
C3. (not (endp l1))
C4. (endp l2)
?
Proof:
(m (rest l1) nil)
= { Def m, Def len, C1 }
0
< { C1, C3, Def len }
(len l1)
= { Def m, C4, C1, C2 }
(m l1 l2)

Proof of Condition 4 for the second recursive call:
Context:
C1. (lorp l1)
C2. (lorp l2)
C3. (not (endp l1))
C4. (not (endp l2))
Proof:
(m (rest l1) (cons (first l1) l2))
= { Def m, len. of rest }
(len l1) - 1
< { Arithmetic }
(len l1)
= { Def m }
(m l1 l2)


;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;2. Prove termination for the following function.

(defunc foo2 (p v)
  :input-contract (and (posp p) (posp v))
  :output-contract (posp (foo2 p v))
  (cond ((< p v)     (foo2 p (- v p)))
        ((> p v)     (foo2 (- p v) v))
        (t           (+ (* p 2) (+ 3 v)))))

Define a measure function m for foo2 and prove using equation reasoning that
It is indeed a measure.
;PART OF SOLUTION:
(defunc m (p v)
  :input-contract (and (posp p) (posp v))
  :output-contract (natp (m p v))
  (+ p v))

The formalization for Condition 4 (above).

For the first recursive call, we have:
(implies (and (posp p) (posp v) (< p v))
         (< (m p (- v p)) (m p v)))

which is the same as:
(implies (and (posp p) (posp v) (< p v))
         (< (+ p (- v p)) (+ p v)))

 
For the second recursive call, we have:
(implies (and (posp p) (posp v) (not (< p v)) (> p v))
         (< (m (- p v) v) (m p v)))

which is the same as:
(implies (and (posp p) (posp v) (not (< p v)) (> p v))
         (< (+ (- p v) v) (+ p v)))

Now prove the above two using equational reasoning
 
;PART OF SOLUTION:         
For Condition 4 of the first recursive call:
Context:
C1. (posp p)
C2. (posp v)
C3. p < v
Proof:
(m p v-p)
= { Def m, C1, C2 }
p+v-p
= { Arithmetic }
v
< { Arithmetic, C1 }
p+v
= { Def m, C1, C2 }
(m p v)

QED

Proof of Condition 4 for the second recursive call:
Context:
C1. (posp p)
C2. (posp v)
C3. p > v

(m p-v v)
= { Def m, C1, C2 }
p-v+v
= { Arithmetic }
p
< { Arithmetic, C2 }
p+v
= { Def m, C1, C2 }
(m p v)

QED
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;3. Prove termination for the following function:
 
(defunc foo3 (x1 x2)
  :input-contract (and (listp x1) (integerp x2))
  :output-contract (natp (foo3 x1 x2))
  (cond ((and (endp x1) (equal x2 0)) (+ 1 (len x1)))
        ((and (endp x1) (> x2 0))     (+ 1 (foo3 x1 (- x2 1))))
        ((endp x1)                   (+ 1 (foo3 x1 (+ 1 x2))))
        (t                          (+ 1 (foo3 (rest x1) (- 0 x2))))))

; Define a measure function m for foo3.
#|Hint: Note that you can start by writing candidate measures for each branch
above that has a recursive call. However, you might be finally able to
combine some/all of these measures to come up with one that works in all
the 3 relevant cases above.  

Also, feel free to use any (terminating) function  we've defined in the past 
in your measure function. 
|#
;Then prove that the above defined function m is indeed a measure for foo3.

;PART OF SOLUTION:
(defunc m (x1 x2)
  :input-contract (and (listp x1) (integerp x2))
  :output-contract (natp (m x1 x2))
  (+ (len x1) (abs x2)))

Proof of Condition 4 for the first recursive call
There are two cases in function foo3 since x2 might be 1 but 
by using the above measure function, the value resolves to the same thing.
This is why it's not always easier to use if statements.
Context:
C1. (listp x1)
C2. (integerp x2)
C3. (endp x1)
C4. (not (and (endp x1)(equal x2 0)))
C5. (> x2 0)

Proof:
(m x1 x2-1)
= { Def m, C1, C2, C3, C5}
0+x2-1
< { Arithmetic }
x2
= { Def m, C1, C2, C3, C5 }
(m x1 x2)

Proof of Condition 4 for the second recursive call:
Context:
C1. (listp x1)
C2. (integerp x2)
C3. (endp x1)
C4. (not (and (endp x1)(equal x2 0)))
C5. (not (and (endp x1)(> x2 0))) {You can simplify in advance but this was left 
                                  for illustrative purposes}
------------------------------
C6. (not (> x2 0)) {PL, C5, C3}
C7. (not (equal x2 0)) {PL C4, C3}
C8. (< x2 0) {C7, C6, C2, Arithmetic}

Proof:
(m x1 x2+1)
= { Def m, C1, C2, C3, C8}
0 + -(x2 + 1)
< { Arithmetic}
-x2
= { Def m, C1, C2, C3, C7 }
(m x1 x2)

Proof of Condition 4 for the third recursive call:
(listp x1) /\ (integerp x2) /\ (not (and (endp x1) (equal x2 0)))
    /\(not(and (endp x1) (> x2 0)))/\(not(endp x1)) 
=> ((m x1 x2) > (m (rest x1) (- 0 x2)))
Context:
C1. (listp x1)
C2. (integerp x2)
C3. (not (endp x1))
NOTE: the other parts of the context didn't help so I left them off.

Proof:
(m x1 x2)
= {Def m, C1, C2, C3}
(len x1) + (abs x2)
> {Arithmetic}
(len x1) - 1 + (abs (- 0 x2))
= {def len, C3, def endp}
(len (rest x1)) + (abs (- 0 x2))
= {Def m, C1, C2, C3}
(m (rest x1) (- 0 x2))

|#