Solutions to Problem Set 4
==========================

Written by Paul Hudak
October 7, 2004

1. Exercise 11.1 in SOE.

"From Chapter 5, prove that (a) putCharList cs = map putChar cs,
and that (b) listProd xs = fold (*) 1 xs, for all finite lists
cs and xs."

Solution:

(a) putCharList cs = map putChar cs, where:

    putCharList []     = []
    putCharList (c:cs) = putChar c : putCharList cs

Base case (cs=[])
putCharList [] 
=> []                                   -- unfold putCharList
=> map putChar []                       -- fold map

Induction step (cs=c:cs):
putCharList (c:cs) 
=> putChar c : putCharList cs           -- unfold outCharList
=> putChar c : map putChar cs           -- ind hyp
=> map putChar (c:cs)                   -- fold map

(b) listProd xs = fold (*) 1 xs, where:

    listProd [] = 1
    listProd (x:xs) = x * listProd xs

Base case (xs=[]):

listProd [] 
=> 1                                    -- unfold listProd
=> fold (*) 1 []                        -- fold fold

Induction step (xs=x:xs):

listProd (x:xs)
=> x * listProd xs                      -- unfold listProd
=> x * fold (*) 1 xs                    -- ind hyp
=> fold (*) 1 (x:xs)                    -- fold fold
       

2. Exercise 11.2 in SOE, but only for the 2nd fold law in Table 11.1,
   and the third take/drop law in Table 11.2.

"Prove as many of the properties in Tables 11.1 and 11.2 as you can."

Solution:

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

Proof:

For convenience, I will write + and * for op1 and op2.

Base case (xs=[]):
foldr (+) e [] => e => foldl (*) e []

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 0
=> foldl (*) (e*x) xs           -- aux (2)
foldl (*) e (x:xs)              -- unfold foldl

Lemma 0: 
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 + a                        -- unfold foldl
foldl (*) (x+a) []              -- fold foldl

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

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"

Proof:

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, xs=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


3. Exercise 11.3 in SOE.
       
"Which of the following functions are strict (if the function takes
more than one argument, specify on which arguments it is strict):"

Solution:

reverse:         strict
simple:          strict on all arguments
map:             not strict on first arg, strict on second arg
tail:            strict
area:            strict
regionToGRegion: strict
(&&):            strict on first arg, but not second
(True&&):        strict
(False&&):       not strict
ifFun:           strict only on first arg


4. Exercise 11.5 in SOE.
       
"Consider this definition of the factorial function:

> fac1 :: Integer -> Integer
> fac1 0 = 1
> fac1 n = n * fac1 (n-1)

and this alternative definition:

> fac2 :: Integer -> Integer
> fac2 n = fac' n 1
> where fac' 0 x = x
>       fac' n x = fac' (n-1) (n*x)

Prove that fac1 n = fac2 n for all non-negative integers n."

Solution:

Base case (n=0):
fac1 0 => 1 => fac' 0 1 => fac2 0

Induction step:
fac1 (n+1)
=> (n+1) * fac1 n               -- unfold fac1
=> (n+1) * fac2 n               -- ind hyp
=> (n+1) * fac' n 1             -- unfold fac2
=> fac' n (n+1)                 -- Lemma 1
=> fac' (n+1) 1                 -- fold fac'
fac2 (n+1)                      -- fold fac2

Lemma 1:  (n+1) * fac' n 1 = fac' n (n+1)

To prove Lemma 1 it is easier to first prove a more general lemma:

Lemma 2:  a * fac' n x = fac' n (a*x)

Indeed, Lemma 1 follows immediately from Lemma 2.

Proof of Lemma 2:

Base case (n=0):
a * fac' 0 x => a * x => fac' 0 (a*x)

Induction step (n=n+1):
a * fac' (n+1) x
=> a * fac' n ((n+1)*x)         -- unfold fac'
=> fac' n (a*((n+1)*x))         -- ind hyp
=> fac' n ((n+1)*(a*x))         -- associativity & commutativity
fac' (n+1) (a*x)                -- fold fac'


5. Consider the example involving the tree data type in the lecture notes
   for Chapter 11.
   a. Prove the lemma.
   b. Can you think of a useful generalization of this lemma, involving
      just foldl or foldr and (++), that would be suitable to add
      to Table 11.1 or 11.2?  Prove that it is correct.

Solution:

Lemma 3 (from lecture notes):
      sum (xs++ys) = sum xs + sum ys
      where sum = foldl (+) 0

Proof:

Base case (xs=[]):
sum ([]++ys) 
=> sum ys                       -- unfold (++)
=> 0 + sum ys                   -- identity law
=> foldl (+) 0 [] + sum ys      -- fold foldl   
sum [] + sum ys                 -- fold sum

Induction step (xs=x:xs):
sum ((x:xs)++ys) 
=> sum (x : (xs++ys))           -- unfold (++)
=> foldl (+) 0 (x : (xs++ys))   -- unfold sum
=> foldl (+) (0+x) (xs++ys)     -- unfold foldl
=> foldl (+) x (xs++ys)         -- identity law
=> x + foldl (+) 0 (xs++ys)     -- fold law (??)
=> x + sum (xs++ys)             -- fold sum
=> x + sum xs + sum ys          -- ind hyp
=> x + foldl (+) 0 xs + sum ys  -- unfold sum
=> foldl (+) x xs + sum ys      -- fold law (??)
=> foldl (+) (0+x) xs + sum ys  -- identity law
=> foldl (+) 0 (x:xs) + sum ys  -- fold foldl
sum (x:xs) + sum ys             -- fold sum

The steps labelled "fold law (??)"  should really be another lemma,
but instead of working that out, let's prove a more general overall
lemma, as asked for in the assignment.

Lemma 4:  If  e`op`x = x  &  x`op`e = x         (1)
         and  `op` is associative               (2)
        then  foldl op e (xs++ys) = foldl op e xs `op` foldl op e ys

Lemma 3 follows trivially from Lemma 4, since 0 is a left and right
identity for (+), and (+) is associative.

Proof:
Base case (xs=[]):
foldl op e ([]++ys) 
=> foldl op e ys                                -- unfold (++)
=> e `op` foldl op e ys                         -- aux (1)
foldl op e [] `op` foldl op e ys                -- fold foldl

Induction step (xs=x:xs):
foldl op e ((x:xs)++ys) 
=> foldl op e (x:(xs++ys))                      -- unfold (++)
=> foldl op (e`op`x) (xs++ys)                   -- unfold foldl
=> foldl op x (xs++ys)                          -- aux (1)
=> x `op` (foldl op e (xs++ys))                 -- Lemma 5
=> x `op` (foldl op e xs `op` foldl op e ys)    -- ind hyp
=> (x `op` foldl op e xs) `op` foldl op e ys    -- aux (2)
=> foldl op x xs `op` foldl op e ys             -- Lemma 5
=> foldl op (e`op`x) xs `op` foldl op e ys      -- aux (1)
foldl op e (x:xs) `op` foldl op e ys            -- fold foldl

Lemma 5:  If  e`op`x = x  &  x`op`e = x         (1)
         and  op is associative                 (2)
        then  foldl op a xs = a `op` foldl op e xs

Note that this lemma is very simmilar to Lemma 0 from problem 1 above,
which states:

Lemma 0: 
If   x + (y * z) = (x + y) * z
then x + foldl (*) a xs = foldl (*) (x+a) xs

Indeed, we can use it to prove Lemma 5 directly:

foldl op a xs 
=> foldl op (a`op`e) xs                 -- aux (1)
=> a `op` foldl op e xs                 -- Lemma 0

The last step is justified because op is associative.


6. Prove that the evaluate function defined recursively in Chapter 7
   is equivalent to the evaluate function defined in Problem 2 from
   Problem Set 3.

Solution:

From Chapter 7:

> evaluate :: Expr -> Float
> evaluate (C x) = x
> evaluate (e1 :+ e2) = evaluate e1 + evaluate e2
> evaluate (e1 :- e2) = evaluate e1 - evaluate e2
> evaluate (e1 :* e2) = evaluate e1 * evaluate e2
> evaluate (e1 :/ e2) = evaluate e1 / evaluate e2

From PS3, renamed to evaluate':

> evaluate' :: Expr -> Float
> evaluate' = foldExpr id (+) (-) (*) (/)
>
> foldExpr :: (Float->a) -> (a->a->a) -> (a->a->a) -> 
>                           (a->a->a) -> (a->a->a) -> Expr -> a
> foldExpr cf plusf minusf timesf divf expr =
>   let recurse = foldExpr cf plusf minusf timesf divf 
>   in case expr of
>        C x      -> cf x
>        e1 :+ e2 -> plusf  (recurse e1) (recurse e2)
>        e1 :- e2 -> minusf (recurse e1) (recurse e2)
>        e1 :* e2 -> timesf (recurse e1) (recurse e2)
>        e1 :/ e2 -> divf   (recurse e1) (recurse e2)

Theorem:  For all e :: Expr, evaluate e = evaluate' e.

Proof:

Base case (e = C x):
evaluate (C x)
=> x                                    -- unfold evaluate
=> id x                                 -- foldl id
=> foldExpr id (+) (-) (*) (/) (C x)    -- fold foldExpr
evaluate' (C x)                         -- fold evaluate'

Induction steps:
(a) e = e1 :+: e2
evaluate (e1 :+: e2)
=> evaluate e1 + evaluate e2            -- unfold evaluate
=> evaluate' e1 + evaluate' e2          -- ind hyp
=> (+) (evaluate' e1) (evaluate' e2)    -- syntax
=> (+) (foldExpr id (+) (-) (*) (/) e1)
       (foldExpr id (+) (-) (*) (/) e2) -- unfold evaluate'
=> (+) (recurse e1) (recurse e2)        -- fold recurse
=> foldExpr id (+) (-) (*) (/) 
            (e1 :+: e2)                 -- fold foldExpr
evaluate' (e1 :+: e2)                   -- fold evaluate'

(b) e = e1 :-: e2
Similar to (a), and thus omitted.

(c) e = e1 :*: e2
Similar to (a), and thus omitted.

(d) e = e1 :/: e2
Similar to (a), and thus omitted.