#| CS 2800 Homework 10 - Summer 2018 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. |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| Inductive Proofs: - For all proofs below, solutions must be in the format described in class and in the notes. This includes: * Explicitly identifying an induction scheme and the function that gives rise to it. * Labeling general context (C1, C2....) and derived context. * Providing justifications for each piece of derived context. * Explicitly identifying axioms and theorems used * The if axioms and theorem substitutions are not required. You can use any other shortcuts previously identified. * PL can be given as justification for any propositional logic rules with the exceptions of Modus Ponens (MP) and Modus Tollens (MT) * Hocus Pocus (HP) is not permissible justification. * All arithmetic rules can be justified by writing "Arithmetic". Previous homeworks (such as HW05) identify these requirements in more detail. |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| For this homework you may want to use ACL2s to help you. Technical instructions: - open this file in ACL2s as hw10.lisp - make sure you are in BEGINNER mode. This is essential! Note that you can only change the mode when the session is not running, so set the correct mode before starting the session. - insert your solutions into this file where indicated (usually as #......# or ....) - only add to the file. Do not remove or comment out anything pre-existing unless asked to. - make sure the entire file is accepted by ACL2s. In particular, there must be no "..." left in the code. If you don't finish all problems, comment the unfinished ones out. Comments should also be used for any English text that you may add. This file already contains many comments, so you can see what the syntax is. - when done, save your file and submit it as hw10.lisp - avoid submitting the session file (which shows your interaction with the theorem prover). This is not part of your solution. Only submit the lisp file! |# #| ------------------------------------ REASONING ABOUT TAIL-RECURSIVE FUNCTIONS You can freely use the definitional and function contract theorems of the functions we provide below or that we have covered in class. You can also freely use any theorems we proved in class and in the lecture notes. Make sure you identify what induction scheme you are using. For example, suppose you were proving that app is associative: (listp x) ^ (listp y) ^ (listp z) => (app (app x y) z) = (app x (app y z)) At the beggining of the proof you should say: Proof by induction using (listp x). You will be asked to define tail recursive versions of given functions, using accumulators. This involves two function definitions. For example, to define a tail recursive version of rev, we first define rev-tl. rev-tl is recursive and has an extra argument, the accumulator. Second, we define rev*, a non-recursive function that calls rev-tl with the accumulater appropriately initialized and which satisfies the theorem that rev* = rev, ie, : (listp x) => (rev* x) = (rev x) |# ;; Tail-recursive version of rev (auxiliary function) (defunc rev-tl (x acc) :input-contract (and (listp x) (listp acc)) :output-contract (listp (rev-tl x acc)) (if (endp x) acc (rev-tl (rest x) (cons (first x) acc)))) ;; Non-recursive version of rev that uses rev-tl (defunc rev* (x) :input-contract (listp x) :output-contract (listp (rev* x)) (rev-tl x nil)) #| You will also be asked to prove that the tail recursive version of a function is equal to the original function. For our example, the theorem is (implies (listp x) (equal (rev* x) (rev x))) To do that you have to come up with lemmas; in particular you have to come up with the right generalizations. If you choose to use ACL2s to help you figure out the proofs, here is how you would do that: |# ; This is the lemma we need (defthm revt-rev (implies (and (listp x) (listp acc)) (equal (rev-tl x acc) (app (rev x) acc)))) ; With the lemma above, the main theorem follows (defthm rev*-rev (implies (listp a) (equal (rev* a) (rev a)))) ; The proofs were given in class. #| ===================================== Q1. In this example, we will see how to speed up numeric functions. Consider the following Fibinacci-like function. Notice it takes a long time to admit because it takes a long time to run (so testing takes a long time). NOTE: going to labs will be extremely useful for this function. We'll be covering the fib-t proof |# :program (defunc f1 (p) :input-contract (posp p) :output-contract (posp (f1 p)) (if (<= p 2) (+ p 2) (+ (f1 (- p 1)) (f1 (- p 2))))) #| Q1a Think about why f1 takes long. Consider (f1 6) = (f1 5) + (f1 4) = (f1 4) + (f1 3) + (f1 3) + (f1 2) = (f1 3) + (f1 2) + (f1 2) + (f1 1) + (f1 2) + (f1 1) Notice that (f1 2) was computed multiple times, as was (f1 1). This leads to an exponential number of calls to f1. We can do better. Define f1-t, a function that takes multiple arguments and can be used to compute f1 quickly. f1-t should only lead to a linear (in n) number of recursive calls. Note that you can have as many arguments to f1-t as you like. |# (defunc f1-t (p a b) :input-contract (and (posp p) (posp a) (posp b)) :output-contract (posp (f1-t p a b)) (cond ((equal p 1) 3) ((equal p 2) b) ;#......# #| Q1b Define f1*, a non-recursive function that has the same signature as f1 and uses f1-t to efficiently compute f1. f1* should be equal to f1. |# #......# #| Q1c Prove a theorem of this form (implies ... (equal (f1-t ...) ... (f1 n) ....)) HOWEVER, we gave this to students last term and even I couldn't figure it out (at least not with people looking at me). Thus let me remind you of something: (defunc fib (n) :input-contract (natp n) :output-contract (natp (fib n)) (if (<= n 1) n (+ (fib (- n 1)) (fib (- n 2))))) Fill out the following table: (f1-t p a b) | p | (ft p) | a | b | (fib (- p 1)) -------------------------------------------------------- 47 | 7 | 47 | 3 | 4 | 8 47 | 6 | 29 | 4 | 7 | 5 47 | 5 | | | | 3 47 | 4 | | | | 2 47 | 3 | | | | 1 47 | 2 | | | | 1 47 | 1 | | | | 0 #......# Furthermore, let me point out that (f1-t p a b) = (f1 p) + (a-3)______ + (b-4)_________ Essentially you are looking for a pattern to calculate the missing term to match f1-t and ft. F1-t always returns the same value while f1 changes based on a fib-like pattern. #......# Prove that (f1* p) = (f1 p) using your lemma. #......# NO POINTS BONUS QUESTION: Prove the lemma involving f1-t that you defined above ....the basic arithmetic got too hairy for me so I can't ask you to do it but it's still a nice exercise. #......# |# #| Q1e If your definition of f* is correct and efficient, then the following test should pass instantaniously......and if your answer doesn't match, check on piazza. It's not like I can confirm my answer is correct |# (check= (f1* 500) 504437965285332091151961460776886639946151838089152805116856792315125770984413464788131304805242011086876) (check= (f1* 6) 29) (check= (f1* 1) 3) (check= (f1* 2) 4) (test? (implies (and (posp p)(< p 30)) (equal (f1 p) (f1* p)))) #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 2. Let's revisit a problem from the sample exam. You've been given functions how-many-t and how-many* such that how-many = how-many* |# (defunc how-many (e l) :input-contract (listp l) :output-contract (natp (how-many e l)) (if (endp l) 0 (+ (if (equal e (first l)) 1 0) (how-many e (rest l))))) ;; how-many-t: All x List x Nat -> Nat ;; The tail recursive helper function for how-many* ;; where acc keeps a tally of the number of instances of ;; found so far in the list l. (defunc how-many-t (e l acc) :input-contract (and (listp l) (natp acc)) :output-contract (natp (how-many-t e l acc)) (if (endp l) acc (how-many-t e (rest l) (+ (if (equal e (first l)) 1 0) acc)))) ;; how-many*: All x List -> Nat (defunc how-many* (e l) :input-contract (listp l) :output-contract (natp (how-many* e l)) (how-many-t e l 0)) #| The goal is to prove the following conjecture: phi : (listp l) => (how-many* e l) = (how-many e l) That is, we want to show that the two functions compute the same result on all inputs. We will prove this in several steps. (a) Formulate a lemma that relates how-many-t to how-many, by filling in the ... below: phi_1 : (listp l) /\ (natp acc) => (how-many-t e l acc) = ... (how-many e l) ... #......# (b) Prove phi_1. Use the induction scheme how-many-t gives rise to. Note that how-many-t has an if nested inside other functions. You can rewrite it, using cond, before extracting an induction scheme if you want to use the I.S. generating pattern from the the notes (it may help). #......# (c) Using only equational reasoning (no induction!), prove the main conjecture phi from above. Using phi_1 (which you just proved) this should be very simple. phi : (listp l) => (how-many* e l) = (how-many e l) #......# |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 2. Filtering Data Consider the following defdata and the function get-integers that uses it: We're going to selectively filter out all elements in a list that aren't integers |# (defdata integerlist (listof integer)) (defunc get-integers (l) :input-contract (listp l) :output-contract (integerlistp (get-integers l)) (cond ((endp l) nil) ((integerp (first l)) (cons (first l) (get-integers (rest l)))) (t (get-integers (rest l))))) (check= (get-integers '(b "23" lk ())) ()) (check= (get-integers '(h "ter" -1 aw 9)) '(-1 9)) (check= (get-integers '("qw" "brc" aw (1 2 3) 89 rt -1)) '(89 -1)) ;(a) Write the function get-integers-t, which is a tail-recursive version of ;get-integers with an accumulator: ;; get-integers-t: listp x integerlist -> integerlist ;; get-integers-t takes a list and removes all elements ;; in the list that are not integers (this includes sub-lists of integers) ;; acc is an accumulator that collects integers to return. (defunc get-integers-t (l acc) ;;......................) ;;Obviously write your own tests too #......# ;; Here is get-integers*, a non-recursive function that calls ;; get-integers-t and suitably initializes l and acc : (defunc get-integers* (l) :input-contract (listp l) :output-contract (integerlistp (get-integers* l)) (rev (get-integers-t l ()))) #| (c) Identify a lemma that relates get-integers-t to get-integers. Remember that this is a generalization step, i.e., all arguments to get-integers-t are variables (no constants). The RHS should include acc. .................... #......# (d) Assuming that lemma in (c) is true and using ONLY equational reasoning, prove the main theorem: (listp l) => (get-integers* l) = (get-integers l) If you need any "lemmas", note them down as "debt", to be proved later. This should include any theorems that we've already proven (you won't need to prove these but you still need to list them) .................... #......# (e) Prove the lemma in (c). Use the induction scheme of get-integers-t. In doing so, you can use the following lemma for free (i.e., you don't need to prove it). L3: (integerp e) /\ (integerlistp l) => (integerlistp (cons e l)) Again, if you need another lemma, note it as "dept" #......# (f) List here any lemmas that you used in parts c and d. If any of them are "new", you need to prove them. (Hint: all lemmas in my solution have appeared in class/notes before but your proof my differ) #......# |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 3. Max Depth Consider a btree data structure that we want to calculate the maximum depth for. We will do this in 2 parts: 1) Write the tail recursive functions t-maxdepth-t and t-maxdepth* - If you all find this too difficult I can supply t-maxdepth-t It is NOT what I want you spending all your time on. You time should be spent on the proof. 2) Prove t-maxdepth* = t-maxdepth |# ; A binary tree structure where each node has a numeric value ; Notice the tree does not have to be in order. (defdata btree (oneof nil (list rational btree btree))) ;; An empty tree has no child nodes and no value. (defunc t-emptyp (btree) :input-contract (btreep btree) :output-contract (booleanp (t-emptyp btree)) (equal btree nil)) (check= (t-emptyp '(2 nil nil)) nil) (check= (t-emptyp nil) t) (check= (t-emptyp '(3 (4 nil nil) (4 (3 nil nil) (2 nil nil)))) nil) (defunc max (x y) :input-contract (and (natp x)(natp y)) :output-contract (natp (max x y)) (if (< x y) y x)) ;; Proof for non-empty trees. Used to help ACL2s reason. (defthm t_secondne (implies (and (btreep btree)(not (t-emptyp btree))) (btreep (second btree)))) (defthm t_thirdne (implies (and (btreep btree)(not (t-emptyp btree))) (btreep (third btree)))) (defconst *tTest* '(3 (4 (5 (6 nil nil) (7 nil (8 nil nil))) (4 (3 nil nil) (2 nil nil))) (5 nil nil))) (defunc t-maxdepth (btree) :input-contract (btreep btree) :output-contract (natp (t-maxdepth btree)) (if (t-emptyp btree) 0 (let ((sdepth (+ 1 (t-maxdepth (second btree)))) (tdepth (+ 1 (t-maxdepth (third btree))))) (if (< sdepth tdepth) tdepth sdepth)))) (check= (t-maxdepth *tTest*) 5) (check= (t-maxdepth (list 4 nil *tTest*)) 6) (test? (implies (btreep tree)(equal (t-maxdepth (list 4 nil tree))(+ (t-maxdepth tree) 1)))) ; Program mode is fine if you need that. #......# #| Now prove t-maxdepth = t-maxdepth*. You will need a lemma and you will have to prove that lemma #......# |# (t-maxdepth-t nil 8 24) (t-maxdepth nil) ;; You can test your lemma with test? if that makes your life easier. #......# #| EXTRA PRACTICE ??? If you want additional practice problems, try writing tail recursive functions for the following functions and then prove they are equivalent to the original - min-l - delete - merge In fact, for many functions that aren't already tail recursive, you can write a tail recursive version and then prove the equivalence. You can generate your own problems. |#