#| CS 2800 Homework 4 - 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. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; For this homework you will need to use ACL2s. Technical instructions: - open this file in ACL2s as hw04.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 "...") - 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 hw04.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! 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. The markers have been given permission to add any tests they want. Thus one way to tell how many tests you need: are you positive the markers won't break your code? 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. You should also use test? for your tests. See Section 2.13 of the lecture notes. An example of test? is the following. (test? (implies (and (listp l) (natp n)) (<= (len (sublist-start n)) n))) |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; Propositional Logic ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| We use the following ascii character combinations to represent the Boolean connectives: NOT ~ AND /\ .....^ in the programming section OR \/ .....v in the programming section IMPLIES => EQUIV = XOR <> The binding powers of these functions are listed from highest to lowest in the above table. Within one group (no blank line), the binding powers are equal. This is the same as in class. |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Section 1: Truth Tables Construct the truth table for the following Boolean formulas. Use alphabetical order for the variables in the formula, and create columns for all variables occurring in the formula AND for all intermediate subexpressions. (with one exception: you can omit negations of a single variable such as ~p or ~r). For example, if your formula is (p => q) \/ r your table should have 5 columns: p | q | r | p => q | (p => q) \/ r ------------------------------------- F | F | F | T | T F | F | T | T | T F | T | F | T | T F | T | T | T | T T | F | F | F | F T | F | T | F | T T | T | F | T | T T | T | T | T | T Then decide whether the formula is satisfiable, unsatisfiable, valid, or falsifiable (more than one of these predicates will hold!). Example: Satisfiable and falsifiable a) (~p /\ q) = (q => p) ....... b) (~p => q) /\ (~r = q) <> (~p => r) Hint: your table should have 8 or 11 columns (depending if you write the not columns including columns for p,q,r). ....... ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; Section 2. Logic Rules Simplify the following expressions using propositional logic rules (give either the rule name or the formula. You will get no credit for using a truth table. Transformations should take the form: expression 1 = {Justification} expression 2 = {Justification} expression 3 ...... (a) ~p = (q \/ p) /\ p .... (b) (p \/ r => ((q /\ ~r) => (r => ~r))) .... (c) (~a /\ ~b) \/ (b \/ (a /\ ~b)) ... (d) (p <> (q /\ r)) => ~(~p = (q /\ r)) ... ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |# ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; Section 3: Characterization of formulas ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| For each of the following formulas, determine if they are valid, satisfiable, unsatisfiable, or falsifiable. These labels can overlap (e.g. formulas can be both satisfiable and valid), so keep that in mind and indicate all characterizations that apply. In fact, exactly two characterizations always apply. (Think about why that is the case.) Provide proofs of your characterizations, using a truth table or simplification argument (for valid or unsatisfiable formulas) or by exhibiting assignments that show satisfiability or falsifiability. (A) ~p = (p => (q => q)) .... (B) (p => q) = ~(q \/ ~p) .... (C) ((false /\ p) \/ ~p) => (p<>p) .... (D) [(~(p /\ q) \/ r) /\ (~p \/ ~q \/ ~r)] <> (p /\ q) .... (E) ~(p => ~q \/ q) .... |# #| ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; SECTION 4: DNF In previous terms we've looked at satisfiability in this assignment. It's a known Non-deterministic Polynomial Time problem (AKA bad bad bad) that is a real costraint in a variety of CS domains. In fact, if you can solve this issue in polynomial time you can earn a million dollars and go down in history as one of the all time great computer scientists.....so pretty simple for a weekly assignment. So why is satisfiability so difficult to prove. Well you try out all assignment combinations for all variables and see if one of them resolves to true.....what if we keep going? What if we get all assignments that resolve to true? Then (if you remember CS 1800) we can generate the Disjunctive Normal Form or DNF. The DNF is a a series of expressions only containing and and not joined by ORs (or disjunctions) For example: (a /\ b /\ ~c) \/ (a /\ ~b /\ ~c) Each and expression represents a single row in the truth table that evaluates to true. ORing these together should be equivalent to the original expression. This term we'll try to generate a DNF. We're even going to give you the code for satisfiability to make your life easier. Please use the PropSatp function provided. Your job will be to return the DNF for an arbitrary expression. For this exercise, some pre-generated code and definitions are provided. This code should *not* be modified unless you check with me first. You will use these functions in the functions you write. The constants used in testing can be modified or added to. NOTE: If your functions do not get automatically admitted in ACL2s, refer to section 2.17 of the lecture notes and use the (set-defunc-...) forms described there. If your code is correct, you will get full credit, even if you need to admit the code in program mode. Don't spend time trying to get ACL2s to admit your functions. Right now, you don't know how to do that effectively. If you define a recursive function based on a recursive data definition, use the template that the data definition gives rise to. Read Section 2.15 of the lecture notes and make sure to at least read up to the bottom of page 25. Notice that in the definition of foo in the lecture notes, you have TWO recursive calls in a single cond branch, due to the PropEx data definition. Even if you don't use program mode, I've turned off the strict error checking (it will check but then time out in some cases) to hopefully make your life easier. Just the same, please be patient regarding the existing code being admitted into ACL2s. ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |# ;; Let's define the operators for any propositional expression (defdata UnaryOp '~) ; BinaryOp: '^ means "and", 'v means "or", '<> means "xor" ; and '=> means "implies" (defdata BinaryOp (enum '(^ v <> =>))) ; PXVar are the set of possible variables in an expression. (defdata PXVar (enum '(a b c d e f g h i j k p q r s x y z))) ; PropEx: A Propositional Expression (PropEx) can be a boolean (t ; or nil), a PXVar denoting a variable (e.g. 'p or 'q), or a ; list denoting a unary or binary operation. (defdata (BinEx (list BinaryOp PropEx PropEx)) (UnaryEx (list UnaryOp PropEx)) (PropEx (oneof boolean PXVar UnaryEx BinEx))) ; A list of prop-vars (PXVar)) (defdata Lopv (listof PXVar)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; DEFINE ;; add: PXVar x lopv -> lopv ;; (add a X) conses PXVar a to list of PXVars ;; X if and only if a is not in X ;; You can use the function in. ....... ;; BRUTE FORCE: I was sick of waiting for ACL2s to prove things or trying to get ;; the theorem prover to work. Hence I'm cheating and putting things in program mode. ;; That's OK but please convince yourself that your code works, terminates, and makes sense. :program ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; get-vars: PropEx x LOPV -> LOPV ;; get-vars returns a list of variables appearing in px OR ;; in the provided accumulator acc. If acc has ;; no duplicates in it, then the returned list should not have ;; any duplicates either. See the check='s below. (defunc get-vars (px acc) :input-contract (and (PropExp px) (Lopvp acc)) :output-contract (Lopvp (get-vars px acc)) (cond ((booleanp px) acc) ((PXVarp px) (add px acc)) ((UnaryExp px)(get-vars (second px) acc)) (t (get-vars (third px) (get-vars (second px) acc))))) (check= (PropExp '(v t (=> s q))) t) (check= (get-vars '(v r (=> s q)) nil) '(q s r)) (check= (get-vars '(v t nil) nil) nil) (check= (get-vars '(v s (^ s b)) nil) '(b s)) (check= (get-vars '(v s (~ b)) '(c)) '(b s c)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; del: Any x list -> list ;; Del removes the first instance of an element e in list l (defunc del (e l) :input-contract (listp l) :output-contract (listp (del e l)) (cond ((endp l) l) ((equal e (first l)) (rest l)) (t (cons (first l) (del e (rest l)))))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; perm: list x list -> boolean ;; We define perm (permutation) to make the tests more robust. ;; Otherwise, some of the tests below may fail because the order ;; in which variables appear does not matter. (defunc perm (a b) :input-contract (and (listp a) (listp b)) :output-contract (booleanp (perm a b)) (cond ((endp a) (endp b)) ((endp b) nil) (t (and (in (first a) b) (perm (rest a) (del (first a) b)))))) (check= (perm (get-vars 'A '()) '(A)) t) (check= (perm (get-vars 'A '(B C)) '(A B C)) t) (check= (perm (get-vars '(^ A B) '()) '(B A)) t) (check= (perm (get-vars '(^ B A) '()) '(B A)) t) ;; We need to evaluate all possible ways variables can be ;; assigned. Thus we need lists of var-value pairs (assign-lists) ;; ...and lists of these lists (loal) (defdata PXvar-val (list PXVar boolean)) (defdata assign-list (listof PXvar-val)) (defdata loal (listof assign-list)) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; DEFINE ;; update: PropEx x PXVar x Boolean -> PropEx ;; The update function "updates a variable" by replacing all instances ;; of the variable with the boolean val in the expression px. ;; Use the template propex gives rise to, as per the lecture notes. ;; Look at get-vars (above). (defunc update (px name val) .......) (check= (update T 'A NIL) T) (check= (update NIL 'A T) NIL) (check= (update 'A 'B T) 'A) (check= (update 'A 'A NIL) NIL) (check= (update '(^ (v NIL A) (~ B)) 'A T) '(^ (v NIL T) (~ B))) (check= (update '(^ (v NIL A) (~ B)) 'C T) '(^ (v NIL A) (~ B))) (check= (update '(^ (v NIL A) (~ B)) 'B NIL) '(^ (v NIL A) (~ NIL))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; ConstBoolExp: All -> Boolean ;; (ConstBoolExp px) determines if px is a PropEx ;; with NO symbols / free variables. (defunc ConstBoolExp (px) :input-contract t :output-contract (booleanp (ConstBoolExp px)) (and (PropExp px) (equal (get-vars px nil) nil))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; GIVEN ;; xor: Boolean x Boolean -> Boolean ;; (xor x y) returns true iff x or y are true but ;; not both (defunc xor (x y) :input-contract (and (booleanp x)(booleanp y)) :output-contract (booleanp (xor x y)) (if x (not y) y)) ;; DEFINE (helper) ;; update-all: PropEx x assign-list -> PropEx (presumably a ConstBoolExp) ;; (update-all px lv) takes a propex and updates it with each var-value assignment ;; given. This should make the resultant px a ConstBoolEx but we still need to test this. ....... ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; DEFINE ;; beval: PropEx -> Booleanp ;; beval evaluates a constant boolean expression and returns its value. ;; A constant boolean expression is a PropEx with no variables, ;; just booleans and operators. If this expression has variables, then ;; return nil. You may have to define helper functions to evaluate ;; your expressions. (defunc beval (bx) :input-contract (PropExp bx) :output-contract (Booleanp (beval bx)) .......) (check= (beval T) T) (check= (beval NIL) NIL) (check= (beval '(^ T NIL)) NIL) (check= (beval '(^ T T)) T) (check= (beval '(v T NIL)) T) (check= (beval '(~ T)) NIL) (check= (beval '(<> T NIL)) T) (check= (beval '(<> T T)) nil) (check= (beval '(<> NIL NIL)) NIL) (check= (ConstBoolExp '(v (~ nil) (^ nil t))) t) (check= (ConstBoolExp '(v (~ a) (^ nil t))) nil) ;; Tests that may help you later (you can also write your own) (defconst *test_px1* '(v (~ a) (^ a c))) ;; Sat/Falsifiable (defconst *test_px2* '(v (~ a) (^ b c))) ;; Sat/Falsifiable (defconst *test_px3* '(=> t (^ b (~ b)))) ;; Unsatisfiable/Falsifiable (defconst *test_px4* '(<> (~ a) a)) ;; Valid/Satisfiable (defconst *test_px5* t) (defconst *test_px6* nil) (defconst *test_px7* '(=> a (^ a (v a b)))) ;; Valid/Satisfiable (defconst *test_px2assign1* '((a 0) (b 0) (c 0))) (defconst *test_px2assign2* '((a 1) (b 0) (c 0))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| Generating the DNF: 1) Find all the variables in the expression 2) Generate all ways the variables can be assigned t/nil. Each way the variables can be assigned is a assign-list (list of var-value pairs) and a assign-list defines a unique ASSIGNMENT SET. 3) Assign the variables in the prop ex using each assignment set to make a constant boolean expression. 3) Evaluate each constant boolean expression you generate (using beval) and note which ones return t. Return the list of assignment sets that result in a t. 4) For each expression that returns t, use the assignment set to generate a conjuction. Combine the conjunctions using ORs. (my solution defines a function print-conj (assign-list -> list) and print-DNF (loal -> list) which uses print-conj |# (defunc getDNF (px) :input-contract (PropExp px) :output-contract (listp (getDNF px)) .........) (check= (getDNF *test_px1*) (LIST (LIST 'A '^ 'C) 'V (LIST '~ 'A '^ 'C) 'V (LIST '~ 'A '^ '~ 'C))) (check= (getDNF *test_px2*) (LIST (LIST 'A '^ 'B '^ 'C) 'V (LIST '~ 'A '^ 'B '^ 'C) 'V (LIST '~ 'A '^ '~ 'B '^ 'C) 'V (LIST '~ 'A '^ 'B '^ '~ 'C) 'V (LIST '~ 'A '^ '~ 'B '^ '~ 'C))) (check= (getDNF *test_px3*) nil) (check= (getDNF *test_px4*) (LIST (LIST 'A) 'V (LIST '~ 'A))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ; SECTION 5: SPECIFICATIONS ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; #| This section deals with specifications using the functions defined in the lecture notes. Claims below may not satisfy contract checking, which means you should perform contract completion before answering the question. For each claim, formalize it using ACL2s syntax (remember this requires that you perform contract completion). After that, indicate whether the formalized claim is valid. You do not need proofs here. If it is invalid, provide a counterexample. Also, if it is invalid, propose the simplest modification you can think of that is valid and formalize your new claim. For this part, there may be many possible answers, in which case any reasonable answer is fine. If you discover anything interesting, indicate it. Example: len2 is equivalent to len where len2 is defined as (defunc len2 (l) :input-contract (listp l) :output-contract (natp (len2 l)) (if (endp l) 0 (+ 1 (len2 (rest l))))) Answer. The formalization is: (implies (listp l) (equal (len2 l) (len l))) This conjuncture is valid. Note: that if you were to say that the claim is false because it only holds for lists, that is not a correct answer because you have to perform contract completion first! (defunc orderedp (lr) :input-contract (lorp lr) :output-contract (booleanp (orderedp lr)) (cond ((endp lr) t) ((endp (rest lr)) t) ((<= (first lr)(second lr)) (orderedp (rest lr))) (t nil))) ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 5a. The length of the list obtained by consing x and y is equal to the length of x plus the length of y. ....... ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 5b. Appending the reverse of x and the reverse of y is equivalent to reversing the list generated by appending x to y. ............... ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 5c. For any propositional expression (defined above), if the expression is a cons and not a unary expression or a list, then it is binary expression. ............... ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 5d. For any list of rationals lr that has been ordered (see definition above), the first element of the list is smaller than any other elements in the list. ............... |#