Functional Programming
Sheet 5
11/11/03
>module Sheet5 where
Question 1
It takes theta (n^2) time.
Justification:
insert = theta (n), since to insert an element into a sorted list of size n and keep it sorted requires anywhere between 0 and n comparisons. Or
to put it another way, in the worst-case, insert takes n comparisons.
sort uses insert to insert each of n elements into a sorted list, so sort = theta (n^2). In fact, we can say a little more about the worst-case.
Consider the following:
The first element is inserted into an empty list (no comparisons are required). Assuming that the worst-case occurs at every stage, the nth
element requires (n-1) comparisons before being inserted at the end of the list. So the number of comparisons required is:
sum (from 1 to n) (of (n-1)) = 0 + 1 + 2 + ... + (n-1)
But this is just (1/2)n(n-1) = (1/2)(n^2)-(1/2)n, which is theta (n^2).
---
Note: Typo in question, should be "y:insert x ys".
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)
sort [3,2,1,4]
= foldr insert [] [3,2,1,4] {defn. of sort}
= insert 3 (foldr insert [] [2,1,4]) {defn. of foldr}
{at this stage, there's no way of knowing which case of insert we're in without evaluating the foldr}
= insert 3 (insert 2 (foldr insert [] [1,4])) {defn. of foldr}
{at this stage, *we* do in theory know that we're in the recursive case of insert (since insert 2 <...> will not give [],
but the interpreter still doesn't, so the foldr will be evaluated again}
= insert 3 (insert 2 (insert 1 (foldr insert [] [4]))) {defn. of foldr}
= insert 3 (insert 2 (insert 1 (insert 4 (foldr insert [] [])))) {defn. of foldr}
= insert 3 (insert 2 (insert 1 (insert 4 []))) {defn. of foldr}
{we have to keep evaluating the arguments first here, even though this seems a bit like applicative-order reduction;
the reason being that we can't tell what case of insert we're in until the arguments are evaluated}
= insert 3 (insert 2 (insert 1 [4])) {defn. of insert}
= insert 3 (insert 2 (if 1<=4 then 1:4:[] else <...>)) {defn. of insert}
= insert 3 (insert 2 [1,4])
= insert 3 (if 2<=1 then <...> else 1:(insert 2 [4])) {defn. of insert}
= insert 3 (1:(insert 2 [4]))
{now at this stage, we can do the insert 3, since we know which case of insert we're in}
= if 3<=1 then <...> else 1:(insert 3 (insert 2 [4])) {defn. of insert}
= 1:(insert 3 (insert 2 [4]))
{now we have to evaluate insert 2 [4] to know which case of insert we're in again}
= 1:(insert 3 (if 2<=4 then 2:4:[] else <...>)) {defn. of insert}
= 1:(insert 3 [2,4])
= 1:(if 3<=2 then <...> else 2:(insert 3 [4])) {defn. of insert}
= 1:(2:(insert 3 [4]))
= 1:(2:(if 3<=4 then 3:4:[] else <...>)) {defn. of insert}
= 1:(2:([3,4]))
= [1,2,3,4]
Question 2
"Lazy evaluation means that no expression is evaluated more than once; for example in the term subseqs xs is evaluated at most once."
This is false, both because lazy evaluation means something else and because the term subseqs xs is evaluated twice in the given expression.
"Lazy evaluation means that no expression bound to a variable, either explicitly by a global or local definition, or implicitly as the argument of
a function, is evaluated more than once."
This is also false. It's true that no expression bound to a variable is evaluated more than once, but lazy evaluation still means something else.
Specifically, it means normal-order reduction.
Question 3
mult :: Integer -> Integer -> Integer
mult 0 y = 0
mult (x+1) y = mult x y + y
(a) Prove that mult (x+y) z = mult x z + mult y z
Proof (by induction over x):
[Base]
Show that mult (0+y) z = mult 0 z + mult y z [base]
LHS:
mult (0+y) z
= mult y z
= 0 + mult y z
= mult 0 z + mult y z {defn. of mult}
QED
[Induction Hypothesis]
mult (x+y) z = mult x z + mult y z [hyp]
[Induction Step]
Show that [hyp] => mult ((x+1)+y) z = mult (x+1) z + mult y z
LHS:
mult ((x+1)+y) z
= mult ((x+y)+1) z
= mult (x+y) z + z {defn. of mult}
= mult x z + mult y z + z {by [hyp]}
= (mult x z + z) + mult y z
= mult (x+1) z + mult y z {defn. of mult}
QED
(b) Prove that mult (mult x y) z = mult x (mult y z)
Proof (by induction over x):
[Base]
Show that mult (mult 0 y) z = mult 0 (mult y z)
LHS:
mult (mult 0 y) z
= mult 0 z {defn. of mult}
= 0 {defn. of mult}
= mult 0 (mult y z) {defn. of mult}
QED
[Induction Hypothesis]
mult (mult x y) z = mult x (mult y z)
[Induction Step]
Show that [hyp] => mult (mult (x+1) y) z = mult (x+1) (mult y z)
LHS:
mult (mult (x+1) y) z
= mult (mult x y + y) z {defn. of mult}
= mult (mult x y) z + mult y z {by proof in (a)}
= mult x (mult y z) + mult y z {by [hyp]}
= mult (x+1) (mult y z) {defn. of mult}
QED
Question 4
4.2.3
We first review the definition of (++):
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys [++.1]
(x:xs) ++ ys = x:(xs ++ ys) [++.2]
Prove by induction that xs ++ [] = xs for all lists xs.
Proof:
[Base]
Show that [] ++ [] = []
LHS:
[] ++ []
= [] {by ++.1}
QED
[Induction Hypothesis]
xs ++ [] = xs [hyp]
[Induction Step
Show that [hyp] => (x:xs) ++ [] = x:xs
LHS:
(x:xs) ++ []
= x:(xs ++ []) {by ++.2}
= x:xs {by [hyp]}
QED
4.2.5
We first review the definition of length:
length :: [a] -> Int
length [] = 0 [length.1]
length (x:xs) = 1 + length xs [length.2]
Prove that length (xs ++ ys) = length xs + length ys.
Proof (by induction over xs):
[Base]
Show that length ([] ++ ys) = length [] + length ys
LHS:
length ([] ++ ys)
= length ys {by ++.1}
= 0 + length ys
= length [] + length ys {by length.1}
QED
[Induction Hypothesis]
length (xs ++ ys) = length xs + length ys [hyp]
[Induction Step]
Show that [hyp] => length ((x:xs) ++ ys) = length (x:xs) + length ys
LHS:
length ((x:xs) ++ ys)
= length (x:(xs ++ ys)) {by ++.2}
= 1 + length (xs ++ ys) {by length.2}
= 1 + length xs + length ys {by [hyp]}
= length (x:xs) + length ys {by length.2}
QED