Solutions to Problem Set 7
==========================

Written by Paul Hudak in literate Haskell style.
October 27, 2004


1. Exercise 14.2 in SOE, but, as before, only for the 2nd fold law in
   Table 11.1, and the third take/drop law in Table 11.2.  If the
   property does not hold for infinite lists, state so, and why.

"Prove as many of the properties in Tables 11.1 and 11.2 as you can,
for infinite lists."

Solution:

Recall the 2nd fold law.

  If the following are true:

  x `op1` (y `op2` z) = (x `op1` y) `op2` z       (1)
  x `op1` e = e `op2` x                           (2)

  then for all finite xs:

  foldr op1 e xs = foldl op2 e xs

In a previous assignment we proved this for finite xs.  Now we need to
show that this holds for INFINITE lists as well.

The base case is xs = _|_:
foldr op1 e _|_
=> _|_                  -- unfold foldr
=> foldl op2 e xs       -- fold foldl

The induction step is just as we did previously (where + and * are
used for op1 and op2, respectively).

Induction step (xs=x:xs):
foldr (+) e (x:xs)
=> x + foldr (+) e xs           -- unfold foldr
=> x + foldl (*) e xs           -- ind hyp
=> foldl (*) (x+e) xs           -- Lemma
=> foldl (*) (e*x) xs           -- aux (2)
foldl (*) e (x:xs)              -- unfold foldl

But this requires proving the Lemma for infinite lists too.

Lemma: 
If   x + (y * z) = (x + y) * z                  (1) -- same as above
then x + foldl (*) a xs = foldl (*) (x+a) xs

Proof: 

Base case (xs = _|_):
x + foldl (*) a _|_
=> x + _|_                      -- unfold foldl

but now we are stuck, because x + _|_ is not the same as:

foldl (*) (x+a) _|_  =>  _|_

unless + is strict in its second argument.  If we make that assumption
then the base case holds, as does the induction step, as before:

Induction step (xs=x':xs):
x + foldl (*) a (x':xs)
=> x + foldl (*) (a * x') xs    -- unfold foldl
=> foldl (*) (x + (a*x')) xs    -- ind hyp
=> foldl (*) ((x+a) * x') xs    -- aux (1)
=> foldl (*) (x+a) (x':xs)      -- fold foldl

Conclusion: the original law does NOT hold for infinite lists.  A
counter example is the following:

...

However, if we add the constraint that op1 is strict in its second
argument, then it DOES hold.

QED

Recall now the third take/drop law:

  For all finite non-negative m and n, and finite xs:
      drop m . drop n = drop (m + n)
  where:
      drop 0 xs = xs
      drop _ [] = []
      drop n (_:xs) | n > 0 = drop (n-1) xs
      drop _ _ = error "PreludeList.drop: negative argument"

To prove this for infinite lists, we note that the previous proof was
an induction on "n", and not "xs".  It is repeated here:

Base case (n=0):
(drop m . drop 0) xs
=> drop m (drop 0 xs)           -- unfold (.)
=> drop m xs                    -- unfold drop

Induction step (n=n+1, x=[]):
(drop m . drop (n+1)) []
=> drop m (drop (n+1) [])       -- unfold (.)
=> drop m []                    -- unfold drop
=> []                           -- unfold drop
=> drop (m+(n+1)) []            -- fold drop

Induction step (n=n+1, x=x:xs):
(drop m . drop (n+1)) (x:xs)
=> drop m (drop (n+1) (x:xs))   -- unfold (.)
=> drop m (drop n xs)           -- unfold drop
=> (drop m . drop n) xs         -- fold (.) 
=> drop (m+n) xs                -- ind hyp
=> drop ((m+n)+1) (x:xs)        -- fold drop
=> drop (m+(n+1)) (x:xs)        -- associativity

For the case xs = _|_, we need to consider whether or not m=0 or n=0,
which leads to three base cases:

Base case (xs = _|_, n = 0):
(drop m . drop 0) _|_
=> drop m (drop 0 _|_)
=> drop m _|_
=> drop (m + 0) _|_

Base case (xs = _|_, m = 0):
(drop 0 . drop n) _|_
=> drop 0 (drop n _|_)
=> drop n _|_
=> drop (0 + n) _|_

Base case (xs = _|_, m /= 0, n /= 0):
(drop m . drop n) _|_
=> drop m (drop n _|_)
=> drop m _|_
=> _|_
=> drop (m+n) _|_

Conclusion: this law DOES hold for infinite lists.

QED


2. Exercise 14.3 in SOE.
       
"Prove that fib n = fibs !! n for all n >= 0."

Solution:

Recall the definitions of fib and fibs:

  fib 0 = 1
  fib 1 = 1
  fib n = fib (n-1) + fib (n-2)

  fibs = 1 : 1 : zipWith (+) fibs (tail fibs)

There are two base cases:

Base case (n=0):
fib 0
=> 1            -- unfold fib
=> fibs !! 0    -- fold (!!)

Base case (n=1):
fib 1
=> 1            -- unfold fib
=> fibs !! 1    -- fold (!!)

For the induction step, assume that the property is true for n and
n+1, and prove that it's true for n+2:
fib (n+2)
=> fib (n+1) + fib n             -- unfold fib
=> (fibs !! (n+1)) + (fibs !! n) -- ind hyp
=> fibs !! (n+2)                 -- Lemma 1

Lemma 1 is:
fibs (n+2)  =  (fibs !! (n+1)) + (fibs !! n)

Proof:

Base case (n=0):
fibs !! (0+2)
fibs !! 2
=> 2
=> 1 + 1
=> (fibs !! 1) + (fibs !! 0)
=> (fibs !! (0+1)) + (fibs !! 0)

Induction step (n=n+1):
fibs !! (n+1+2)  
=> fibs !! (n+3)                                          -- arithmetic
=> (1 : 1 : zipWith (+) fibs (tail fibs)) !! (n+3)        -- unfold fibs
=> zipWith (+) fibs (tail fibs) !! (n+1)                  -- unfold (!!)
=> (fibs !! (n+1)) + ((tail fibs) !! (n+1))               -- Lemma 2
=> (fibs !! (n+1)) + ((1 : tail fibs) !! (n+1+1))         -- fold (!!)
=> (fibs !! (n+1)) + ((1 : 1 : zipWith (+) fibs (tail fibs)) !! (n+1+1))
                                                          -- unfold tail
=> (fibs !! (n+1)) + (fibs !! (n+1+1))                    -- fold fibs
=> (fibs !! (n+1+1)) + (fibs !! (n+1))                    -- commutativity

Lemma 2: if op is strict, and xs and ys are infinite, then
         zipWith op xs ys !! n = (xs!!n) `op` (ys!!n)

Base case (xs=_|_):
zipWith op _|_ ys !! n
=> _|_ !! n                                     -- unfold zipWith
=> _|_                                          -- unfold (!!)
=> _|_ `op` (ys!!n)                             -- op is strict
=> (_|_!!0) `op` (ys!!n)                        -- fold (!!)

Induction step (xs=x:xs, ys=y:ys, n=0)
zipWith op (x:xs) (y:ys) !! 0
=> ((x `op` y) : zipWith op xs ys) !! 0         -- unfold zipWith
=> x `op` y                                     -- unfold (!!)
=> ((x:xs) !! 0) `op` ((y:ys) !! 0)             -- fold (!!)

Induction step (xs=x:xs, ys=y:ys, n=n+1)
zipWith op (x:xs) (y:ys) !! (n+1)
=> ((x `op` y) : zipWith op xs ys) !! (n+1)     -- unfold zipWith
=> zipWith op xs ys !! n                        -- unfold (!!)
=> (xs!!n) `op` (ys!!n)                         -- ind hyp
=> ((x:xs)!!(n+1)) `op` ((y:ys)!!(n+1))         -- fold (!!)

QED


3. Exercise 14.5 in SOE.

"Show that `cycle' is the identity function on infinite lists.
I.e., show that for any infinite list `lst', cycle lst == lst."

Recall the definition of cycle:

  cycle [] = error "Prelude.cycle: empty list"
  cycle xs =  xs' where xs' = xs ++ xs'

Solution:

Base case (lst=_|_):
cycle _|_
=> _|_          -- unfold cycle

Induction step (lst=x:xs):
cycle (x:xs)
=> xs' where xs' = (x:xs) ++ xs'        -- unfold cycle
=> xs' where xs' = (x:xs)               -- Lemma
=> x:xs                                 -- semantics of where

Lemma: if xs is infinite, then xs ++ ys = xs.

Proof:

Base case (xs=_|_):
_|_ ++ ys
=> _|_

Induction step (xs=x:xs):
(x:xs) ++ ys
=> x : (xs ++ ys)               -- unfold (++)
=> x:xs                         -- ind hyp

QED


4. A mutable variable, or reference, in Haskell might have the
   following interface:
       
   newRef :: a -> IO (Ref a)
   setRef :: Ref a -> a -> IO ()
   getRef :: Ref a -> IO a
       
   For example, here's a program that creates a reference with an
   initial value of 42, then adds it to itself, finally printing out
   the final value:
       
   do r <- newRef 42
      v <- getRef r
      setRef r (v+v)
      v' <- getRef r
      print v'
       
   Define these three functions using first-class channels in Haskell.
   You should use good abstraction techniques to make the
   implementation completely opaque to the user.

Solution:

> module PS7 (Ref, newRef, setRef, getRef) where

Note that the Ref type is exported, BUT NOT ITS CONSTRUCTORS.
This makes it an "abstract type".

> import Channel

Define Ref as a newtype that hides the Chan implementation:

> newtype Ref a = Ref (Chan a)

A Ref will be implemented as a channel that will always have exactly
one value written into it, namely the contents of the Ref:

> newRef :: a -> IO (Ref a)
> newRef x =         do c <- newChan
>                       writeChan c x
>                       return (Ref c)
>
> setRef :: Ref a -> a -> IO ()
> setRef (Ref c) x = do readChan c
>                       writeChan c x
>
> getRef :: Ref a -> IO a
> getRef (Ref c) =   do x <- readChan c
>                       writeChan c x
>                       return x

Test:

> main = do r <- newRef 42
>           v <- getRef r
>           print v
>           setRef r (v+v)
>           v' <- getRef r
>           print v'