#| CS 2800 Homework 2 - 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. * 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 need to use ACL2s. Technical instructions: - Open this file in ACL2s as hwk02.lisp - Make sure you are in ACL2s 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 "..."). Sometimes we require textual explanations (e.g., complexity analysis below) so just add your explanation inside the ACL2s comments. - Only add to the file. Do not remove or comment out anything pre-existing. - 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 hwk01.lisp - Do not submit the session file (which shows your interaction with the theorem prover). This is not part of your solution. Only submit the lisp file. Instructions for programming problems: For each function definition, you must provide both contracts and a body. You must also ALWAYS supply your own tests. This is in addition to the tests sometimes provided. Make sure you produce sufficiently many new test cases. This means: cover at least the possible scenarios according to the data definitions of the involved types. For example, a function taking two lists should have at least 4 tests: all combinations of each list being empty and non-empty. Beyond that, the number of tests should reflect the difficulty of the function. For very simple ones, the above coverage of the data definition cases may be sufficient. For complex functions with numerical output, you want to test whether it produces the correct output on a reasonable number of inputs. Use good judgment. For unreasonably few test cases we will deduct points. We will use ACL2s' check= function for tests. This is a two-argument function that rejects two inputs that do not evaluate equal. You can think of check= roughly as defined like this: (defunc check= (x y) :input-contract (equal x y) :output-contract (equal (check= x y) t) t) That is, check= only accepts two inputs with equal value. For such inputs, t (or "pass") is returned. For other inputs, you get an error. If any check= test in your file does not pass, your file will be rejected. We will again use the following directives to allow ACL2s to proceed even if a proof fails (do not remove them): |# (set-defunc-termination-strictp nil) (set-defunc-function-contract-strictp nil) (set-defunc-body-contracts-strictp nil) #| 1. Use defdata to define lor, a true list of rationals. This automatically generates the recognizer lorp which checks whether a given object is a rational number. Subsequent problems in this homework might require the use of lorp. |# (defdata lor ...) (check= (lorp ()) t) (check= (lorp '(1 2/3 3)) t) (check= (lorp '(1 "2/3" 3)) nil) #| 2. Define a recognizer for a true list that has an odd number of elements. Call it "oddlenlistp". You can use the built-in functions that check if a number is odd/even: oddp: int -> bool evenp: int -> bool |# (definec oddlenlistp (l ...) ...) #| 3. Define a function that checks whether a given true list of rationals is non-decreasing. For example '(1 2 3) is non-decreasing and so is '(2/3 1 3) but '(1 2/3 3) is not. Duplicates are allowed, so '(1 1 2) is also non-decreasing. |# (definec non-decreasing (l ...) ... ... (check= (non-decreasing '(1 2 3)) t) (check= (non-decreasing '(2/3 1 3)) t) (check= (non-decreasing '(1 2/3 3)) nil) (check= (non-decreasing '()) t) #| 4. Use defdata to define ne-lor, a non-empty true list of rationals. |# (defdata ne-lor ...) #| 5. Define a function ith-element, which consumes a non-empty true list of rationals l and a number i and returns the ith element of l. The index i must be a natural number between 0 (inclusive) and the length of l (exclusive). |# (defunc ith-element (l i) :input-contract ... :output-contract ... ... (check= (ith-element '(1 2 3) 1) 2) (check= (ith-element '(1 3) 0) 1) (check= (ith-element '(1 2/3 3 0) 3) 0) #| 6. Define the function odd-ordered-median that computes the median of a given true list of rationals nl. There are two conditions on nl: First, nl must be in non-decreasing order. Second, nl must contain an odd number of elements. Hint: the functions you have defined so far should come in handy, both in the contract and in the body definition of median. |# (defunc odd-ordered-median (nl) :input-contract ... :output-contract ... ... (check= (odd-ordered-median '(1)) 1) (check= (odd-ordered-median '(1 2 3)) 2) (check= (odd-ordered-median '(1 1 2)) 1) (check= (odd-ordered-median '(1 2 3 4 5)) 3) #| 7. Define the function median. It is given a non-empty true list of rational numbers and returns a rational number, the median. The input does not have to be ordered, so you should sort it, say using insertion sort, and if its length is odd, return the element in the middle. If the length of the list is even, then there are two middle numbers, so return their average. See the tests below. |# (definec median (l :ne-lor) :rational ... (check= (median '(4 2 5 0 1 3)) 5/2) (check= (median '(4 2 5 0 1 3 6)) 3) #| 8. Do Exercise 2.4 from the lecture notes. Write your answer here (inside the comments): ... |# #| 9. Define the Collatz conjecture function in ACL2s. The Collatz conjecture function can be written as follows in imperative pseudo-code: collatz (n : positive integer (>0)) returns positive integer { while (n > 1) do { if (n is even) then n := n/2; else n := 3*n + 1; } return n; } In the code above, := denotes assignment. So x := 1 assigns the value 1 to variable x. Perform the computations manually for a few different values of n, to see the sequence of numbers generated during the successive loop iterations. What does the function return? Can ACL2s prove termination for the Collatz function? |# (definec collatz (...) ... ... (check= (collatz 100) 1) (check= (collatz 1000) 1) (check= (collatz 10000) 1) #| 10. Define the function snoc which takes a list l and an element x and places x at the end of l. |# (definec snoc (...) ... ... (check= (snoc () 1) '(1)) (check= (snoc '(2 ) 1) '(2 1)) (check= (snoc '(2 3) 1) '(2 3 1)) ;; 11. ;; Define using defdata a list of Booleans, lob. (defdata lob ... (check= (lobp '(t nil t)) t) (check= (lobp '(nil 1 t)) nil) (check= (lobp '(nil)) t) (check= (lobp nil) t) (check= (lobp (snoc '(t) nil)) t) #| 12. We can use list of Booleans to represent natural numbers as follows. The list (t nil nil) corresponds to the number 4 written in binary as 100 (true false false). Similarly, (t nil) represents the number 2, (t t) the number 3, etc. Adding nils at the beginning of the list doesn't matter, so (nil t t) is also 3, and so is (nil nil t t). As another example, 31 is (t t t t t) or (nil nil t t t t t) or ... Usually we prefer lists of minimal length. So, although both (nil t t) and (t t) represent 3, (t t) is better because it's shorter. In many problems below we require the list to be of minimal length. What list of minimal length represents the number 0? What list of minimal length represents the number 1? Write your answers below. Note that empty lists are fine. ... the shortest list representing the number 0 is ... ... the shortest list representing the number 1 is ... |# #| 13. Define the function n-to-b that given a natural number, returns a list of Booleans, of minimal length, corresponding to that number. |# (defunc n-to-b ... (check= (n-to-b 10) '(t nil t nil)) (check= (n-to-b 7) '(t t t)) (check= (n-to-b 4) '(t nil nil)) (check= (n-to-b 31) '(t t t t t)) (check= (n-to-b 0) ()) #| 14. Define the function b-to-n that given a list of Booleans, returns the natural number corresponding to that list. Do NOT assume that the given list of Booleans is of minimal length. So (nil t nil) is an acceptable input, and b-to-n should return 2 for that one. |# (defunc b-to-n ... (check= (b-to-n '(nil t nil t)) 5) (check= (b-to-n '(t t t)) 7) (check= (b-to-n '(nil nil t)) 1) (check= (b-to-n '(t t t t t)) 31) (check= (b-to-n ()) 0)