#| CS 2800 Homework 11 - 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 hwk11.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_ need to use ACL2s. Technical instructions: - Open this file in ACL2s. - 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. We will deduct points for files that are not accepted by ACL2s: we sometimes ask explicitly to insert your answer in the comments, when the answer is not to be accepted by ACL2s. When asked to insert your answer in the comments, do so. - 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. |# #| Part A. Algebraic data types: Considering the following three properties: T1: (natp x) => (f x 0) = x T2: (natp x) & (natp y) => (f x y) = (f y x) T3: (natp x) & (natp y) & (natp z) => (f x (f y z)) = (f (f x y) z) Notice that the + function (addition) satisfies all three properties, T1, T2, and T3. |# #| A1. Find another function that satisfies all three properties, T1, T2, and T3. Prove that your function satisfies all three properties using ACL2s. |# ; answer ... #| Next we prove that T1, T2, T3, are independent. We have to prove three things: |# #| A2. Prove that T1 is not redundant. That is, find a function f1 which satisfies T2 and T3, but does not satisfy T1. Prove using ACL2s that your f1 satisfies T2 and T3, and present using check= a counter-example that shows that your f1 violates T1. |# ; answer: ... #| A3. Prove that T2 is not redundant. That is, find a function f2 which satisfies T1 and T3, but does not satisfy T2. Prove using ACL2s that your f2 satisfies T1 and T3, and present using check= a counter-example that shows that your f2 violates T2. |# ; answer: ... #| A4. Prove that T3 is not redundant. That is, find a function f3 which satisfies T1 and T2, but does not satisfy T3. Prove using ACL2s that your f3 satisfies T1 and T2, and present using check= a counter-example that shows that your f3 violates T3. |# ; answer: ... #| Part B. Observational equivalence and state machines A state machine is an object that has a notion of "states" and a notion of "transitions" between states. State machines also usually have inputs and outputs. We define a simple state machine as follows: The machine has 7 states, labeled: I, E, O, EE, EO, OE, OO. Initially, the machine is at state I. The machine has 10 possible inputs, the digits from 0 to 9: 0, 1, 2, 3, 4, 5, 6, 7, 8, 9. At each step in its operation, the machine moves from its current state S to its next state S', depending on the given input X. These moves are represented by the transition table of the machine, which is as follows: ----------------------------------------- Current state | Input | Next state ----------------------------------------- I | 0,2,4,6,8 | E I | 1,3,5,7,9 | O E | 0,2,4,6,8 | EE E | 1,3,5,7,9 | EO O | 0,2,4,6,8 | OE O | 1,3,5,7,9 | OO EE | 0,2,4,6,8 | EE EE | 1,3,5,7,9 | EO EO | 0,2,4,6,8 | OE EO | 1,3,5,7,9 | OO OE | 0,2,4,6,8 | EE OE | 1,3,5,7,9 | EO OO | 0,2,4,6,8 | OE OO | 1,3,5,7,9 | OO ----------------------------------------- You should read this table as follows: Row 1: "If the current state of the machine is I, and the input is either 0, or 2, or 4, or 6, or 8, then the machine moves to state E." Row 4: "If the current state of the machine is E, and the input is either 1, or 3, or 5, or 7, or 9, then the machine moves to state EO." Etc. We first provide a "flat" implementation of the above state machine: |# (defdata state (enum '(I E O EE EO OE OO))) (defdata input (range integer (0 <= _ <= 9))) (definec init-state () :state 'I) (definec transition (s :state x :input) :state (cond ((equal s 'I) (if (oddp x) 'O 'E)) ((or (equal s 'O) (equal s 'OO) (equal s 'EO)) (if (oddp x) 'OO 'OE)) ((or (equal s 'E) (equal s 'EE) (equal s 'OE)) (if (oddp x) 'EO 'EE)) (t 'I))) ; should be unreachable ; a sequence of states (defdata state-seq (listof state)) ; a sequence of inputs (defdata input-seq (listof input)) (definec aapp (x :tl y :tl) :tl (if (endp x) y (cons (car x) (aapp (cdr x) y)))) (defthm lem-aapp-state-state-seq (implies (and (statep s) (state-seqp l)) (state-seqp (aapp l (list s))))) (in-theory (disable statep)) #| B1. Define a function called "run" which takes as input a sequence of machine inputs, input-seq, and returns the sequence of states that the machine goes through as it executes on the given input sequence. As usual, feel free to introduce helper functions. |# ; answer ... (check= (run nil) '(I)) (check= (run '(1 1 1)) '(I O OO OO)) (check= (run '(1 2 3 4 5)) '(I O OE EO OE EO)) #| B2. State in ACL2s the property that no matter what the input sequence is, state 'I appears exactly once in the state sequence generated by run. Check this property using ACL2s using test?. |# ; answer: ... #| B3. Come up with a new (and simpler) implementation of the above state machine. That is, come up with new data types "state2" and "state2-seq", a new initial-state function "init-state2", and a new transition function "transition2". You will also need a new function "run2" (you may need a lemma to get this accepted -- see above what we did before the definition of "run"). |# ; answer: ... #| B4. Define a function "obs" which maps states of type state2 to states of type state. Then define a function "observations" which maps state2-seq to state-seq. |# ; answer: ... #| B5. State formally the property that the state/transition implementation of the state machine is observationally equivalent to the state2/transition2 implementation of the state machine. That is, the property stating that for any input sequence the output sequences (i.e., the sequences of states) generated by the two implementations are observationally equivalent. Use the "observations" function that you defined above. Use ACL2s property-based testing (test?) to check the observational equivalence property. |# ; answer: ... ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; 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/1FAIpQLSc9GGvRZcbqSP6hvJJKUh1B77sBXJTn-x9SjOI6MvY6xrYv2Q/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). --------------------------------------------- ... |#