haskell代写 Foundations of Computation

程序代写 CS代考 / Haskell代写代考

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)

  1. a)  State and prove the base case goal.
  2. b)  State the inductive hypothesis.
  3. 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.

  1. a)  State and prove the base case of the proof of P.
  2. b)  State the inductive hypotheses of the proof of P.
  3. 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

Related Posts