The Austalian National University Semester 2, 2018
Research School of Computer Science Assignment 2
Dirk Pattinson
Foundations of Computation
Released: Tue Sep 4 2018
Due: Tue Sep 28 2018 (any time)
Mode: individual submissions only
Submit: hard copy with cover sheet, ground oor CSIT building
Question 1 List Induction (2017 Exam) [25 + 25 credits]
Give an inductive proof the fact that consecutively mapping two functions over a list is equivalent to
mapping their composition over the list. That is:
map f (map g xs) = map (f.g) xs
The de nitions of map and compose (.) are:
map f [] = [] -- M1
map f (x:xs) = f x : map f xs -- M2
(f . g) x = f (g x) -- C
a) State and prove the base case goal.
b) State the inductive hypothesis.
c) State and prove the step case goal.
Now consider the following functions de ned on lists over an arbitrary type a
takew :: (a -> Bool) -> [a] -> [a]
takew p [] = []
takew p (x:xs) = if (p x) then x:(takew p xs) else []
dropw :: (a -> Bool) -> [a] -> [a]
dropw p [] = []
dropw p (x:xs) = if p x then (dropw p xs) else (x:xs)
together with the append function and the standard equations for if
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys -- A1 if True then p else _ = p -- I1
(x:xs) ++ ys = x : (xs ++ ys) -- A2 if False then _ else q = q -- I2
Show, using structural induction on lists, that the property
P(xs) = takew p xs ++ dropw p xs = xs
holds for all lists xs and all functions p :: a -> Bool. In all proofs indicate the justi cation (eg, the
line of a de nition used) for each step.
a) State and prove the base case of the proof of P.
b) State the inductive hypotheses of the proof of P.
c) State and prove the step case goal of the proof of P.
1
Question 2 Structural Induction with accumulator [25 credits]
Consider the functions count’ and (++):
count’ acc [] = acc -- C1
count’ acc (x:xs) = count’ (1 + acc) xs -- C2
[] ++ ys = ys -- A1
(x:xs) ++ ys = x : (xs ++ ys) -- A2
Prove by structural induction the following property:
count’ (count’ acc ys) xs = count’ acc (ys ++ xs)
State clearly what property P is being proved by induction, including any quanti ers needed in the
statement of P and in the inductive hypothesis.
Question 3 Tree Induction [25 credits]
Consider the de nition of binary trees given in the lectures
data Tree a = Nul | Node (Tree a) a (Tree a)
and the following three functions:
f :: Tree a -> Int
f Nul = 0 -- F1
f (Node Nul x Nul) = 1 -- F2
f (Node l x r ) = (f l) + (f r) -- F3
g :: Tree a -> Int
g t = h 0 t -- G
h :: Int -> Tree a -> Int
h acc Nul = acc -- H1
h acc (Node Nul x Nul) = acc + 1 -- H2
h acc (Node l x r ) = h (h acc l) r -- H3
Establish, using structural induction, that f t = g t for all trees t of type Tree a.
State clearly what property P is being proved by induction, including any quanti ers needed in the
statement of P and in the inductive hypothesis.