S08

Description

Synopsis

# Exercise 2

• The function drop from Lecture 3, given by

drop :: Integer -> [a] -> [a]
drop n xs | n <= 0  =  xs
drop _ []           =  []
drop n (_ :xs)      =  drop (n - 1) xs


is tail recursive, since the only recursive call is the last operation in the function body.

• The function range of Lecture 2 is guardedly recursive, since the only recursive call takes place in the second argument of the data constructor :.
• mySum from the same lecture is neither tail recursive nor guardedly recursive, since the last operation is addition (using +), which is not a data constructor.

# Exercise 3

initLast' :: [a] -> ([a], a) Source #

We prove the property P(xs) = (xs /= [] ==> initLast xs = initLast' xs) by induction on xs.

• We start with the base case xs = []: since the premise of P([]) is [] /= [] the claim holds vacuously.
• In the step case xs = y:ys and P(ys) by IH. In principle, we may assume

y:ys /= []


since the statement we want to show (P(y:ys)) is an implication. However, this assumption trivially reduces to True and hence doesn't help us in our proof.

We continue by a case analysis on ys, which is either empty or not:

• If ys = [] then

initLast [y] = (init [y], last [y]) = ([], y) = initLast' [y]


and we are done.

• Otherwise, ys /= [] and hence by IH initLast ys = initLast' ys, which implies (init ys, last ys) = initLast'. We conclude by the derivation:

initLast (y:ys)
= (init (y:ys), last (y:ys))
= (y : init ys, last ys)
= (y : us, u) where (us, u) = initLast' ys -- by IH
= initLast' (y:ys)


# Exercise 4

We prove the property P(n) = (fac n * k = go k n) for arbitrary k, by induction on n.

• We start with the base case n = 0. Then

fac 0 * k = k = go k 0

• In the step case we try to show P(n+1) under the IH that P(n) holds for arbitrary values of k. We proceed by a case analysis on n:

• If n = 0 then fac 1 * k = k = go k 1.
• Otherwise n > 0 and hence:

fac (n+1) * k
= (n+1) * fac n * k
= fac n * ((n + 1) * k)
= go ((n + 1) * k) n -- by IH
= go k (n + 1)


In the end, from P(n) for all n, we trivially obtain that fac n = fac' n for all n.

# Exercise 5

sort' :: Ord a => [a] -> [a] Source #

A potential sorting function.

prop_sort :: Int -> [Int] -> Bool Source #

The property

prop_sort y xs

does not hold, e.g., for y = 0 and xs = [0,0]. Hence, sort' is not a correct sorting function.

# Exercise 6

nfold' :: (Num t1, Ord t1) => t1 -> (t2 -> t2) -> t2 -> t2 Source #

nfold' n f x iteratively for n steps applies the given function f to the argument x

prop_nfold :: Int -> (Int -> Int) -> Int -> Bool Source #

The two implementations of n-fold function application behave the same:

nfold n f x = nfold' n f x