Untitled

#|<html><head></head><body><pre style="word-wrap: break-word; white-space: pre-wrap;">#|

CS 2800 Homework 2 - Spring 2018

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 hwk2.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.

- 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 hwk2.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.

Since this is our first programming exercise, we will simplify the interaction
with ACL2s somewhat. Instead of requiring ACL2s to prove termination and
contracts, we allow ACL2s to proceed even if a proof fails.  However, if a
counterexample is found, ACL2s will report it.  See section 2.17 of the lecture
notes for more information.  This is achieved using the following directives (do
not remove them):

|#

(set-defunc-termination-strictp nil)
(set-defunc-function-contract-strictp nil)
(set-defunc-body-contracts-strictp nil)

#|

 Part I:
 Function definitions.

 In this part, you will be given a set of programming exercises. Since you
 already took a fantastic course on programming (CS2500), the problems are not
 entirely trivial. Make sure you give yourselves enough time to develop
 solutions and feel free to define helper functions as needed.

|#

#|
Define the function rr.
rr: List x Nat -&gt; List

(rr l n) rotates the list l to the right n times.
|#

;(defunc rr (l n)
 ; :input-contract
  ;:output-contract
  ;)

;(check= (rr '(1 2 3) 1) '(3 1 2))
;(check= (rr '(1 2 3) 2) '(2 3 1))
;(check= (rr '(1 2 3) 3) '(1 2 3))

#|
Define the function err, an efficient version of rr.
err: List x Nat -&gt; List

(err l n) returns the list obtained by rotating l to the right n times
but it does this efficiently because it actually never rotates more than
(len l) times.
You can use acl2::mod in your answer. For example (acl2::mod 11 3) = 2
because 11 mod 3 = 2.
|#

#| (defunc err (l n)
  :input-contract
  :output-contract
  )
|#
#|
(check= (err '(1 2 3) 1) '(3 1 2))
(check= (err '(1 2 3) 2) '(2 3 1))
(check= (err '(1 2 3) 3) '(1 2 3))
|#
#|
Make sure that err is efficient by timing it with a large n
and comparing the time with rr.

Replace the 's in the string below with the times you
observed.
|#
#|
(acl2::time$ (rr '(a b c d e f g) 10000000))
(acl2::time$ (err '(a b c d e f g) 10000000))

"rr took  seconds but err took  seconds"
|#
;; Here is a data definition for a list of Booleans. See Section 2.14 of the
;; lecture notes.

(defdata lob (listof boolean))

;; For example

(check= (lobp '(t nil t)) t)
(check= (lobp '(nil 1 t)) nil)

#|
We can use list of Booleans to represent natural numbers as follows.
The list

(nil nil t)

corresponds to the number 4 because the first nil is the "low-order"
bit of the number which means it corresponds to 2^0=1 if t and 0
otherwise. The next Boolean corresponds to 2^1=2 if t and 0 otherwise
and so on. So the above number is:

0 + 0 + 2^2 = 4.

As another example, 31 is

(t t t t t)

or

(t t t t t nil nil)

or

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 (n)
  :input-contract (natp n)
  :output-contract (lobp (n-to-b n))
    (cond
     ((equal n 0) ())
     ((equal n 1) (cons t ()))
     ((equal (acl2::mod n 2) 0) (cons nil (n-to-b (/ n 2))))
     (t (cons t (n-to-b (/ (- n 1) 2))))))

(check= (n-to-b 24) '(nil nil nil t t))
(check= (n-to-b 10) '(nil t nil t))
(check= (n-to-b 7) '(t t t))
(check= (n-to-b 4) '(nil nil t))
(check= (n-to-b 31) '(t t t t t))
(check= (n-to-b 0) ())

#|
Define the function b-to-n that given a list of Booleans, returns
the natural number corresponding to that list.
|#

(defunc b-to-n (l)
  :input-contract (lobp l)
  :output-contract (natp (b-to-n l))
  (cond
   ((endp l) 0)
   ((equal (first l) t) (+ 1 (* 2 (b-to-n (rest l)))))
   ((equal (first l) nil) (* 2 (b-to-n (rest l))))))


(check= (b-to-n '(nil t nil t)) 10)
(check= (b-to-n '(t t t)) 7)
(check= (b-to-n '(nil nil t)) 4)
(check= (b-to-n '(t t t t t)) 31)
(check= (b-to-n ()) 0)

#|

The permutations of a list are all the list you can obtain by swapping any two
of its elements. For example, starting with the list

(1 2 3)

I can obtain

(3 2 1)

by swapping 1 and 3.

So the permutations of (1 2 3) are

(1 2 3) (1 3 2) (2 1 3) (2 3 1) (3 1 2) (3 2 1)

Notice that if the list is of length n and all of its elements are distinct, it
has n! (n factorial) permutations.

Given a list, say (a b c d e), we can define any of its permutations using a
list of *distinct* positive integers from 1 to the length of the list, which
tell us how to reorder the elements of the list.  Let us call this list of
distinct positive integers an arrangement.  For example applying the
arrangement (5 1 3 2 4) to the list (a b c d e) yields (e a c b d).

Define the function find-arrangement that given two lists, either returns nil if
they are not permutations of one another or returns an arrangement such that
applying the arrangement to the first list yields the second list. Note that if
the lists have repeated elements, then more than one arrangement will work. In
such cases, it does not matter which of these arrangements you return.

|#
(defunc member (a b)
  :input-contract (and t (listp b))
  :output-contract (booleanp (member a b))
  (cond
   ((endp b) nil)
   ((listp b) (if (equal a (first b)) t
                (member a (rest b))))))

(check= (member "h" '(a b c)) nil)
(check= (member 'x '(x y z)) t)
(check= (member () (cons () ())) t)
(check= (member nil '(nil t nil)) t)


(defunc remover (a b)
  :input-contract (and t (listp b))
  :output-contract (listp (remover a b))
  (cond
   ((endp b) b)
   (t (if (equal a (first b))
               (rest b)
               (cons (first b) (remover a (rest b)))))))

(check= (remover 1 '(1 2 3)) '(2 3))
(check= (remover 5 '(4 1 5 8)) '(4 1 8))
(check= (remover 8 '(1 2 3)) '(1 2 3))


(defunc permhelper (a b)
  :input-contract (and (listp a) (listp b))
  :output-contract (booleanp (permhelper a b))
  (cond
   ((not (equal (len a) (len b))) nil)
   ((and (endp a) (endp b)) t)
   ((or (endp a) (endp b)) nil)
   ((endp (rest a)) (member (first a) b))
   (t
    (if
      (member (first a) b)
      (permhelper (rest a) (remover (first a) b))
       nil))))

(check= (permhelper '(1 2 3) '(2 3 1)) t)
(check= (permhelper '(5 1 3) '(2 3 1)) nil)
(check= (permhelper '(5 1 3 6 7) '(2 3 1 1)) nil)
(check= (permhelper () '(2 3 1)) nil)
(check= (permhelper '(1 2 3) '(1 2 3 4)) nil)
(check= (permhelper '(1 2 3 4) '(1 2 3)) nil)

(defunc replacer (x y)
  :input-contract (and t (listp y))
  :output-contract (listp y)
  (cond
   ((not (member x y)) y)
   ((equal x (first y)) (cons () (rest y)))
   (t (cons (first y)(replacer x (rest y))))))

(check= (replacer 0 '(1 2 3)) '(1 2 3))
(check= (replacer 0 '(1 0 2)) '(1 () 2))
(check= (replacer 0 '(0 1 2)) '(() 1 2))
(check= (replacer 0 '(0 1 0)) '(() 1 0))
(check= (replacer 1 '(0 1 0)) '(0 () 0))
(check= (replacer 5 '(3 1 5)) '(3 1 ()))

(defunc positionhelper (x y)
  :input-contract (and t (listp y))
  :output-contract (natp (positionhelper x y))
  (cond
   ((endp y) 0)
   ((equal x (first y)) 1)
   ((not (member x y)) 0)
   (t (+ 1 (positionhelper x (rest y))))))

(check= (positionhelper 1 '(1 2 3)) 1)
(check= (positionhelper 1 ()) 0)
(check= (positionhelper 2 '(3 1 2)) 3)

(defunc generate (x y)
  :input-contract (and (listp x) (listp y))
  :output-contract (listp (generate x y))
  (cond
   ((endp x) ())
   (t (cons (positionhelper (first x) y) (generate (rest x) (replacer (first x) y))))))

(check= (generate '(a b c) '(a c b)) '(1 3 2))
(check= (generate () '(a a)) ())

(defunc find-arrangement (x y)
  :input-contract (and (listp x) (listp y))
  :output-contract (listp (find-arrangement x y))
  (cond
   ((permhelper x y) (generate x y))
   (t nil)))


(check= (find-arrangement '(a b c) '(a b b)) nil)
(check= (find-arrangement '(a b c) '(a c b)) '(1 3 2))
(check= (find-arrangement '(a a) '(a a)) '(1 2))
;; in the above check= you can use '(2 1) instead of '(1 2) if you wish
;; since both arrangements work


#|

 Part II:
 Exploring the ACL2s language.

 In this section, we are going to explore the ACL2s language as defined in the
 lecture notes. We are going to revisit some of the decisions made and we will
 consider certain "what if" scenarios. Make sure you read and understand the
 lecture notes really well.

|#

#|

The built-in functions introduced in Section 2.2 are if and equal.
Without using if, but using equal, booleanp and the constants, which
of the following functions can you define?

and, implies, or, not, iff, xor

For each of the functions you can define, provide a definition using
the names

band, bimplies, bor, bnot, biff, bxor

If you cannot define one of the above functions, you do not need to do
anything.

The restriction on not using if applies only to the body of your function
definitions. You can use all the functions in the lecture notes (including
booleanp, if and and) for the input and output contracts.

|#


#|
Consider the following function definition.
|#

(defunc iif (a b c)
  :input-contract (booleanp a)
  :output-contract t
  (if a b c))

#|
This is accepted by ACL2s. Suppose I define iif. Is it the case
that I can always use iif instead of if for subsequent function
definitions? Explain why or why not.

 (replace this line with your explanation, in English)

|#

#|
In the lecture notes, unary-- was provided as a built-in function.
Explain why it is required or show that it is not really required.

When we say that unary-- is required, we mean that you cannot define
it in the ACL2s language (Bare Bones mode) using the built-in
functions in the lecture notes upto the end of Section 2.5, except
that you cannot use unary-- (obviously). You can define helper
functions, if needed.

If you think it is really required, then argue that it allows you to
do things that the other built-in functions do not. You do not need a
proof here, just a good argument in English.

If you think it is not required, show how to define it using the other
built-in functions.  Do this by providing a definition of my-unary--
that only uses the other built-in functions (except unary--) or
functions defined based on the other built-in functions.
You will do this in Beginner mode, as per the instructions above.

|#

 (the definition of my-unary-- goes here or a comment with an argument)

#|

In the lecture notes, unary-/ was provided as a built-in function.
Explain why it is required or show that it is not really required.
Follow the instructions for unary--.

|#

 (the definition of my-unary-/ goes here or a comment with an argument)

#|

In the lecture notes, integerp was provided as a built-in function.
Explain why it is required or show that it is not really required.
Follow the instructions for unary--.

|#

 (the definition of my-integerp goes here or a comment with an argument)

#|
In the lecture notes, denominator was provided as a built-in function.
Explain why it is required or show that it is not really required.
Follow the instructions for unary--.
|#

 (the definition of denominator goes here or a comment with an argument)

</pre></body></html>