#| CS 2800 Homework 7 - Summer 2018 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; This homework is to be done in a group of 2-3 students. It is designed to give you practice with function admissibility and introduce you to measure functions. 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. However, you could use the Eclipse/ACL2s text editor to write up your solution. |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Admissible or not? ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; For each of the definitions below, check whether it is theoretically 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, BRIEFLY 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. Your explanations should be brief but clear. We are not looking for a page of text per question but we also want to clearly see that you understand the function and if/what is wrong with it. I used the term "theoretically admissible" because for some functions below you can demonstrate they are admissible but ACL2s won't actually admit it without a lot of extra guidance from you (this isn't your responsibility). ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; SECTION 1: Admissibility ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 1. (defunc f1 (n) :input-contract (natp n) :output-contract (rationalp (f1 n)) (if (equal n 0) n (f1 (/ n 2)))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 2. (defunc f2 (a b) :input-contract (and (listp a) (listp b)) :output-contract (posp (f2 a b)) (cond ((or (endp a) (endp b)) 1) ((> (len a) (len b)) (+ 1 (f2 (rest a) (cons (first a) b)))) ((equal (len a) (len b)) 0) (t (+ 1 (f2 (cons (first b) a)(rest b)))))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 3. (defunc f3 (x y) :input-contract (and (listp x)(listp y)) :output-contract (listp (f3 x y)) (cond ((< (len x) (len y)) (f3 (cons (first y) x) y)) ((> (len x) (len y)) (f3 (rest x) y)) (t x))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 4. (defunc f4 (x y) :input-contract (and (natp x) (posp y)) :output-contract (posp (f4 x y)) (cond ((equal y 1) y) ((equal x 0) x) ((< y x) (f4 y x)) (t (f4 x (- y 1))))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 5. (defunc f5 (y z) :input-contract (and (rationalp y) (rationalp z)) :output-contract (rationalp (f5 y z)) (cond ((<= y 0) z) ((> z 0) (f5 y (- z y))) (t z))) Think about if any variables converge towards a value and how much they are guaranteed to converge each recursive call. Can you convert this amount to a natural? ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 6. (defunc f6 (x y) :input-contract (and (listp x)(natp y)) :output-contract (natp (f6 x y)) (cond ((equal y 0) (len x)) ((endp x) 0) (t (f6 (len x) (list y))))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 7. (defunc f7 (i) :input-contract (integerp i) :output-contract (integerp (f7 i)) (if (< i -5) i (- f7 (* i i)))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 8. (defunc f8 (x y) :input-contract (and (posp x) (integerp y)) :output-contract (posp (f8 x y)) (if (>= y x) (+ x y) (+ (* y y) (f8 (+ x 1) (+ y 2))))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 9. (defunc f9 (i x j) :input-contract (and (posp i) (listp x) (posp i)) :output-contract (posp (f9 i x j)) (cond ((equal j 1) (+ (len x) j)) ((equal i 1) (+ i j)) (t (f9 (- i 1) (cons (+ i j) x) (- j 1))))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 10. (defunc f10 (a b) :input-contract (and (natp a) (posp b)) :output-contract (posp (f10 a b)) (cond ((or (equal a 0)(equal b 1)) 1) ((> a b) (f10 b a)) (t (+ 1 (f10 a (- b 1)))))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 11. (defunc f11 (x n) :input-contract (and (listp x) (integerp n)) :output-contract (loip (f11 x n)) (if (endp x) nil (if (< n 0) (cons (first x) (f11 (rest x) (+ n 1)) (f11 (cons n (rest x)) (- n 1))))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 12. ; if you want to push ACL2s through these functions, put it in program mode here. ;:program (defunc f12 (p i) :input-contract (and (posp p)(integerp i)) :output-contract (posp (f12 p i)) (cond ((equal p 1) 10) ((< p 9) (- (f12 (- p 1) i) 1)) ((> i p) (f12 i (- p 2))) (t (f12 (- p 1) i)))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 13. (defunc f13 (p r) :input-contract (and (posp p)(rationalp r)) :output-contract (posp (f13 p r)) (cond ((equal p r) 10) ((< p r) (+ (f13 (+ p (numerator r)) r) 1)) (t (f13 p (+ r 1))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 14. (defunc f14 (x y) :input-contract (and (posp x) (posp y)) :output-contract (integerp (f14 x y)) (cond ((equal x y) 5) ((< x y) (f14 y x)) ((< x 1) (f14 x y)) (t (- (f14 (- x 1) y) 3)))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 15. (defunc f15 (x y) :input-contract (and (natp x) (natp y)) :output-contract (posp (f15 x y)) (cond ((equal x y) 1) ((> x y) (f15 y x)) (t (f15 x (- y 2))))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 16. (defunc f16 (x y) :input-contract (and (listp x) (posp y)) :output-contract (listp (f16 x y)) (cond ((endp x) (list y)) ((equal y 1) (f16 x (len x))) (t (f16 (rest x) (- y 1))))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 17. (defunc f17 (l) :input-contract (listp l) :output-contract (booleanp (f17 l)) (cond ((endp l) l) ((in e l) t) (t (cons (first l)(f17 (rest l)))))) ................ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; SECTION 2: DOES IT TERMINATE? ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; For each of the following functions, mention whether the function terminates ;; or not. If it does, give a measure function for it AND write the proof obligations ;; needed to prove termination (here we are not asking you to prove anything). ;; Features of a valid measure function are described ;; in section 3 below and in the notes. ;; If it does not terminate, give a concrete input on which it fails. ;; Here is a function you can use to help you ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; abs: integer -> natural ;; (abs i) takes an integer value ;; and returns the absolute value ;; of that number (thus a natural number) (defunc abs (i) :input-contract (integerp i) :output-contract (natp (abs i)) (if (< i 0) (unary-- i) i)) #| ;; EXAMPLE: for the function app the solution would be (defunc m-app (x y) :input-contract (and (listp x)(listp y)) :output-contract (listp (m-app x y)) (len x)) ;Proof Obligation (listp x) /\ (listp y) /\ ~(endp x) => (m-app x y) = (len x) > (len (rest x)) = (m-app (rest x) y) |# #| (defunc f18 (r) :input-contract (rationalp r) :output-contract (integerp (f18 r)) (if (equal r 0) 14 (+ (f18 (- (abs (numerator r)) 1)) 4))) ................ (defunc f19 (x) :input-contract (integerp x) :output-contract (integerp (f19 x)) (cond ((equal x 0) 1) ((> x 0) (* x (f19 (- x 1)))) (t (* x (f19 (+ x 1)))))) ................ (defunc f20 (l i) :input-contract (and (listp l)(integerp i)) :output-contract (natp (f20 l i)) (if (< i 0) (len l) (f20 l (- i (len l))))) ................ (defunc f21 (l1 l2) :input-contract (and (listp l1)(listp l2)) :output-contract (booleanp (f21 l1 l2)) (cond ((endp l1) t) ((endp l2) (f21 (rest l1) l2)) (t (f21 (cons (first l2) l1) (rest l2))))) ................ (defunc f22 (n m) :input-contract (and (integerp n)(integerp m)) :output-contract (integerp (f22 n m)) (cond ((equal n m) 1) ((< n m) (f22 (+ n 1)(- m 1))) (t (f22 (- n 1) m)))) ................ |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Section 3: Proving a Measure Function ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| You can prove a function f terminates using a measure function m. This requires the following conditions are met: 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 on exams): - Write down the propositional logic formalization of Condition 4. - Simplify the formula. - 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) (if (equal y 0) 0 (+ 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)) For the first recursive call in f, the propositional logic formalization for proving Condition 4 is: (implies (and (listp x) (natp y) (endp x) (not (equal y 0))) (< (m x (- y 1)) (m x y))) This can be rewritten as: (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, Def len, Arithmetic } (- y 1) < { Arithmetic } y = { Def m, C3, Def. len, Arithmetic } (m x y) The propositional logic formalization for Proof of Condition 4 for the second recursive call: (implies (and (listp x) (natp y)(not (endp x))) (< (m (rest x) y) (m x y))) Proof: C1. (listp x) C2. (natp y) C3. (not (endp x)) (m (rest x) y) = { Def m, C3 } (+ (len (rest x)) y) < { Arithmetic, Decreasing len axiom } (+ (len x) y) = { Def m } (m x y) Hence f terminates, and m is a measure function for it. QED ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 23. Prove f23 terminates: (defunc f23 (x y c) :input-contract (and (natp x) (natp y) (natp c)) :output-contract (integerp (f23 x y c)) (cond ((and (>= x 1024) (>= y 1024)) c) ((< y 1024) (f23 x (+ y 1) (+ c 1))) (t (f23 (+ x 1) 0 (+ c 1))))) .....in case you are curious as to what this is, think about a 2D array What is the measure function for f23? Keep in mind that (if (> x 1024) 0 (- 1024 x)) will always be a nat AND if x is outside of a typical the value is 0. Also, what is the maximum number of recursive calls this function can ever make? ............ What are the proof obligations? ......... Now prove that m23 is a measure function for f23 using equational reasoning .......... ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 24. Prove f24 terminates (ungraded extra practice) |# (defunc f24 (l1 l2 flag) :input-contract (and (listp l1)(listp l2)(booleanp flag)) :output-contract (listp (f24 l1 l2 flag)) (cond ((and (endp l1) (not flag)) (f24 l1 l2 t)) ((not flag) (f24 (rest l1) (cons (first l1) l2) flag)) ((not (endp l2)) (f24 (cons (first l2) l1) (rest l2) flag)) (t l1))) #| ............... Proof Obligations: ................ |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Feedback (5 points) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| Each week we will ask a couple questions to monitor how the course is progressing. This won't be as long as the HW05 survey. Please fill out the following form. https://goo.gl/forms/pypK8LX4GlfQ1Ovs1 As before, feedback is anonymous and each team member should fill out the form (only once per person). After you fill out the form, write your name below in this file, not on the questionnaire. We have no way of checking if you submitted the file, but by writing your name below you are claiming that you did, and we'll take your word for it. 5 points will be awarded to each team member for filling out the questionnaire. More importantly, if a course topic is confusing you, I can address the issue without you having to worry that only you don't get the topic (Note: it's almost never the the case that only 1 student is confused but I know it can still be scary) The following team members filled out the feedback survey provided by the link above: --------------------------------------------- |#