The Austalian National University Research School of Computer Science Dirk Pattinson
Semester 2, 2018 Assignment 2
Foundations of Computation
Tue Sep 4 2018
Tue Sep 28 2018 (any time)
individual submissions only
hard copy with cover sheet, ground floor CSIT building
mapping their composition over the list. That is:
mapf(mapgxs) = map(f.g)xs The definitions of map and compose (.) are:
map f [] = []
map f (x:xs) = f x : map f xs (f.g)x = f(gx)
Released: Due: Mode: Submit:
[25 + 25 credits] Give an inductive proof the fact that consecutively mapping two functions over a list is equivalent to
Question 1
List Induction (2017 Exam)
- 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 defined 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 justification (eg, the
line of a definition 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
— M1 — M2 –C
Question 2 Structural Induction with accumulator [25 credits] Consider the functions count’ and (++):
count’ acc [] = acc count’ acc (x:xs) = count’ (1 + acc) xs
[] ++ys =ys
(x:xs) ++ ys = x : (xs ++ ys)
Prove by structural induction the following property:
— C1 — C2
–A1 — A2
count’ (count’ acc ys) xs = count’ acc (ys ++ xs)
State clearly what property P is being proved by induction, including any quantifiers needed in the statement of P and in the inductive hypothesis.
Question 3 Tree Induction [25 credits] Consider the definition 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 -- F2 -- F3
–G
— H1 — H2 –H3
f (Node Nul f (Node l
xNul)=1
xr )=(fl)+(fr)
g :: Tree a -> Int gt=h0t
h :: Int -> Tree a -> Int
haccNul= acc
h acc (Node NulxNul)=acc+1 hacc(Nodel xr ) =h(haccl)r
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 quantifiers needed in the statement of P and in the inductive hypothesis.
2