Functional Programming
Sheet 6
18/11/03
> module Sheet6 where
Question 1
FOR REFERENCE PURPOSES:
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z [] = z
foldr f z (x:xs) = f x (foldr f z xs)
Proof:
Case ():
LHS:
(f . foldr g a)
= f (foldr g a ) {defn. of (.)}
= f {defn. of foldr}
= {since f is strict}
RHS:
foldr h b
= {defn. of foldr}
QED
Case ([]):
LHS:
(f . foldr g a) []
= f (foldr g a []) {defn. of (.)}
= f a {defn. of foldr}
= b {since f a = b}
RHS:
foldr h b []
= b {defn. of foldr}
QED
Induction Hypothesis:
(f . foldr g a) xs = foldr h b xs [hyp]
Induction Step:
Show that [hyp] => (f . foldr g a) (x:xs) = foldr h b (x:xs)
LHS:
(f . foldr g a) (x:xs)
= f (foldr g a (x:xs)) {defn. of (.)}
= f (g x (foldr g a xs)) {defn. of foldr}
RHS:
foldr h b (x:xs)
= h x (foldr h b xs) {defn. of foldr}
= h x ((f . foldr g a) xs) {by [hyp]}
= h x (f (foldr g a xs)) {defn. of (.)}
Now we are given that for all x and y, f (g x y) = h x (f y). So taking x = x and y = foldr g a xs, we have:
f (g x (foldr g a xs)) = h x (f (foldr g a xs))
i.e. that the above expressions are the same.
QED
Thus completing the proof.
Question 2
cp [] = [[]]
cp (xs:xss) = [y:ys | y <- xs, ys <- cp xss]
> cp = foldr op [[]]
> where op xs xss = [y:ys | y <- xs, ys <- xss]
(a) Express map length in the form foldr f a for suitable f and a.
map length = foldr ((:) . length) []
(b) Recalling the fusion theorem for foldr, express product . map length in terms of foldr.
product . map length
= product . foldr ((:) . length) [] {by (a)}
In the theorem, we have:
f = product
g = (:) . length
a = []
We need to find h and b. Since f a = b, we have:
b
= product []
= foldr (*) 1 [] {defn. of product}
= 1 {defn. of foldr}
To find h, we use the fact that f (g x y) = h x (f y) for all x and y.
---------------------------------------------------
FOR REFERENCE PURPOSES:
foldr :: (a -> b -> b) -> b -> [a] -> b
foldr f z [] = z
foldr f z (x:xs) = f x (foldr f z xs)
---------------------------------------------------
h x (f y)
= h x (product y)
= h x (foldr (*) 1 y) {defn. of product}
= f (g x y)
= product (((:) . length) x y)
= foldr (*) 1 (((:) . length) x y) {defn. of product}
= foldr (*) 1 (length x : y) {defn. of (.)}
= (*) (length x) (foldr (*) 1 y) {defn. of foldr}
Rewriting what we have now discovered for clarity:
h x (foldr (*) 1 y) = (*) (length x) (foldr (*) 1 y)
So h = (*) . length.
And thus product . map length = foldr ((*) . length) 1.
(c) Again using the fusion theorem for foldr, express length . cp in terms of foldr.
length . cp
= length . foldr op [[]] {defn. of cp}
In the theorem, we have:
f = length
g = op
a = [[]]
We need to find h and b. Since f a = b, we have:
b
= length [[]]
= 1 {defn. of length}
To find h, we use the fact that f (g x y) = h x (f y) for all x and y.
h x (f y)
= h x (length y)
= f (g x y)
= length (op x y)
= length [q:qs | q <- x, qs <- y] {defn. of op (in cp)}
= length x * length y {since it is all possible pairs from x and y}
= (*) (length x) (length y)
Rewriting what we have now discovered for clarity:
h x (length y) = (*) (length x) (length y)
So h = (*) . length.
And thus length . cp = foldr ((*) . length) 1.
(d) Check that the two results are identical.
They are (which is something of a relief after all that!). Thus length . cp = product . map length, as required.
Question 3
Recall the definition of (+) for Nat:
(+) :: Nat -> Nat -> Nat
m + Zero = m [nat+.1]
m + Succ n = Succ (m + n) [nat+.2]
3.2.4
Proof by induction (over p):
Case ():
LHS:
(m + n) +
= {from defn. of (+) for Nat}
RHS:
m + (n + )
= m + {from defn. of (+) for Nat}
= {from defn. of (+) for Nat}
QED
Case (Zero):
LHS:
(m + n) + Zero
= m + n {by [nat+.1]}
RHS:
m + (n + Zero)
= m + n {by [nat+.1]}
QED
Induction Hypothesis:
(m + n) + p = m + (n + p) [hyp]
Induction Step:
Show that [hyp] => (m + n) + Succ p = m + (n + Succ p)
LHS:
(m + n) + Succ p
= Succ ((m + n) + p) {by [nat+.2]}
= Succ (m + (n + p)) {by [hyp]}
= m + Succ (n + p) {by [nat+.2]}
= m + (n + Succ p) {by [nat+.2]}
QED
Question 4
> sieve (p:xs) = [x | x <- xs, x `mod` p /= 0]
FOR REFERENCE PURPOSES:
iterate :: (a -> a) -> a -> [a]
iterate f x = x : iterate f (f x)
First here's a version which doesn't use iterate, so we can see what's going on a bit better:
> primes' :: [Int] -> [Int]
> primes' (p:xs) = p:primes' (sieve (p:xs))
This is a (bad) way of using iterate as required, but it will do for now:
> primes :: [Int]
> primes = head (iterate id (primes' [2..]))
Since we have to use iterate, here's one way (though a bit of an inefficient way) of doing it:
x = 2
f x = 3
f (f x) = 5
f (f (f x)) = 7
f (f (f (f x))) = 11
etc.
So:
> nextPrime :: Int -> Int
> nextPrime 2 = 3
> nextPrime p = recSieve p [p+2..]
> where
> recSieve :: Int -> [Int] -> Int
> recSieve 3 xs = head (sieve (2:(sieve (3:xs))))
> recSieve p xs = recSieve (p-2) (sieve (p:xs))
> primes2 :: [Int]
> primes2 = iterate nextPrime 2
This doesn't seem like a particularly good way of going about things, but it does work. The problem is, of course, that all the sieving gets
repeated each time, and it gets steadily worse the further on you go. Hence why the original definition (primes') was better, but that doesn't
use iterate (and I can't see a way to make it use it).
Question 5
The definition given enumerates the pairs in the order (0,0), (0,1), (0,2), etc. It will never get onto any pair not beginning with a 0.
Better would be something like:
> natpairs = [(i-j,j) | i <- [0..], j <- [0..i]]
which goes through the pairs in the order:
(0,0), (1,0), (0,1), (2,0), (1,1), (0,2), ...
Question 6
-------------------------------------------------------
FOR REFERENCE PURPOSES:
Note: This version is not the Prelude version (which uses a list comprehension), but it's equivalent, and easier to use for a proof.
map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = f x : map f xs
take :: Int -> [a] -> [a]
take n _ | n <= 0 = []
take _ [] = []
take n (x:xs) = x : take (n-1) xs
zipWith :: (a->b->c) -> [a]->[b]->[c]
zipWith z (a:as) (b:bs) = z a b : zipWith z as bs
zipWith _ _ _ = []
> fib :: Integer -> Integer
> fib 0 = 0
> fib 1 = 1
> fib (n+2) = fib n + fib (n+1)
-------------------------------------------------------
Proof:
Firstly, we can say that fibs = map fib [0..] if take n fibs = take n (map fib [0..]) for all natural numbers n.
We'll therefore attempt a proof by induction (which won't work initially, but may give us some ideas). Specifically, we aim to prove that:
take n (0:1:zipWith (+) fibs (tail fibs)) = take n (map fib [0..])
Base Case (n = 0):
LHS:
take 0 (0:1:zipWith (+) fibs (tail fibs))
= [] {defn. of take}
RHS:
take 0 (map fib [0..])
= [] {defn. of take}
QED
Induction Hypothesis:
take n (0:1:zipWith (+) fibs (tail fibs)) = take n (map fib [0..]) [hyp]
Induction Step:
Show that [hyp] => take (n+1) (0:1:zipWith (+) fibs (tail fibs)) = take (n+1) (map fib [0..])
RHS:
take (n+1) (map fib [0..])
= take (n+1) (map fib (enumFrom 0)) {defn. of [m..]}
= take (n+1) (map fib (0 : enumFrom 1)) {defn. of enumFrom}
= take (n+1) (fib 0 : map fib (enumFrom 1)) {defn. of map}
= fib 0 : take n (map fib (enumFrom 1)) {defn. of take}
= 0 : take n (map fib (enumFrom 1)) {defn. of fib}
= 0 : take n (map fib [1..]) {defn. of [m..]}
At this point, we get well and truly stuck, and have to try and come up with something a little bit more cunning.
To make our life a bit easier, we'll first prove by induction (over n) that take n (map f [a..]) = map f [a..a+n-1] for all f, a and n >= 0.
{Lemma [take&map]}
Base Case (n = 0):
LHS:
take 0 (map f [a..])
= [] {defn. of take}
RHS:
map f [a..a+0-1]
= map f [] {defn. of [m..]}
= [] {defn. of map}
QED
Induction Hypothesis:
take n (map f [a..]) = map f [a..a+n-1] [hyp]
Induction Step:
Show that [hyp] => take (n+1) (map f [a..]) = map f [a..a+n]
LHS:
take (n+1) (map f [a..])
= take (n+1) (map f (a:[(a+1)..])) {defn. of [m..]}
= take (n+1) (f a : map f [(a+1)..]) {defn. of map}
= f a : take n (map f [(a+1)..]) {defn. of take}
= f a : map f [(a+1)..(a+1)+n-1] {by [hyp], since a is universally quantified}
= f a : map f [(a+1)..a+n]
= map f (a:[(a+1)..a+n]) {defn. of map}
= map f [a..a+n] {defn. of (:)}
QED
{End Lemma}
This is quite a useful result, because now we can say that take n (map fib [0..]) = map fib [0..n-1].
Now we have to show that take n fibs is equal to this.
Probably the least painful way of doing this is to assume the result we're trying to prove is true, and substitute it in. This isn't
in general a particularly good way of going about proving something, but it may make things a little simpler here:
take n fibs
= take n (0:1:zipWith (+) (map fib [0..]) (tail (map fib [0..])))
= take n (0:1:zipWith (+) (map fib [0..]) (tail (map fib (enumFrom 0)))) {defn. of [m..]}
= take n (0:1:zipWith (+) (map fib [0..]) (tail (map fib (0 : enumFrom 1)))) {defn. of enumFrom}
= take n (0:1:zipWith (+) (map fib [0..]) (tail (fib 0 : map fib (enumFrom 1)))) {defn. of map}
= take n (0:1:zipWith (+) (map fib [0..]) (map fib (enumFrom 1))) {defn. of tail}
= take n (0:1:zipWith (+) (map fib [0..]) (map fib [1..])) {defn. of [m..]}
= 0:take (n-1) (1:zipWith (+) (map fib [0..]) (map fib [1..])) {defn. of take}
= 0:1:take (n-2) (zipWith (+) (map fib [0..]) (map fib [1..])) {defn. of take}
At this point, we again get stuck. What we really need (as the question hints) is a result which connects take and zipWith.
Specifically, we aim to prove that, for all natural numbers n, functions f and lists xs and ys:
take n (zipWith f xs ys) = zipWith f (take n xs) (take n ys)
{Lemma [take&zipWith]}
The proof is by induction (over n).
Base Case (n = 0):
LHS:
take 0 (zipWith f xs ys)
= [] {defn. of take}
RHS:
zipWith f (take 0 xs) (take 0 ys)
= zipWith f [] [] {defn. of take}
= [] {defn. of zipWith}
QED
Induction Hypothesis:
take n (zipWith f xs ys) = zipWith f (take n xs) (take n ys) [hyp]
Induction Step:
Show that [hyp] => take (n+1) (zipWith f xs ys) = zipWith f (take (n+1) xs) (take (n+1) ys)
Firstly, we need to recognise that in order to do anything much with the LHS, we're going to have to rewrite the
two lists as (x:xs) and (y:ys). In order to do this w.l.o.g., we need to prove the above result for the empty list in
each case:
i) take (n+1) (zipWith f [] ys) = zipWith f (take (n+1) []) (take (n+1) ys)
LHS:
take (n+1) (zipWith f [] ys)
= take (n+1) [] {defn. of zipWith}
= [] {defn. of take}
RHS:
zipWith f (take (n+1) []) (take (n+1) ys)
= zipWith f [] (take (n+1) ys) {defn. of take}
= [] {defn. of zipWith}
QED
ii) take (n+1) (zipWith f xs []) = zipWith f (take (n+1) xs) (take (n+1) [])
LHS:
take (n+1) (zipWith f xs [])
= take (n+1) [] {defn. of zipWith}
= [] {defn. of take}
RHS:
zipWith f (take (n+1) xs) (take (n+1) [])
= zipWith f (take (n+1) xs) [] {defn. of take}
= [] {defn. of zipWith}
QED
Returning to our original proof, we have to show that:
take (n+1) (zipWith f (x:xs) (y:ys)) = zipWith f (take (n+1) (x:xs) (take (n+1) (y:ys))
LHS:
take (n+1) (zipWith f (x:xs) (y:ys))
= take (n+1) (f x y : zipWith f xs ys) {defn. of zipWith}
= f x y : take n (zipWith f xs ys) {defn. of take}
= f x y : zipWith f (take n xs) (take n ys) {by [hyp]}
RHS:
zipWith f (take (n+1) (x:xs) (take (n+1) (y:ys))
= zipWith f (x : take n xs) (y : take n ys) {defn. of take}
= f x y : zipWith f (take n xs) (take n ys) {defn. of zipWith}
QED
Finally, to complete the proof of the lemma, we have to prove it for . In particular, we have to prove it
for two cases: xs = or ys = (or both, but we don't have to prove that separately).
So, we aim to prove that:
i) take n (zipWith f ys) = zipWith f (take n ) (take n ys)
LHS:
take n (zipWith f ys)
= take n [] {defn. of zipWith}
= [] {defn. of take}
RHS:
zipWith f (take n ) (take n ys)
= zipWith f [] (take n ys) {defn. of take}
= [] {defn. of zipWith}
QED
ii) take n (zipWith f xs ) = zipWith f (take n xs) (take n )
LHS:
take n (zipWith f xs )
= take n [] {defn. of zipWith}
= [] {defn. of take}
RHS:
zipWith f (take n xs) (take n )
= zipWith f (take n xs) [] {defn. of take}
= [] {defn. of zipWith}
QED
As the original lemma is an equation, we can say that chain completeness holds, thus completing the proof as required.
{End Lemma}
Returning to our original proof, we had the following:
0:1:take (n-2) (zipWith (+) (map fib [0..]) (map fib [1..]))
Given that we now know that:
take n (zipWith f xs ys) = zipWith f (take n xs) (take n ys)
We can rewrite what we had as:
0:1:zipWith (+) (take (n-2) (map fib [0..])) (take (n-2) (map fib [1..])) {by [take&zipWith]}
But we also proved another lemma, namely that:
take n (map f [a..]) = map f [a..a+n-1]
So rewriting the above again, we have:
0:1:zipWith (+) (map fib [0..0+(n-2)-1]) (map fib [1..1+(n-2)-1]) {by [take&map]}
= 0:1:zipWith (+) (map fib [0..n-3]) (map fib [1..n-2])
We now need to show that this is equal to map fib [0..n-1].
This is something that is most easily shown by induction over n, which is now much easier since the lists involved
are all finite. To make things a little neater, we'll actually introduce m = n + 2 at this stage, so that we can
use 0 as the base case. Then the proof will in fact be by induction over m. We aim to show that:
0:1:zipWith (+) (map fib [0..m-1]) (map fib [1..m]) = map fib [0..m+1]
Base Case (m = 0):
LHS:
0:1:zipWith (+) (map fib [0..0-1]) (map fib [1..0])
= 0:1:zipWith (+) (map fib []) (map fib []) {defn. of [m..n] - note: m here denotes an arbitrary number, as always, not the m in the induction}
= 0:1:zipWith (+) [] [] {defn. of map}
= 0:1:[] {defn. of zipWith}
= [0,1]
RHS:
map fib [0..0+1]
= map fib [0,1] {defn. of [m..n]}
= fib 0 : map fib [1] {defn. of map}
= fib 0 : fib 1 : map fib [] {defn. of map}
= fib 0 : fib 1 : [] {defn. of map}
= 0:1:[] {defn. of fib}
= [0,1]
QED
Induction Hypothesis:
0:1:zipWith (+) (map fib [0..m-1]) (map fib [1..m]) = map fib [0..m+1] [hyp]
Induction Step:
Show that [hyp] => 0:1:zipWith (+) (map fib [0..m]) (map fib [1..m+1]) = map fib [0..m+2]
This looks distinctly non-obvious, so at this stage, we'll prove yet another lemma, namely that:
For functions f and two lists xs and ys s.t. length xs = length ys:
zipWith f (xs ++ [a]) (ys ++ [b]) = zipWith f xs ys ++ [f a b]
{Lemma [zipWith|append]}
Rather than having to go all the way back to the beginning of the question for the definition of zipWith, here it is again for reference:
zipWith :: (a->b->c) -> [a]->[b]->[c]
zipWith z (a:as) (b:bs) = z a b : zipWith z as bs
zipWith _ _ _ = []
We will prove the lemma by induction over both xs and ys.
Base Case (xs = ys = []):
LHS:
zipWith f ([] ++ [a]) ([] ++ [b])
= zipWith f [a] [b] {defn. of (++)}
= f a b : zipWith f [] [] {defn. of zipWith}
= f a b : [] {defn. of zipWith}
= [f a b]
RHS:
zipWith f xs ys ++ [f a b]
= zipWith f [] [] ++ [f a b]
= [] ++ [f a b] {defn. of zipWith}
= [f a b]
QED
Induction Hypothesis:
zipWith f (xs ++ [a]) (ys ++ [b]) = zipWith f xs ys ++ [f a b] [hyp]
Induction Step:
Show that [hyp] => zipWith f ((x:xs) ++ [a]) ((y:ys) ++ [b]) = zipWith f (x:xs) (y:ys) ++ [f a b]
LHS:
zipWith f ((x:xs) ++ [a]) ((y:ys) ++ [b])
= zipWith f (x:(xs ++ [a])) (y:(ys ++ [b])) {defn. of (++)}
= f x y : zipWith f (xs ++ [a]) (ys ++ [b]) {defn. of zipWith}
= f x y : (zipWith f xs ys ++ [f a b]) {by [hyp]}
= (f x y : zipWith f xs ys) ++ [f a b]) {defn. of (++)}
= zipWith f (x:xs) (y:ys) ++ [f a b] {defn. of zipWith}
QED
{End Lemma}
Returning to our original (by now distinctly long-winded) proof, we recall that we had the following:
Show that [hyp] => 0:1:zipWith (+) (map fib [0..m]) (map fib [1..m+1]) = map fib [0..m+2]
Now it is clearly the case (and in all honesty not worth proving) that the lengths of [0..m] and [1..m+1] are equal, and that
the lengths of map fib [0..m] and map fib [1..m+1] are likewise equal. Thus we can apply our new lemma to finish the proof:
0:1:zipWith (+) (map fib [0..m]) (map fib [1..m+1])
= 0:1:zipWith (+) (map fib ([0..m-1] ++ [m])) (map fib ([1..m] ++ [m+1]))
= 0:1:zipWith (+) (map fib [0..m-1] ++ [fib m]) (map fib [1..m] ++ [fib (m+1)]) {provable if necessary}
= 0:1:(zipWith (+) (map fib [0..m-1]) (map fib [1..m]) ++ [(+) (fib m) (fib (m+1))]) {by [zipWith|append]}
= (0:1:zipWith (+) (map fib [0..m-1]) (map fib [1..m])) ++ [(+) (fib m) (fib (m+1))] {defn. of (++)}
= map fib [0..m+1] ++ [(+) (fib m) (fib (m+1))] {by [hyp]}
= map fib [0..m+1] ++ [fib (m+2)] {defn. of fib}
= map fib [0..m+2] {provable if necessary}
QED
Thus completing the proof.
[FWIW: If there's a quicker way to prove this, I'd really like to hear about it! This proof has just taken me several hours.]