#| CS 2800 Homework 10 - Spring 2019 This homework is done in groups. * Groups should consist of 2-3 people. * One group member will create a group in BlackBoard. See the class Webpage for instructions on how to do that. * Other group members then join the group. * Homework is submitted by only one person per group. Therefore make sure the person responsible for submitting actually does so. If that person forgets to submit, your team gets 0. - We recommend that groups email confirmation messages and submit early and often. * Submit the homework file (this file) on Blackboard. Do not rename this file. There will be a 10 point penalty for this. When done, save your file and submit it as hwk10.lisp. Make sure your Blackboard submission is valid ACL2s code. One way to check this is to download your submission from Blackboard after you've uploaded it, and check it using ACL2s. * 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. The format should be: FirstName1 LastName1, FirstName2 LastName2, ... For example: Names of ALL group members: Frank Sinatra, Billy Holiday There will be a 10 pt penalty if your names do not follow this format. Replace "..." below with the names as explained above. Names of ALL group members: ... * Later in the term if you want to change groups, the person who created the group should stay in the group. Other people can leave and create other groups or change memberships. See the class Webpage. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; For this homework you will NOT need to use ACL2s. However, you could use the Eclipse/ACL2s text editor to write up your solution and you may want to use ACL2s to help you check your answers. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; In your proofs: If you use induction, identify the induction scheme you are using (function and variable(s)). If you use lemmas, formally define the lemmas and then prove them. Also identify the instantiation you apply to each lemma when you use that lemma in your proof (you can instantiate lemmas in the context or derived context). Assuming your theorem/lemma phi is contract-complete, you may ignore the induction proof obligation ~ic => phi If you use lemmas already introduced/proven in class or in the lecture notes, you don't have to prove them (but you will still need to formally state which lemmas you are using, and instantiate them). |# #| Reasoning about tail recursive functions |# #| Consider the following function definition: |# (definec sum (n :nat) :nat (if (equal n 0) 0 (+ n (sum (- n 1))))) #| 1. Is sum a tail-recursive function? Explain. answer: ... |# #| 2. Define a tail-recursive version of sum, called sumt, using the recipe explained in class. Explain why sumt is tail-recursive. Use sumt for the tail-recursive helper function, and sum* for the new version of sum which has the same interface as sum. |# ; answer: (definec sumt ... ... #| sumt is tail-recursive because ... |# (definec sum* ... ... #| 3. State the theorem that says that sum and sum* are equivalent, and prove the theorem formally. |# ; answer: (thm ... #| Proof: ... QED |# #| Let us now define some functions on sets. We represent sets as lists. Repetitions of elements is allowed. The order of elements in the list does not matter. |# (definec in (a :all x :tl) :bool ; a is an element of set x (cond ((endp x) nil) ((equal a (car x)) t) (t (in a (cdr x))))) (definec subset (x :tl y :tl) :bool (cond ((endp x) t) ((in (car x) y) (subset (cdr x) y)) (t nil))) ; a non-tail-recursive definition of set intersection: (definec intersect (x :tl y :tl) :tl ; returns the intersection of sets x and y (cond ((endp x) nil) ((in (car x) y) (cons (car x) (intersect (cdr x) y))) (t (intersect (cdr x) y)))) #| 4. Explain why intersect is not tail-recursive: answer: ... |# #| 5. Define a tail-recursive version of intersect by modifying the above definition according to the scheme provided in class. You should not use the version in lab 10: in particular do not use the function del-all. |# ; answer: (definec intersectt ... ... #| We want to prove that intersect and intersectt are equivalent in the set-theoretic sense. This means that they might not necessarily yield identical lists, but they should yield lists that represent the same sets. For example, the lists (1 2 3) and (3 1 2 1 3) represent the same sets. 6. State the theorem that expresses that intersect and intersectt are equivalent. Then formally prove the theorem. Feel free to use functions like cons, aapp, etc. But do not prove an equality result with a reverse function like in lab 10. In particular, we want a theorem that states set-equivalence, not list equality (or equality modulo reverse). Warning: this proof might generate many lemmas. Don't be afraid, most are easy to prove. |# ; answer: (thm ... #| Proof ... QED. Phew! |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Part III: Feedback (5 points) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| Each week we will ask a few questions to monitor how the course is progressing and to solicit suggestions for improvement. Please fill out the following form. https://docs.google.com/forms/d/e/1FAIpQLSfW01DDvqHnLTOt4ue6NeMtim6BG96dD5R1aHS68zgt1rCCiA/viewform?usp=sf_link 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, but 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. The questionnaire is worth 5 points (hence the rest of the homework problems are worth 95 points). The following team members filled out the feedback survey provided by the link above (replace the ...'s with the names of the team members who filled out the questionnaire). --------------------------------------------- ... |#