#|
CS 2800 Homework 5 - Spring 2013
For this homework, you will be using the BEGINNER mode in ACL2s.
Instructions for using this file:
- open this file in ACL2s as hw05.lisp
- set the session mode to "Beginner"
- insert your solutions into this file where indicated (for instance as
"..."). This includes contracts, the body of the function, and test cases.
Make sure you provide as many test cases as required (in addition to the
ones already provided, of course).
- do not comment in or comment out any existing function definitions from
this file. Also, do not change the order of any function definitions,
whether provided by us or defined by you.
- make sure the entire file is admitted by ACL2s in Beginner mode. This means:
* there must be no "..." in the code. If you don't finish some problems,
comment them out. The same is true for any English text that you may
add. This file already contains many comments, so you can see what the
syntax is.
* all check= tests must be satisfied. If any of the provided tests fail,
your function definition is wrong, and the file will not be admitted.
If any of your own tests fail, it may be your function is wrong, but
it may also be that your check= specification is incorrect.
Sometimes it may take a while for your function to be admitted. Be
patient: rest assured that, if your function is correct, the process will
succeed. If you don't get a success message after 2-3 mins (depending on
your hardware), then probably your definition is too complicated or
wrong.
- save the file with your additions and turn it in. To do that, check out
the directory at
svn://dell-server-wahl-1.ccs.neu.edu/cs2800-2013-spring/05/
where groupname is the name of the group as it was emailed to you. Your
username and password remain as before.
Place your file hw05.lisp in this directory, add it, and commit. Do NOT
submit the session file (ending in .a2s).
|#
; In this homework we will design a simple SAT checker. It takes a
; propositional expression and prints a satisfying
; assignment if one exists. We then use the SAT checker to build a validity
; checker.
;; We first define functions to evaluate an expression. These functions will
;; be used in the sat solver to create a satisfying assignment incrementally
;; (one variable at a time).
;; Note that this time we work with a different set of binary connectives than
;; in the last homework.
;; First we define propositional expressions. We write
;; negation as '~ , disjunction as '+ , conjunction as '& , equivalence as '==
;; and implication as '=> .
(defdata BinOp (oneof '+ '& '== '=>))
(defdata UnaryOp '~)
(defdata PropEx (oneof boolean symbol
(list UnaryOp PropEx)
(list Binop PropEx PropEx))
:type-lemmas t)
; The value type involves boolean and a special error value, which will be
; used as the evaluation result in case variables are not assigned.
(defdata value (oneof boolean 'error))
; Note: any function that you write that recurs on a propositional
; expression px must be based on its data definition. The base cases are
; (symbolp px) and (booleanp px).
; Recall the definitions of the following functions:
(defunc vand (a b)
:input-contract (and (valuep a) (valuep b))
:output-contract (valuep (and a b))
(if (or (equal a 'error)
(equal b 'error))
'error
(and a b)))
(defunc vor (a b)
:input-contract (and (valuep a) (valuep b))
:output-contract (valuep (vor a b))
(if (or (equal a 'error)
(equal b 'error))
'error
(or a b)))
(defunc vnot (a)
:input-contract (valuep a)
:output-contract (valuep (vnot a))
(if (equal a 'error)
'error
(not a)))
(defunc viff (a b)
:input-contract (and (valuep a) (valuep b))
:output-contract (valuep (viff a b))
(if (or (equal a 'error)
(equal b 'error))
'error
(iff a b)))
(defunc vimplies (a b)
:input-contract (and (valuep a) (valuep b))
:output-contract (valuep (vimplies a b))
(if (or (equal a 'error)
(equal b 'error))
'error
(if a b t)))
;; The following lemmas are required for proving the termination, contract
;; and the body contract of the functions. Please do not delete or comment
;; them out.
(defthm consp-propexp
(implies (and (not (symbolp s))
(PropExp s))
(consp s))
:rule-classes :forward-chaining)
(defthm consp-rest-propexp
(implies (and (PropExp s)
(not (symbolp s)))
(consp (acl2::rest s)))
:rule-classes (:type-prescription :forward-chaining))
(defthm consp-rest-rest-propexp
(implies (and (PropExp s)
(not (symbolp s))
(not (equal (acl2::first s) '~)))
(consp (acl2::rest (acl2::rest s))))
:rule-classes (:type-prescription :forward-chaining))
(acl2::in-theory (acl2::disable valuep-definition-thm
BinOpp-definition-thm))
; list of symbols
(defdata LoSymbol (listof symbol))
; add : symbol x LoSymbol
; (add a X): if a is not in X add symbol a to the front of X. Otherwise
; return X.
; Use the function 'in' to check if a given element is in X.
; Write at least five tests.
(defunc add (a X)
:input-contract ...
:output-contract ...
... )
(check= (add 'a nil) '(a))
(check= (add 'a '(a b)) '(a b))
(check= (add 'a '(b a)) '(b a))
; get-vars : PropEx x LoSymbol -> LoSymbol
; (get-vars px acc) returns the list of variables appearing in the
; expression `px`, including those in the provided accumulator `acc'.
; Write at least five checks.
(defunc get-vars (px acc)
:input-contract ...
:output-contract ...
...)
(check= (get-vars 'A '()) '(A))
; Whether the following tests pass depends on the order in which you return
; the variables (which is intentionally left unspecified).
; (check= (get-vars 'A '(B C)) '(A B C))
; (check= (get-vars '(& A B ) '()) '(B A))
; (check= (get-vars '(& (& A B) (+ C D) ) '()) '(D C B A))
; bval : PropEx -> value
; (bval px) evaluate boolean expression px. If px contains an unassigned
; variable, the function returns the symbol 'error. Use the function vand,
; vor, vimplies, vnot and viff.
; Write at least five checks.
(defunc bval (px)
:input-contract ...
:output-contract ...
...)
(check= (bval T) T)
(check= (bval NIL) NIL)
(check= (bval '(& T NIL)) NIL)
(check= (bval '(& T T)) T)
(check= (bval '(+ T NIL )) T)
(check= (bval '(~ T)) NIL)
(check= (bval '(+ (& NIL (~ NIL)) NIL)) NIL)
(check= (bval '(+ (& T (~ NIL)) T)) T)
(check= (bval '(+ (& NIL (~ NIL)) T)) T)
(check= (bval '(== T NIL)) NIL)
(check= (bval '(== T T)) T)
(check= (bval '(== NIL NIL)) T)
(check= (bval '(+ t x)) 'error)
(check= (bval '(+ (& NIL (~ x)) T)) 'error)
; Data definition for Assignment. The type Assign contains pairs of a
; symbol and the boolean value assigned to it.
(defdata Assign (list symbol boolean))
(defdata LoAssign (listof Assign))
;data definition for result of sat-solver : a list of
;assignments, 'unsat , 'valid , or 'error
(defdata SatisfyResult (oneof LoAssign 'unsat 'valid 'error))
; bind : PropEx x symbol x boolean -> PropEx
; (bind px name val) replaces the variable name in px with value val
; (that is, it binds the variable).
; Write at least five checks.
(defunc bind (px name val)
:input-contract ...
:output-contract ...
...)
(check= (bind T 'A NIL) T)
(check= (bind NIL 'A T) NIL)
(check= (bind 'A 'B T) 'A)
(check= (bind 'A 'A NIL) NIL)
(check= (bind '(& (+ NIL A) (~ B) ) 'A T) '(& (+ NIL T) (~ B)))
(acl2::in-theory (acl2::disable SatisfyResultp-definition-thm))
; satisfy-remain : PropEx x LoSymbol x LoAssign -> SatisfyResult
;; Function satisfy-remain takes a propositional expression px, a list vars of
;; variables, and a list bindings of assignments to variables. The goal of
;; this function is to find assignments to all unbound variables in px such
;; that px evaluates to T. If such an assignment exists, it is returned. If no
;; such assignment exists, the function returns 'unsat.
;; This can be accomplished as follows. Let us assume that all variables
;; appearing in px are contained in vars; if we find during execution that
;; this assumption is violated, we return 'error. The function now tries all
;; possible assignments to the variables in vars (which, by the assumption,
;; includes all the variables unbound in px), binding the variables in px
;; according to these assignments, and checking whether any of the resulting
;; expressions evaluates to T. Specifically:
;; If vars is empty, we have no more variables to assign. Now evaluate px,
;; using one of the evaluation functions defined earlier. There are 3
;; different outcomes; for each of these decide what the return value of
;; satisfy-remain should be.
;; If vars is not empty, pick the first variable v in it (which we assume is
;; an unbound variable of px). Assign T to v in px, using one of the functions
;; defined above. We have now one unassigned variable fewer in px; use a
;; suitable recursive call to satisfy-remain to check for satisfiability of
;; the remaining expression (where v no longer occurs unbound).
;; If this succeeds, you are done. If this does not succeed, your only hope to
;; find a satisfying assignment is to try to assign F (nil) to v. Do that, and
;; recur, using a very similar recursive call as before.
; Write at least ten checks.
(defunc satisfy-remain (px vars bindings)
:input-contract ...
:output-contract ...
...)
(check= (satisfy-remain T '() '((A T))) '((A T)))
(check= (satisfy-remain NIL '() '((A T))) 'unsat)
(check= (satisfy-remain '(& A B) '(A B) '()) '((B T) (A T)))
(check= (satisfy-remain '(& A B) '(A) '()) 'error)
; Function (satisfy px) is just a user-friendly wrapper around
; satisfy-remain that initializes satisfy-remain's arguments appropriately.
; The goal of satisfy is to find a satisfying assignment (a binding) to the
; variables in px if one exists, or return 'unsat.
; The following useful theorem should go through automatically.
(defthm loassignp-satisfyresultp
(implies (loassignp x)
(satisfyresultp x)))
; This is a one-liner! Use existing functions to gather all the variables in
; the expression 'px', and initialize the binding list of satisfy-remain as
; needed.
; Write at least five checks.
(defunc satisfy (px)
:input-contract ...
:output-contract ...
...
)
; Notice that satisfy should never return 'error. Use acl2::test? to check
; this conjecture. Remember to add appropriate hypothesis.
(acl2::test?
(implies ...
...))
; Now use the satisfy function to find a satisfying assignment to the
; Classification problems in the Homework 4. First write the expressions
; in the problem in the form required by the data-definition of PropEx.
; Then use the function 'satisfy' to find a satisfying assignment.
; isvalid : PropEx -> SatisfyResultp
; (isvalid px) uses the above function satisfy to determine whether
; expression px is valid.
; This is a small non-recursive function. Do not write a validity checker
; from scratch!
;
; Write at least five tests.
(defunc isvalid (px)
:input-contract ...
:output-contract ...
... )
; Now use the function 'isvalid' to determine validity of the Word
; problems in the Homework 4. First write the expressions in the problem
; in the form required by the data-definition of PropEx. Then use the
; function 'isvalid' to report 'valid or provide a falsifying assignment.
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Decimal to binary conversion
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; In the last homework we have seen how to build an adder for integers.
; Unfortunately, the integers had to be written in binary, for instance 8
; in the form 1000. Of course, this conversion is easy to automate, in both
; directions. And we can even use ACL2 to test that converting to and from
; binary notation gives us the original integer back.
; In fact, later in the class we will be able to _prove_ that, but you
; don't need to do that in this homework.
; We begin with a few simple data definitions.
(defdata digit (oneof 1 0))
; Write three tests (one negative, two positive) involving the recognizer
; for this datatype, digitp.
...
(defdata digitlist (listof digit))
; Write three tests (one negative, two positive) involving the recognizer
; for this datatype, digitlistp.
...
; The following theorems will help ACL2s reason about digitlists.
(defthm digitlist-append
(implies (and (digitlistp l1)
(digitlistp l2))
(digitlistp (acl2::append l1 l2))))
(defthm digitlist-rev
(implies (digitlistp l)
(digitlistp (rev l))))
(defthm digitlist-tlp
(implies (digitlistp l)
(acl2::true-listp l))
:rule-classes (:forward-chaining :rewrite))
; power : Nat x Nat -> Nat
; (power n e) computes n raised to power e
; Write 4 more tests.
(defunc power (n e)
:input-contract ...
:output-contract ...
...
)
(check= (power 0 0) 1)
(check= (power 3 1) 3)
; Function evenp is a recognizer for even numbers.
; As a recognizer, evenp should take _anything_ as input (not just
; numbers), and return a boolean. It should return t if the input
; is an even integer and nil otherwise.
(defunc evenp (n)
:input-contract ...
:output-contract ...
...
)
; Now our first conversion function:
; digitlist2dec : Digitlist -> Nat
; (digitlist2dec l) takes a list of digits (zeros and ones), interprets them as
; an integer in binary notation, and converts this integer into decimal notation.
; The empty digitlist should be converted to 0.
; Hint: process the digitlist from left to right, accumulating the final
; decimal number on the way.
; Add 5 more test cases.
(defunc digitlist2dec (l)
:input-contract ...
:output-contract ...
...
)
(check= (digitlist2dec '()) 0)
(check= (digitlist2dec '(1 1 0 1)) 13)
(check= (digitlist2dec '(1 1 0 1 1 0 1 0 1)) 437)
; Now the inverse conversion function:
; dec2digitlist : Nat -> Digitlist
; (dec2digitlist n) takes a natural number n (which, by the definition of
; the type of natural numbers, is interpreted by ACL2 in decimal notation), and
; converts it into binary notation.
; Number 0 should be converted into the empty digitlist.
; This function is slightly more tricky: let us first define a helper
; function dec2digitlist-helper that has the exact same signature as
; dec2digitlist. The helper function processes the digits of n from right
; to left, that is, starting with the lowest-order decimal digit. Decide
; whether this digit should be translated into a 0 or a 1. Then form a cons
; of the binary digit 0 or 1 you decided on, and a list obtained from a
; suitable recursive call of the helper function.
(defunc dec2digitlist-helper (n)
:input-contract ...
:output-contract ...
...
)
; The above function pretty much does the job, except for one thing. What?
; Fix this "one thing" by defining the real dec2digitlist function, which
; calls dec2digitlist-helper and post-processes the result.
; Write 5 more test cases.
(defunc dec2digitlist (n)
:input-contract ...
:output-contract ...
...
)
(check= (dec2digitlist 8) '(1 0 0 0))
(check= (dec2digitlist 26) '(1 1 0 1 0))
; Finally, use acl2::test? to test whether converting a digitlist to
; decimal and back gives us the original result. Your conjecture should take a
; digitlist l and a natural number n, perform conjecture contract checking,
; and state that if l is the dec2digitlist conversion of n, then ...
; [complete on your own].
...
; What do you find? Do you think there is a counterexample to your
; conjecture? If so state it (whether you have found it using test? or
; not).
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
; Conjecture contract checking
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
The following conjectures are incomplete (irrespective of whether they are
true or false): they lack hypotheses that make sure the functions
involved are called only on arguments that satisfy the functions' input
contracts. Make the conjectures meaningful by adding the necessary contract
hypotheses. For example, given a conjecture c, if you think hypotheses h1
and h2 (and nothing else) are necessary to ensure the input contracts of
all functions occurring in c are satisfied, your output should be
h1 & h2 => c
The added hypotheses should be minimal. Therefore:
- do not add any hypotheses that are enforced by the output contracts of
the participating functions. For instance, if the expression (f (g x))
appears in your conjecture, and g : type1 -> type2 and f : type2 -> type3,
then do not add (type2p (g x)) as a hypothesis: this is guaranteed by the
output contract of g.
- simplify the conjecture hypotheses as much as possible. In the above
example, suppose h1 => h2 is valid (say h1 = (equal x nil) and h2 = (listp x)).
Then the conjunction h1 & h2 is equivalent to h1 ; thus, simplify your
output to
h1 => c
The examples below may contain some unknown functions (whose signature will
be provided), and known functions such as arithmetic + . The input
contracts of _all_ functions need to be enforced by the hypotheses.
1. Given
foo: List x List -> List
bar: All x List -> List
the conjecture c is
(foo (bar (/ x y) l) z) = (bar (/ y x) (foo l z))
Conjecture with hypotheses:
...
2. Consider the following two definitions, the first of which gives rise to
a recognizer natlistp:
|#
(defdata natlist (listof nat))
(defunc evenlistp (l)
:input-contract t
:output-contract (booleanp (evenlistp l))
(if (listp l)
(integerp (/ (len l) 2))
nil))
#|
For the following functions we only know the signature:
d: List -> All
m: Nat x List -> NatList
f: List -> Nat
s: EvenList -> List
the conjecture c is
(d (m x l)) = (f (s l))
Conjecture with hypotheses:
...
Now define four functions d, m, f, s (as simple as possible) with the above
signatures. The actual outputs of the functions are arbitrary, as long as
they satisfy the output contract. For example, for m, you may choose to
simply return the constant nil, which is a natlist.
|#
#|
Write an acl2::test? that tests the conjecture for your definitions.
Remember to add appropriate hypotheses. Do the function definitions satisfy
the conjecture, or there is a witness that falsifies the conjecture?
3. Given function signatures for d, m, f, s as above in 2, the conjecture c
now is
(d (m x l)) = (f (s x))
Conjecture with hypotheses:
...
Write an acl2::test? that tests the conjecture for your definitions.
Remember to add appropriate hypotheses. Do the function definitions satisfy
the conjecture, or there is a witness that falisifies the conjecture?
Explain.
4.
Come up with a conjecture that is not valid but for which you think finding
a counterexample is hard. You may only use the following functions in the
conjecture:
listp
endp
consp
first
rest
len
equal
if
and
or
implies
remove-dups
rev
append
in
PropExpp
Use acl2::test? to test your conjecture. Does ACl2s find a counterexample?
|#
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Feedback
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
#|
Please fill out the following feedback form, not as a team, but each team
member individually:
https://docs.google.com/spreadsheet/viewform?formkey=dF9HMEpYX040SVYtTkExSkppRm1QSGc6MA
Confirm here whom of the team members filled out the form:
Name 1 ...
Name 2 ...
(Name 3 ...)
Everyone who filled out the form gets credit worth 1 quiz.
The form is anonymous, to encourage you to write what you think about this
class. (If you want to stay anonymous, do not reveal your name on the
feedback form.) On the other hand, we must rely on your honesty in stating
whether you filled out the form or not, and in NOT filling out the form
several times (why would you do that??). We do not want to find
discrepancies in the number of entries on the form, and the number of
people claiming to have filled out the form.
|#