#|

CS 2800 Homework 9 - Spring 2013

Student names:

For this homework, you will be using the BEGINNER mode in ACL2s.

Instructions for using this file:

- Open this file in ACL2s as hw09.lisp. Note that only Part III. on
  TERMINATION actually requires ACL2s. Other questions are text that
  require answers as text, which must be written as ACL2s comments. This
  file already contains many comments, so you can see what the syntax is.

- Set the session mode to "BEGINNER".

- Insert your solutions into this file where indicated (for instance
  as "..."). For programming problems, this includes contracts, function
  bodies, 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.

  * 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 that your function is wrong,
    but it may also be that your check= specification is incorrect.

 - To turn in your solution, check out the directory at

  svn://dell-server-wahl-1.ccs.neu.edu/cs2800-2013-spring/09/<groupname>

  where groupname is the name of the group as it was emailed to you in the
  last homework. Your username and password remain as before.

  Place your file hw09.lisp in this directory, add it, and commit.

- Whenever convenient, we will use F and T to represent false and true, and
  the following character combinations to represent the Boolean
  connectives:

    NOT        ~

    AND        /\
    OR         \/

    IMPLIES    =>

    EQUIVALENT =
    XOR        <>

  The binding powers of these connectives are as in class: they are listed
  in the above table from highest to lowest. Within one group
  (no blank line), the binding power is the same.

|#

; I. EQUATIONAL REASONING and INDUCTION

#|

This part assumes the following definitions:

(defdata nat-list (listof nat))

(defunc scale (l n)
  :input-contract (and (nat-listp l) (natp n))
  :output-contract (nat-listp (scale l n))
  (if (endp l)
    nil
    (cons (* n (first l)) (scale (rest l) n))))

(defunc in2 (a l)
  :input-contract (listp l)
  :output-contract (booleanp (in2 a l))
  (if (endp l)
    nil
    (or (equal a (first l)) (in2 a (rest l)))))

(defunc subsetp (l1 l2)
  :input-contract (and (listp l1) (listp l2))
  :output-contract (booleanp (subsetp l1 l2))
  (if (endp l1)
    t
    (and (in2 (first l1) l2) (subsetp (rest l1) l2))))

1. Using equational reasoning, prove the following:

(and (implies (endp l)
              (equal (scale (scale l n1) n2)
                     (scale l (* n1 n2))))
     (implies (and (consp l)
                   (equal (scale (scale (rest l) n1) n2)
                          (scale (rest l) (* n1 n2))))
              (equal (scale (scale l n1) n2)
                     (scale l (* n1 n2)))))

2. Using equational reasoning, prove the following:

(and (implies (endp l)
              (subsetp l l))
     (implies (and (consp l)
                   (subsetp (rest l) (rest l)))
              (subsetp l l)))

;; In doing so, you might require a lemma: in general we need to prove any
;; conjectures we make up, only then do they become lemmas. For this question,
;; you may assume the following lemma for free (that is you don't need to prove
;; it before using it).
L1:
(implies (and (listp l1)
              (listp l2)
              (subsetp l1 l2))
         (subsetp l1 (cons a l2)))

INDUCTION

Induction Schemes

Assume you are attempting to prove a formula phi using induction. Write the
proof obligations that the induction scheme of each of the following
functions gives rise to:

3. (defunc nind (n)
 :input-contract (natp n)
 :output-contract t
  (if (equal n 0)
   0
   (nind (- n 1))))

4. (defunc del (a x)
 :input-contract (listp x)
 :output-contract (listp (del a x))
  (cond ((endp x)            nil)
        ((equal a (first x)) (del a (rest x)))
        (t                   (cons (first x) (del a (rest x))))))

5. (defunc in (a x)
 :input-contract (listp x)
 :output-contract (booleanp (in a x))
   cond ((endp x)            nil)
        ((equal a (first x)) t)
        (t                   (in a (rest x))))

6. (defunc new-sum (a b)
 :input-contract (and (natp a) (natp b))
 :output-contract (natp (new-sum a b))
     (if (equal a 0)
       0
      (+ a b)))

7. (defunc rev3 (x)
 :input-contract (listp x)
 :output-contract (listp (rev3 x))
   (if (endp x)
    nil
    (app (rev3 (rest x)) (list (first x)))))

8. (defunc fib (n)
 :input-contract (natp n)
 :output-contract (natp (fib n))
    (cond ((equal n 0)
            1)
          ((equal n 1)
            1)
          (t (+ (fib (- n 1)) (fib (- n 2))))))

Functions from induction schemes

9. Write a function such that its induction scheme gives rise to the below
proof obligations:

1. (not (listp l)) => phi
2. (listp l) /\ (endp l)  => phi
3. (listp l) /\ (not (endp l)) /\ phi|((l (rest l))) => phi

Is the above function unique (it is unique if there does not exist another
function that has the induction scheme above)? If yes, justify in English.
If no, write that function's definition in ACL2s syntax.

Proofs using induction

10a. Write a recursive function cube-n to compute the sum of cubes of the
first n natural numbers. Make your function as simple and as concise as
possible, as you will use this definition in proofs below.

(defunc cube-n (n)
  :input-contract (natp n)
  :output-contract (natp (cube-n n))
  ...

)

10b. Someone claims the following closed-form formula for the sum of cubes
of the first n natural numbers as 1^3 + ... + n^3 = n*n*(n+1)*(n+1)/4.

Prove this claim using induction. Formally, prove:

(natp n => ((cube-n n)= (n*n*(n+1)*(n+1)/4)))

Hint: Use the induction scheme of nind. Prove each of the proof obligations
arising from the induction scheme of nind using Equational reasoning, where phi
is the conjecture.

|#

; II. DEFINITIONAL PRINCIPLE

#|

 Review the Definitional Principle: course notes at
 http://www.ccs.neu.edu/course/cs2800/rapdt.pdf

For each of the definitions below, check whether it is admissible, i.e., it
satisfies the definitional principle. You can assume that f is a new
function symbol in each case, even though we use the same name f for all
functions.

If yes,

1. Provide a measure function that can be used to show termination.
2. Explain in English why the contract theorem holds.
3. Explain in English why the body contracts hold.

If no,

1. Identify which of the 6 conditions of the Definitional Principle are violated.
2. If the function is terminating, provide a measure function. Otherwise,
   provide an input that satisfies the input contract, but the function
   does not terminate on it.

1.
(defunc f (x l)
  :input-contract (and (integerp  x) (listp l))
  :output-contract (natp (f x l))
  (cond ((endp l) 0)
        ((> x 0)  (f (len l) (rest l)))
        (t        (+ (f x (rest l)) 1))))

2.
(defunc f (a b)
  :input-contract  (and (natp a) (natp b))
  :output-contract (natp (f a b))
  (cond ((and (equal a 0) (equal b 0)) 0)
        ((< a b)                       (f b a))
        (t                             (f a (- b 1)))))

3.
(defunc f (a b)
  :input-contract  (and (natp a) (natp b))
  :output-contract (natp (f a b))
  (cond ((and (equal a 0) (equal b 0)) 0)
        ((< a b)                       (f a b))
        (t                             (f b (- a 1)))))

4.
(defunc f (x y)
  :input-contract (listp y)
  :output-contract (natp (f x y))
  (cond ((endp y)  0)
        (t         (f  (len y) (x (rest y))))))

5.
(defunc f (x y)
  :input-contract (and (natp x) (natp y))
  :output-contract (booleanp(f x y))
  (cond ((equal x y) t)
         ((> x y)    (f (- x 1) y))
         (t          (f x (- y 1)))))

6.
(defunc f (a b a)
  :input-contract  (and (natp a) (natp b))
  :output-contract (natp (f a b))
  (cond
    ((and (equal a 0) (equal b 0))  0)
    ((< a b)                        (f a (- b 1)))
    (t                              (f b (- a 1)))))

7.
(defunc f (x y)
  :input-contract (and (natp x) (natp y))
  :output-contract (booleanp(f x y))
  (cond ((equal x y) t)
         ((> x y)    (f (- x 1) y))
         (t          (f y x))))

8.
(defunc f (x l)
  :input-contract (and (integerp  x) (listp l))
  :output-contract (natp (f x l))
  (cond ((endp l) 0)
        ((> x 0)  (f (len l) (rest l)))
        (t        (- (f x (rest l)) 1))))

9.
(defunc f (x y)
  :input-contract (and (natp x) (natp y))
  :output-contract (booleanp(f x y))
  (cond ((equal x y) t)
         ((> x y)    (f (- x 1) (+ y 1)))
         (t          (f (+ y 1) x))))

; III. A TERMINATION TESTER

The subject of this exercise is to study the problem of designing a
function that automatically checks whether another (recursively defined)
function terminates.

But wait -- we already know this problem is undecidable! That means there
is no ACL2 function that takes an arbitrary ACL2 function f as
input (encoded in some suitable way) and determines correctly whether f
terminates.

We will therefore only solve a simple version of this problem: our function
will determine whether a given function f terminates in a predetermined
number of "steps". We will see shortly what "steps" means.

We begin with an example.

1. Define a function f that takes a positive natural number and is defined
mathematically as follows:

         1        if n is 1
       /
f(n) = - f(n/2)   if n is even
       \
         f(3*n+1) if n is greater than 1 and odd.

Here is how to read that notation: first observe that the three cases on
the right are mutually exclusive, i.e. every positive natural number fits
into exactly one case. Given n, determine which case it fits in. The
expression associated with that case determines f(n).

Define this function in ACL2s, in :program mode. We will soon see why.

|#

:program

(defunc f (n)
  :input-contract ...
  :output-contract ...
  ...

)

; What does this function return, if anything?
;...

; Write at least 3 check= tests that (should) confirm your conjecture.

(check= (f  8) ...)
(check= (f  5) ...)
(check= (f 40) ...)

#|

You can think of this function as generating a sequence of positive natural
numbers, namely the numbers that f is called on recursively. For example:

f(8) = f(4) = f(2) = f(1) = 1

To get a feel for f, write down the call sequences for the following
initial arguments, until the recursion ends:

f(10) = f(...) = ...
f( 7) = f(...) = ...

Hint: try out (acl2::trace! f)

The reason we have defined this function in :program mode is that ACL2
cannot prove its termination. In fact, nobody knows whether this function
always terminates! You can read the whole story on Wikipedia. Search for
Collatz Conjecture.

Think about why it is (apparently) difficult to define a measure function
for f. Try it! (No response is required in your homework file.)

2. Modify f into a function f-c that takes not only n but also two other
arguments, count and limit, which are natural numbers such that count <=
limit. The idea is that count counts the number of recursive calls we have
to make to evaluate (f n). If that number exceeds limit, we abort the
entire computation and return the symbol ! (exclamation mark). Otherwise we
proceed as in f. Think about what values to pass to count and limit in
recursive calls.

f-c : Pos x Nat x Nat -> Pos union {!}

The input contract MUST enforce the arithmetic relationship between count
and limit mentioned above. The output contract MUST state that f-c returns
a positive natural number OR the symbol ! .

|#

(defunc f-c (n count limit)
  :input-contract ...
  :output-contract ...
  ...

)

(check= (f-c 8 0 2) '!)
(check= (f-c 8 0 3) '!)
(check= (f-c 8 0 4)  1)

; Write at least 3 more tests.

#|

3. Define a function f-terminates that takes two arguments: a positive
natural n and a natural number limit, and checks whether (f n) returns
after at most limit recursive calls. f-terminates returns t or nil.
Obviously, in the body of f-terminates use f-c instead of f .

f-terminates : Pos x Nat -> Bool

|#

(defunc f-terminates (n limit)
  :input-contract ...
  :output-contract ...
  ...)

(check= (f-terminates 8 2) nil)
(check= (f-terminates 8 3) nil)
(check= (f-terminates 8 4) t)

; Write at least 3 more check= tests

#|

4. Find the number *limit* of recursive calls that it takes for f to
terminate on input

1267650600228229401496703205376

That is, the following two tests must pass with your number *limit*,
which you should enter in place of the ... below:

|#

(defconst *limit* ...)

(check= (f-terminates 1267650600228229401496703205376 (- *limit* 1)) nil)
(check= (f-terminates 1267650600228229401496703205376    *limit*   ) t  )

#|

Hint: to determine *limit*, consider the trace mechanism mentioned above,
or binary search for the optimal parameters to f-c.

What is the mathematical relationship between the (large) input to f shown
above, and the number *limit* you found? Answer and explain in English.

*limit* is ...

5. Remember that f may not terminate on all inputs: nobody has been able to
prove that it does. Now observe that function f-terminates itself always
does terminate, even if f does not! The reason is that, instead of f, we
are using f-c within f-terminates, and f-c only recurs a given number of
times.

We can therefore use ...-terminates to test termination of functions even if
we _know_ they do not terminate. Consider:

|#

(acl2::acl2s-defaults :set acl2::testing-enabled nil) ; this turns off contract testing

(defunc g (n)
  :input-contract (integerp n)
  :output-contract (integerp (g n))
  (if (equal n 0)
    0
    (+ 1 (g (- n 1)))))

#|

This function behaves like the identity on natural number inputs, and
diverges on all others. Try (g 10), (g 0), (g -1). What does ACL2 return on
the final example?

Now modify g into a function g-c that relates to g like f-c does to f. That
is, g-c counts the number of recursive calls we have to make to evaluate (g
n). If that number exceeds a given limit, we abort the entire computation and
return the symbol ! (exclamation mark).

g-c : Int x Nat x Nat -> Int union {!}

This function is a bit more tricky than f, as it is not tail-recursive!
'let' is your friend.

|#

(defunc g-c (n count limit)
  :input-contract ...
  :output-contract ...
  ...

)

#|

Now define a similar wrapper function g-terminates that tests termination
of g within a pre-specified number of recursive calls. In the body of
g-terminates use g-c instead of g .

g-terminates : Int x Nat -> Bool

|#

(defunc g-terminates (n limit)
  :input-contract ...
  :output-contract ...
  ...)

(check= (g-terminates 10 10)  nil)
(check= (g-terminates 10 11)  t)
(check= (g-terminates -1 10)  nil) ; g does not terminate at all on this input
(check= (g-terminates -1 100) nil) ; g does not terminate at all on this input

; Write 2 more check= tests

#|

6. How would you modify a function that has several recursive calls, like
fib shown below, in a manner analogous to what we did to f, with arguments
count and limit, such that evaluation is aborted when count reaches limit?

(defunc fib (n)
  :input-contract (natp n)
  :output-contract (natp (fib n))
  (if (<= n 1)
    1
    (+ (fib (- n 1)) (fib (- n 2)))))

Explain in plain English. You don't need to write function code.

...

###################################################################################

Some final comments (no response required): In this exercise, for every
function f we wanted to termination-test, we had to write a new function
f-terminates. Wouldn't it be better to have a function terminatesp that
takes (the code of) another function as input and performs the steps above?
so we don't have to write another function ?-terminates every time, which
anyway differs from the others mostly in the name of the function that is
being tested?

Yes, that would be better. But there are a number of difficulties. An
obvious one is that the different functions we want to test may take
different numbers of arguments, and may return different types of values.
So how many arguments would terminatesp have? and what would be their
types? Not obvious.

Supporting such "generic" terminatesp functions requires quite heavy
programming language support, such as higher-order functions: functions
that take other functions as input and can run them on arbitrary arguments.
As we have often mentioned, ACL2 does not support higher-order functions,
since they make proving theorems much much harder.

Note that a true termination prover would have to be a higher-order
procedure, since it takes another procedure/function as input.

|#

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Feedback
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

#|

Please fill out the following form:

https://docs.google.com/spreadsheet/viewform?formkey=dDhMZjZpcGlRaFRveEV0UUlNdUJqMVE6MA

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