#|

CS 2800 Homework 1 - 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 hwk01.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.

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)

#| 
 Function definitions with contracts.

 You already took a fantastic course on programming (CS2500), and have
 seen how to define functions in a functional programming style. One
 new thing in CS2800 is contracts.  The goal of this homework is to
 get you use to writing functions with contracts.  Make sure you give
 yourselves enough time to develop solutions and feel free to define
 helper functions as needed.
|# 

#|
Define the function addnat that adds two natural numbers.  The
signature of the function is given:

addnat: Nat x Nat -> Nat
|#

(definec addnat ...

(check= (addnat 1 2) 3)
... add more tests ...

#|
Stop and think: what should happen if you try the following?

(check= (addnat -1 2) 1)

Why should this happen?  Try it in ACL2s and confirm that this is indeed what happens.

... enter your answer here ...

|#

#|
Define the function addposnat that adds two positive (non-zero) natural numbers.

The input contracts should require that the arguments are positive integers.

|#

(definec addposnat ...

(check= (addposnat 1 2) 3)
...

#|
 Define the function list-delete, which consumes a list l and a number i and 
 deletes the ith element from l. i must be a number between 0 (inclusive)
 and the length of l (exclusive). Can list-delete deal with empty lists? 
 You may have to use defunc instead of definec. Do not forget to add
 tests!

 You can only use cons, equal, rest, first, len, arithmetic, ...,
 recognizers, boolean operators, but nothing else. 

 In the output contract specify the type of the output and also 
 (using and) the relationship between the length of the list returned
 by list-delete and l.

|#

(defunc list-delete (l i)
  :input-contract ...
  :output-contract ...
  ...

(check= (list-delete '(1) 0) '())
(check= (list-delete '(1 2 3) 2) '(1 2))
(check= (list-delete '(1 2 3) 1) '(1 3))

#|
Consider the following definitions:
|#

(definec number-but-not-42-v1 (x :all) :bool
  (and (rationalp x)
       (not (equal x 42))))

(definec number-but-not-42-v2 (x :rational) :bool
  (not (equal x 42)))

#|
Explain how the two definitions differ. Provide some test cases that illustrate
this difference.

... enter answer here ...
|#

#|
Consider this piece of code:

(defunc a-function-that-likes-numbers-except-42 (x)
  :input-contract (number-but-not-42 x)
  :output-contract ...
  ... )

  Which version of number-but-not-42 should the above function use in its
  input contract? Why isn't the other version correct to use?
  
... enter answer here ...

  Call the above versions "correct" and "incorrect". Let's assume that only the
  "incorrect" one is available. Can you still use this version in the contract
  of a-function-that-likes-numbers-except-42 so that the overall behavior is 
  correct? (Hint: you would need to strengthen the contract somehow.)
  
... enter answer here ...

|#

#|

 Define the function avg which computes the average (mean) of a list
 of rational numbers. Do not forget that the list might be empty!
 There are several ways to deal with such a situation (forbid it using
 contracts, allow it but deal with it somehow, etc.). To specify that
 the input must be a list of numbers, first define helper functions
 that you can then use in the contracts.

|#

... define helper functions ...

(defunc avg (nl)
  :input-contract ...
  :output-contract ...
  ...
  
(check= (avg '(1 2 3)) 2)
...

#|
Identify an invariant that must hold at a certain location in your
implementation of avg. Call this invariant I, define what I is (i.e.,
what is the boolean condition that I corresponds to) and label your
code with {I} to show where exactly in the program I must hold true.

... enter answer here ...

|#

#|

Recall the definitions of true-listp, listp, endp and app.

(definec listp (x :all) :bool
  (or (consp x)
      (equal x nil)))

(definec endp (x :list) :bool
  (not (consp x)))

(definec true-listp (x :all) :bool
  (if (consp x)
      (true-listp (rest x))
    (equal x nil)))

(definec app (x :tl y :tl) :tl
  (if (endp x)
      y
    (cons (first x) (app (rest x) y))))

This exercise will require you to use what you learned solving
recurrence relations from discrete.

We will explore the difference between static and dynamic
type checking. 

A. What is the computational complexity of listp?

B. What is the computational complexity of endp?

C. What is the computational complexity of true-listp?

D. What is the computational complexity of app?

To answer the above questions, we will assume that the following
operations have a cost of 1:

 cons, first, or, rest, equal, consp, not, if

We will also assume for this first set of questions that static
contract checking is used.  With static contract checking, ACL2s
checks that the arguments to the function satisfy their contract only
once, for the top-level call. For example, if you type:

(app '(1 2 3 4) '(5 6))

ACL2s checks that '(1 2 3 4) and '(5 6) are both true-lists and no
other contracts.

Remember also that we want the worst-case complexity.
So if the function has an if-then-else, you must compute separately
the complexity of the then branch, the else branch, and then take
the worst case (i.e., the maximum), plus the complexity of the if
condition itself.

To get you going, we will give the complexity of listp as an example.
Checking the contract statically takes no time, since the type of
x is :all. 
Independently of the size of x, there are 3 operations: (consp x),
(equal x nil), and the or. So the complexity is O(3)=O(1), that is,
constant time. 

ANSWER B: ...

ANSWER C: ...

ANSWER D: ...

Once way of implementing dynamic checking is to have every function
dynamically check their input contracts. Think about how you might do
that before reading further. So, the above definitions get transformed
into the following. In essence, we are forcing contract checking to
happen dynamically, during runtime.

(definec listp (x :all) :bool
  (or (consp x)
      (equal x nil)))

(definec endp (x :list) :bool
  (if (listp x)
      (not (consp x))
    (error)))

(definec true-listp (x :all) :bool
  (if (consp x)
      (true-listp (rest x))
    (equal x nil)))

(definec app (x :tl y :tl) :tl
  (if (and (true-listp x) (true-listp y))
      (if (endp x)
          y
        (cons (first x) (app (rest x) y)))
    (error)))

What is the computational complexity of the above modified functions?
You can assume that error has cost 1.

ANSWER A: ... 

ANSWER B: ...

ANSWER C: ...

ANSWER D: ...

|#