Solutions
Content
Programming in Haskell
Solutions to Exercises
Graham Hutton
University of Nottingham
Contents
Chapter 1 - Introduction
1
Chapter 2 - First steps
3
Chapter 3 - Types and classes
4
Chapter 4 - Defining functions
5
Chapter 5 - List comprehensions
7
Chapter 6 - Recursive functions
9
Chapter 7 - Higher-order functions
13
Chapter 8 - Functional parsers
15
Chapter 9 - Interactive programs
19
Chapter 10 - Declaring types and classes
21
Chapter 11 - The countdown problem
23
Chapter 12 - Lazy evaluation
24
Chapter 13 - Reasoning about programs
26
Chapter 1 - Introduction
Exercise 1
=
=
=
=
=
double (double 2)
{ applying the inner double }
double (2 + 2)
{ applying double }
(2 + 2) + (2 + 2)
{ applying the first + }
4 + (2 + 2)
{ applying the second + }
4+4
{ applying + }
8
or
=
=
=
=
=
=
double (double 2)
{ applying the outer double }
(double 2) + (double 2)
{ applying the second double }
(double 2) + (2 + 2)
{ applying the second + }
(double 2) + 4
{ applying double }
(2 + 2) + 4
{ applying the first + }
4+4
{ applying + }
8
There are a number of other answers too.
Exercise 2
sum [x ]
{ applying sum }
x + sum [ ]
=
{ applying sum }
x +0
=
{ applying + }
x
=
Exercise 3
(1)
product [ ]
=
product (x : xs) =
1
x ∗ product xs
1
(2)
=
=
=
=
=
product [2, 3, 4]
{ applying product }
2 ∗ (product [3, 4])
{ applying product }
2 ∗ (3 ∗ product [4])
{ applying product }
2 ∗ (3 ∗ (4 ∗ product [ ]))
{ applying product }
2 ∗ (3 ∗ (4 ∗ 1))
{ applying ∗ }
24
Exercise 4
Replace the second equation by
qsort (x : xs) =
qsort larger ++ [x ] ++ qsort smaller
That is, just swap the occurrences of smaller and larger .
Exercise 5
Duplicate elements are removed from the sorted list. For example:
=
=
=
=
=
qsort [2, 2, 3, 1, 1]
{ applying qsort }
qsort [1, 1] ++ [2] ++ qsort [3]
{ applying qsort }
(qsort [ ] ++ [1] ++ qsort [ ]) ++ [2] ++ (qsort [ ] ++ [3] ++ qsort [ ])
{ applying qsort }
([ ] ++ [1] ++ [ ]) ++ [2] ++ ([ ] ++ [3] ++ [ ])
{ applying ++ }
[1] ++ [2] ++ [3]
{ applying ++ }
[1, 2, 3]
2
Chapter 2 - First steps
Exercise 1
(2 ↑ 3) ∗ 4
(2 ∗ 3) + (4 ∗ 5)
2 + (3 ∗ (4 ↑ 5))
Exercise 2
No solution required.
Exercise 3
n
= a ‘div ‘ length xs
where
a = 10
xs = [1, 2, 3, 4, 5]
Exercise 4
last xs
=
head (reverse xs)
last xs
=
xs !! (length xs − 1)
init xs
=
take (length xs − 1) xs
init xs
=
reverse (tail (reverse xs))
or
Exercise 5
or
3
Chapter 3 - Types and classes
Exercise 1
[Char ]
(Char , Char , Char )
[(Bool , Char )]
([Bool ], [Char ])
[[a ] → [a ]]
Exercise 2
[a ] → a
(a, b) → (b, a)
a → b → (a, b)
Num a ⇒ a → a
Eq a ⇒ [a ] → Bool
(a → a) → a → a
Exercise 3
No solution required.
Exercise 4
In general, checking if two functions are equal requires enumerating all possible argument values, and checking if the functions give the same result for each of these
values. For functions with a very large (or infinite) number of argument values, such
as values of type Int or Integer, this is not feasible. However, for small numbers of
argument values, such as values of type of type Bool , it is feasible.
4
Chapter 4 - Defining functions
Exercise 1
halve xs
= splitAt (length xs ‘div ‘ 2) xs
halve xs
= (take n xs, drop n xs)
where
n = length xs ‘div ‘ 2
or
Exercise 2
(a)
safetail xs
=
if null xs then [ ] else tail xs
(b)
safetail xs | null xs
| otherwise
=
=
[]
tail xs
(c)
safetail [ ]
safetail xs
=
=
[]
tail xs
or
safetail [ ]
=
safetail ( : xs) =
[]
xs
Exercise 3
(1)
False ∨ False
False ∨ True
True ∨ False
True ∨ True
=
=
=
=
False ∨ False
∨
= False
= True
False ∨ b
True ∨
b
True
False
True
True
True
(2)
(3)
=
=
(4)
b ∨ c | b == c
| otherwise
=
=
b
True
5
Exercise 4
a∧b
=
if a then
if b then True else False
else
False
=
if a then b else False
Exercise 5
a∧b
Exercise 6
mult
= λx → (λy → (λz → x ∗ y ∗ z ))
6
Chapter 5 - List comprehensions
Exercise 1
sum [x ↑ 2 | x ← [1 . . 100]]
Exercise 2
= [x |
replicate n x
← [1 . . n ]]
Exercise 3
pyths n
[(x , y, z ) | x
y
z
x
=
← [1 . . n ],
← [1 . . n ],
← [1 . . n ],
↑ 2 + y ↑ 2 == z ↑ 2]
Exercise 4
perfects n
=
[x | x ← [1 . . n ], sum (init (factors x )) == x ]
Exercise 5
concat [[(x , y) | y ← [4, 5, 6]] | x ← [1, 2, 3]]
Exercise 6
positions x xs
=
find x (zip xs [0 . . n ])
where n = length xs − 1
Exercise 7
scalarproduct xs ys
=
sum [x ∗ y | (x , y) ← zip xs ys ]
Exercise 8
shift
shift n c | isLower c
| isUpper c
| otherwise
::
=
=
=
Int → Char → Char
int2low ((low2int c + n) ‘mod ‘ 26)
int2upp ((upp2int c + n) ‘mod ‘ 26)
c
freqs
freqs xs
::
=
String → [Float ]
[percent (count x xs ) n | x ← [’a’ . . ’z’]]
where
xs = map toLower xs
n = letters xs
low2int
low2int c
::
=
Char → Int
ord c − ord ’a’
7
int2low
int2low n
::
=
Int → Char
chr (ord ’a’ + n)
upp2int
upp2int c
::
=
Char → Int
ord c − ord ’A’
int2upp
int2upp n
::
=
Int → Char
chr (ord ’A’ + n)
letters
letters xs
::
=
String → Int
length [x | x ← xs, isAlpha x ]
8
Chapter 6 - Recursive functions
Exercise 1
(1)
m ↑0
= 1
m ↑ (n + 1) = m ∗ m ↑ n
(2)
=
=
=
=
=
2↑3
{ applying ↑ }
2 ∗ (2 ↑ 2)
{ applying ↑ }
2 ∗ (2 ∗ (2 ↑ 1))
{ applying ↑ }
2 ∗ (2 ∗ (2 ∗ (2 ↑ 0)))
{ applying ↑ }
2 ∗ (2 ∗ (2 ∗ 1))
{ applying ∗ }
8
Exercise 2
(1)
=
=
=
=
=
length [1, 2, 3]
{ applying length }
1 + length [2, 3]
{ applying length }
1 + (1 + length [3])
{ applying length }
1 + (1 + (1 + length [ ]))
{ applying length }
1 + (1 + (1 + 0))
{ applying + }
3
(2)
drop 3 [1, 2, 3, 4, 5]
{ applying drop
drop 2 [2, 3, 4, 5]
=
{ applying drop
drop 1 [3, 4, 5]
=
{ applying drop
drop 0 [4, 5]
=
{ applying drop
[4, 5]
=
}
}
}
}
9
(3)
init [1, 2, 3]
{ applying init }
1 : init [2, 3]
=
{ applying init }
1 : 2 : init [3]
=
{ applying init }
1 :2 : []
=
{ list notation }
[1, 2]
=
Exercise 3
and [ ]
and (b : bs)
=
=
True
b ∧ and bs
concat [ ]
concat (xs : xss)
=
=
[]
xs ++ concat xss
replicate 0
replicate (n + 1) x
=
=
[]
x : replicate n x
(x : ) !! 0
( : xs) !! (n + 1)
=
=
x
xs !! n
elem x [ ]
elem x (y : ys) | x == y
| otherwise
=
=
=
False
True
elem x ys
Exercise 4
merge [ ] ys
merge xs [ ]
merge (x : xs) (y : ys)
= ys
= xs
= if x ≤ y then
x : merge xs (y : ys)
else
y : merge (x : xs) ys
Exercise 5
halve xs
= splitAt (length xs ‘div ‘ 2) xs
msort [ ]
= []
msort [x ] = [x ]
msort xs = merge (msort ys) (msort zs)
where (ys, zs) = halve xs
10
Exercise 6.1
Step 1: define the type
sum
:: [Int ] → Int
Step 2: enumerate the cases
sum [ ]
sum (x : xs)
=
=
Step 3: define the simple cases
sum [ ]
sum (x : xs)
= 0
=
Step 4: define the other cases
sum [ ]
sum (x : xs)
= 0
= x + sum xs
Step 5: generalise and simplify
sum
sum
::
=
Num a ⇒ [a ] → a
foldr (+) 0
Exercise 6.2
Step 1: define the type
take
:: Int → [a ] → [a ]
Step 2: enumerate the cases
take
take
take
take
0 []
0 (x : xs)
(n + 1) [ ]
(n + 1) (x : xs)
=
=
=
=
Step 3: define the simple cases
take
take
take
take
0 []
0 (x : xs)
(n + 1) [ ]
(n + 1) (x : xs)
=
=
=
=
[]
[]
[]
Step 4: define the other cases
take
take
take
take
0 []
0 (x : xs)
(n + 1) [ ]
(n + 1) (x : xs)
=
=
=
=
[]
[]
[]
x : take n xs
Step 5: generalise and simplify
take
::
=
take 0
take (n + 1) [ ]
=
take (n + 1) (x : xs) =
Int → [a ] → [a ]
[]
[]
x : take n xs
11
Exercise 6.3
Step 1: define the type
last
:: [a ] → [a ]
Step 2: enumerate the cases
last (x : xs) =
Step 3: define the simple cases
last (x : xs) | null xs
| otherwise
= x
=
Step 4: define the other cases
last (x : xs) | null xs
| otherwise
= x
= last xs
Step 5: generalise and simplify
last
::
last [x ]
=
last ( : xs) =
[a ] → [a ]
x
last xs
12
Chapter 7 - Higher-order functions
Exercise 1
map f (filter p xs)
Exercise 2
all p
=
and ◦ map p
any p
=
or ◦ map p
takeWhile [ ] = [ ]
takeWhile p (x : xs)
|px
= x : takeWhile p xs
| otherwise = [ ]
dropWhile [ ]
dropWhile p (x
|px
| otherwise
= []
: xs)
= dropWhile p xs
= x : xs
Exercise 3
map f
=
foldr (λx xs → f x : xs) [ ]
filter p
=
foldr (λx xs → if p x then x : xs else xs) [ ]
Exercise 4
dec2nat
foldl (λx y → 10 ∗ x + y) 0
=
Exercise 5
The functions being composed do not all have the same types. For example:
sum
:: [Int ] → Int
map (↑2)
:: [Int ] → [Int ]
filter even
:: [Int ] → [Int ]
Exercise 6
curry
curry f
::
=
((a, b) → c) → (a → b → c)
λx y → f (x , y)
uncurry
uncurry f
::
=
(a → b → c) → ((a, b) → c)
λ(x , y) → f x y
13
Exercise 7
chop8
=
unfold null (take 8) (drop 8)
map f
=
unfold null (f ◦ head ) tail
iterate f
=
unfold (const False) id f
Exercise 8
encode
encode
::
=
String → [Bit ]
concat ◦ map (addparity ◦ make8 ◦ int2bin ◦ ord )
decode
decode
::
=
[Bit ] → String
map (chr ◦ bin2int ◦ checkparity ) ◦ chop9
addparity
addparity bs
::
=
[Bit ] → [Bit ]
(parity bs) : bs
parity
::
parity bs | odd (sum bs) =
| otherwise
=
[Bit ] → Bit
1
0
chop9
chop9 [ ]
chop9 bits
::
=
=
[Bit ] → [[Bit ]]
[]
take 9 bits : chop9 (drop 9 bits)
checkparity
checkparity (b : bs)
| b == parity bs
| otherwise
::
[Bit ] → [Bit ]
=
=
bs
error "parity mismatch"
Exercise 9
No solution required.
14
Chapter 8 - Functional parsers
Exercise 1
int
=
do char ’-’
n ← nat
return (−n)
+++nat
Exercise 2
comment
=
do string "--"
many (sat (
= ’\n’))
return ()
Exercise 3
(1)
expr
KK
u
KK
u
u
zu
%
expr
exprI
+
uu III
u
zu
$
expr
expr
+
term
term
term factor
factor
factor
nat
2
nat
3
nat
4
(2)
expr I
ss III
yss
$
exprI
expr
+
uu III
zuu
$
expr
expr
+
term
factor
nat
2
term
factor
term
factor
nat
3
nat
4
15
Exercise 4
(1)
expr I
III
u
u
u
$
zu
expr
+
term
factor
term
factor
nat
nat
2
3
(2)
expr
termI
t
II
I$
yttt
∗
factor
termG
GGG
ww
w
G#
{
w
∗
factor
nat
term
factor
nat
2
nat
3
4
(3)
expr K
ss KKK
yss
%
expr
+
term
factorI
term
III
uuu
II
$
zuuu expr
)
factor
(
JJJ
tt
JJ
zttt
$
expr
+
term
nat
factor
nat
2
term
factor
nat
3
16
4
Exercise 5
Without left-factorising the grammar, the resulting parser would backtrack excessively
and have exponential time complexity in the size of the expression. For example, a
number would be parsed four times before being recognised as an expression.
Exercise 6
expr
= do t ← term
do symbol "+"
e ← expr
return (t + e)
+++ do symbol "-"
e ← expr
return (t − e)
+++ return t
term
= do f ← factor
do symbol "*"
t ← term
return (f ∗ t )
+++ do symbol "/"
t ← term
return (f ‘div ‘ t )
+++ return f
Exercise 7
(1)
factor
::=
atom (↑ factor | epsilon)
atom
::=
(expr ) | nat
factor
factor
:: Parser Int
= do a ← atom
do symbol "^"
f ← factor
return (a ↑ f )
+++ return a
(2)
atom
atom
::
=
Parser Int
do symbol "("
e ← expr
symbol ")"
return e
+++ natural
17
Exercise 8
(a)
expr
::=
expr − nat | nat
nat
::=
0 | 1 | 2 | ···
expr
= do e ← expr
symbol "-"
n ← natural
return (e − n)
+++ natural
(b)
(c)
The parser loops forever without producing a result, because the first
operation it performs is to call itself recursively.
(d)
expr
= do n ← natural
ns ← many (do symbol "-"
natural)
return (foldl (−) n ns)
18
Chapter 9 - Interactive programs
Exercise 1
readLine
= get ""
get xs
= do x ← getChar
case x of
’\n’ → return xs
’\DEL’ → if null xs then
get xs
else
do putStr "\ESC[1D \ESC[1D"
get (init xs)
→ get (xs ++ [x ])
Exercise 2
No solution available.
Exercise 3
No solution available.
Exercise 4
No solution available.
Exercise 5
No solution available.
Exercise 6
type Board
=
[Int ]
initial
initial
::
=
Board
[5, 4, 3, 2, 1]
finished
finished b
::
=
Board → Bool
all (== 0) b
valid
valid b row num
::
=
Board → Int → Int → Bool
b !! (row − 1) ≥ num
move
move b row num
::
=
newline
newline
::
=
Board → Int → Int → Board
[if r == row then n − num else n
| (r , n) ← zip [1 . . 5] b ]
IO ()
putChar ’\n’
19
putBoard
putBoard [a, b, c, d , e ]
::
=
Board → IO ()
do putRow 1 a
putRow 2 b
putRow 3 c
putRow 4 d
putRow 5 e
putRow
putRow row num
::
=
Int → Int → IO ()
do putStr (show row )
putStr ": "
putStrLn (stars num)
stars
stars n
::
=
Int → String
concat (replicate n "* ")
getDigit
getDigit prom
::
=
String → IO Int
do putStr prom
x ← getChar
newline
if isDigit x then
return (ord x − ord ’0’)
else
do putStrLn "ERROR: Invalid digit"
getDigit prom
nim
nim
::
=
IO ()
play initial 1
play
play board player
::
=
Board → Int → IO ()
do newline
putBoard board
if finished board then
do newline
putStr "Player "
putStr (show (next player ))
putStrLn " wins!!"
else
do newline
putStr "Player "
putStrLn (show player )
r ← getDigit "Enter a row number: "
n ← getDigit "Stars to remove : "
if valid board r n then
play (move board r n) (next player )
else
do newline
putStrLn "ERROR: Invalid move"
play board player
next
next 1
next 2
::
=
=
Int → Int
2
1
20
Chapter 10 - Declaring types and classes
Exercise 1
mult m Zero
mult m (Succ n)
= Zero
= add m (mult m n)
Exercise 2
occurs m (Leaf n)
=
occurs m (Node l n r ) =
m == n
case compare m n of
LT → occurs m l
EQ → True
GT → occurs m r
This version is more efficient because it only requires one comparison for each node,
whereas the previous version may require two comparisons.
Exercise 3
leaves (Leaf )
leaves (Node l r )
=
=
balanced (Leaf )
=
balanced (Node l r ) =
1
leaves l + leaves r
True
abs (leaves l − leaves r ) ≤ 1
∧ balanced l ∧ balanced r
Exercise 4
halve xs
=
balance [x ] =
balance xs =
splitAt (length xs ‘div ‘ 2) xs
Leaf x
Node (balance ys) (balance zs)
where (ys, zs) = halve xs
Exercise 5
data Prop
= · · · | Or Prop Prop | Equiv Prop Prop
eval s (Or p q)
eval s (Equiv p q)
= eval s p ∨ eval s q
= eval s p == eval s q
vars (Or p q)
vars (Equiv p q)
= vars p ++ vars q
= vars p ++ vars q
Exercise 6
No solution available.
21
Exercise 7
data Expr
= Val Int | Add Expr Expr | Mult Expr Expr
type Cont
= [Op ]
data Op
= EVALA Expr | ADD Int | EVALM Expr | MUL Int
eval
eval (Val n) ops
eval (Add x y) ops
eval (Mult x y) ops
::
=
=
=
Expr → Cont → Int
exec ops n
eval x (EVALA y : ops)
eval x (EVALM y : ops)
exec
exec
exec
exec
exec
exec
::
=
=
=
=
=
Cont → Int → Int
n
eval y (ADD n : ops)
exec ops (n + m)
eval y (MUL n : ops)
exec ops (n ∗ m)
[] n
(EVALA y : ops) n
(ADD n : ops) m
(EVALM y : ops) n
(MUL n : ops) m
:: Expr → Int
= eval e [ ]
value
value e
Exercise 8
instance Monad Maybe where
return
:: a → Maybe a
return x
= Just x
(>
>=)
Nothing >
>=
(Just x ) >
>= f
:: Maybe a → (a → Maybe b) → Maybe b
= Nothing
= f x
instance Monad [ ] where
return
:: a → [a ]
return x = [x ]
(>
>=)
xs >
>= f
:: [a ] → (a → [b ]) → [b ]
= concat (map f xs)
22
Chapter 11 - The countdown problem
Exercise 1
choices xs
=
[zs | ys ← subs xs, zs ← perms ys ]
Exercise 2
removeone x [ ]
= []
removeone x (y : ys)
| x == y
= ys
| otherwise
= y : removeone x ys
isChoice [ ]
isChoice (x : xs) [ ]
isChoice (x : xs) ys
= True
= False
= elem x ys ∧ isChoice xs (removeone x ys)
Exercise 3
It would lead to non-termination, because recursive calls to exprs would no longer be
guaranteed to reduce the length of the list.
Exercise 4
> length [e | ns ← choices [1, 3, 7, 10, 25, 50], e ← exprs ns ]
33665406
> length [e | ns ← choices [1, 3, 7, 10, 25, 50], e ← exprs ns, eval e
= [ ]]
4672540
Exercise 5
Modifying the definition of valid by
valid Sub x y
valid Div x y
= True
= y
= 0 ∧ x ‘mod ‘ y == 0
gives
> length [e | ns ← choices [1, 3, 7, 10, 25, 50], e ← exprs ns , eval e
= [ ]]
10839369
Exercise 6
No solution available.
23
Chapter 12 - Lazy evaluation
Exercise 1
(1)
2 ∗ 3 is the only redex, and is both innermost and outermost.
(2)
1 + 2 and 2 + 3 are redexes, with 1 + 2 being innermost.
(3)
1 + 2, 2 + 3 and fst (1 + 2, 2 + 3) are redexes, with the first of these being
innermost and the last being outermost.
(4)
2 ∗ 3 and (λx → 1 + x ) (2 ∗ 3) are redexes, with the first being innermost
and the second being outermost.
Exercise 2
Outermost:
fst (1 + 2, 2 + 3)
{ applying fst }
1+2
=
{ applying + }
3
=
Innermost:
fst (1 + 2, 2 + 3)
{ applying the first + }
fst (3, 2 + 3)
=
{ applying + }
fst (3, 5)
=
{ applying fst }
3
=
Outermost evaluation is preferable because it avoids evaluation of the second argument, and hence takes one less reduction step.
Exercise 3
mult 3 4
{ applying mult }
(λx → (λy → x ∗ y)) 3 4
=
{ applying λx → (λy → x ∗ y) }
(λy → 3 ∗ y) 4
=
{ applying λy → 3 ∗ y }
3∗4
=
{ applying ∗ }
12
=
24
Exercise 4
fibs
0 : 1 : [x + y | (x , y) ← zip fibs (tail fibs)]
=
Exercise 5
(1)
fib n
=
fibs !! n
(2)
head (dropWhile (≤ 1000) fibs)
Exercise 6
repeatTree
repeatTree x
:: a → Tree a
= Node t x t
where t = repeatTree x
takeTree
takeTree 0
takeTree (n + 1) Leaf
takeTree (n + 1) (Node l x r )
::
=
=
=
replicateTree
replicateTree n
:: Int → a → Tree a
= takeTree n ◦ repeatTree
Int → Tree a → Tree a
Leaf
Leaf
Node (takeTree n l ) x (takeTree n r )
25
Chapter 13 - Reasoning about programs
Exercise 1
last
::
last [x ]
=
last ( : xs) =
[a ] → a
x
last xs
init
::
=
init [ ]
init (x : xs) =
[a ] → [a ]
[]
x : init xs
or
or
foldr1
::
=
foldr1 [x ]
foldr1 f (x : xs) =
(a → a → a) → [a ] → a
x
f x (foldr1 f xs)
There are a number of other answers too.
Exercise 2
Base case:
add Zero (Succ m)
{ applying add }
Succ m
=
{ unapplying add }
Succ (add Zero m)
=
Inductive case:
add (Succ n) (Succ m)
{ applying add }
Succ (add n (Succ m))
=
{ induction hypothesis }
Succ (Succ (add n m))
=
{ unapplying add }
Succ (add (Succ n) m)
=
Exercise 3
Base case:
add Zero m
{ applying add }
m
=
{ property of add }
add m Zero
=
26
Inductive case:
add (Succ n) m
{ applying add }
Succ (add n m)
=
{ induction hypothesis }
Succ (add m n)
=
{ property of add }
add m (Succ n)
=
Exercise 4
Base case:
all (== x ) (replicate 0 x )
{ applying replicate }
all (== x ) [ ]
=
{ applying all }
True
=
Inductive case:
=
=
=
=
=
all (== x ) (replicate (n + 1) x )
{ applying replicate }
all (== x ) (x : replicate n x )
{ applying all }
x == x ∧ all (== x ) (replicate n x )
{ applying == }
True ∧ all (== x ) (replicate n x )
{ applying ∧ }
all (== x ) (replicate n x )
{ induction hypothesis }
True
Exercise 5.1
Base case:
=
[ ] ++ [ ]
{ applying ++ }
[]
Inductive case:
(x : xs) ++ [ ]
{ applying ++ }
x : (xs ++ [ ])
=
{ induction hypothesis }
x : xs
=
27
Exercise 5.2
Base case:
[ ] ++ (ys ++ zs)
{ applying ++ }
ys ++ zs
=
{ unapplying ++ }
([ ] ++ ys) ++ zs
=
Inductive case:
(x : xs) ++ (ys ++ zs)
{ applying ++ }
x : (xs ++ (ys ++ zs))
=
{ induction hypothesis }
x : ((xs ++ ys) ++ zs)
=
{ unapplying ++ }
(x : (xs ++ ys)) ++ zs
=
{ unapplying ++ }
((x : xs) ++ ys) ++ zs
=
Exercise 6
The three auxiliary results are all general properties that may be useful in other
contexts, whereas the single auxiliary result is specific to this application.
Exercise 7
Base case:
map f (map g [ ])
{ applying the inner map }
map f [ ]
=
{ applying map }
[]
=
{ unapplying map }
map (f ◦ g) [ ]
=
Inductive case:
=
=
=
=
=
map f (map g (x : xs))
{ applying the inner map }
map f (g x : map g xs)
{ applying the outer map }
f (g x ) : map f (map g xs)
{ induction hypothesis }
f (g x ) : map (f ◦ g) xs
{ unapplying ◦ }
(f ◦ g) x : map (f ◦ g) xs
{ unappling map }
map (f ◦ g) (x : xs)
28
Exercise 8
Base case:
take 0 xs ++ drop 0 xs
{ applying take, drop }
[ ] ++ xs
=
{ applying ++ }
xs
=
Base case:
take (n + 1) [ ] ++ drop (n + 1) [ ]
{ applying take, drop }
[ ] ++ [ ]
=
{ applying ++ }
[]
=
Inductive case:
take (n + 1) (x : xs) ++ drop (n + 1) (x : xs)
{ applying take, drop }
(x : take n xs) ++ (drop n xs)
=
{ applying ++ }
x : (take n xs ++ drop n xs)
=
{ induction hypothesis }
x : xs
=
Exercise 9
Definitions:
leaves (Leaf )
leaves (Node l r )
= 1
= leaves l + leaves r
nodes (Leaf )
nodes (Node l r )
= 0
= 1 + nodes l + nodes r
Property:
leaves t = nodes t + 1
Base case:
nodes (Leaf n) + 1
{ applying nodes }
0+1
=
{ applying + }
1
=
{ unapplying leaves }
leaves (Leaf n)
=
29
Inductive case:
nodes (Node l r ) + 1
{ applying nodes }
1 + nodes l + nodes r + 1
=
{ arithmetic }
(nodes l + 1) + (nodes r + 1)
=
{ induction hypotheses }
leaves l + leaves r
=
{ unapplying leaves }
leaves (Node l r )
=
Exercise 10
Base case:
comp (Val n) c
=
{ applying comp }
comp (Val n) ++ c
=
{ applying comp }
[PUSH n ] ++ c
=
{ applying ++ }
PUSH n : c
Inductive case:
=
=
=
=
=
=
comp (Add x y) c
{ applying comp }
comp (Add x y) ++ c
{ applying comp }
(comp x ++ comp y ++ [ADD ]) ++ c
{ associativity of ++ }
comp x ++ (comp y ++ ([ADD ] ++ c))
{ applying ++ }
comp x ++ (comp y ++ (ADD : c))
{ induction hypothesis for y }
comp x ++ (comp y (ADD : c))
{ induction hypothesis for x }
comp x (comp y (ADD : c))
In conclusion, we obtain:
comp (Val n) c
comp (Add x y) c
= PUSH n : c
= comp x (comp y (ADD : c))
30
Solutions to Exercises
Graham Hutton
University of Nottingham
Contents
Chapter 1 - Introduction
1
Chapter 2 - First steps
3
Chapter 3 - Types and classes
4
Chapter 4 - Defining functions
5
Chapter 5 - List comprehensions
7
Chapter 6 - Recursive functions
9
Chapter 7 - Higher-order functions
13
Chapter 8 - Functional parsers
15
Chapter 9 - Interactive programs
19
Chapter 10 - Declaring types and classes
21
Chapter 11 - The countdown problem
23
Chapter 12 - Lazy evaluation
24
Chapter 13 - Reasoning about programs
26
Chapter 1 - Introduction
Exercise 1
=
=
=
=
=
double (double 2)
{ applying the inner double }
double (2 + 2)
{ applying double }
(2 + 2) + (2 + 2)
{ applying the first + }
4 + (2 + 2)
{ applying the second + }
4+4
{ applying + }
8
or
=
=
=
=
=
=
double (double 2)
{ applying the outer double }
(double 2) + (double 2)
{ applying the second double }
(double 2) + (2 + 2)
{ applying the second + }
(double 2) + 4
{ applying double }
(2 + 2) + 4
{ applying the first + }
4+4
{ applying + }
8
There are a number of other answers too.
Exercise 2
sum [x ]
{ applying sum }
x + sum [ ]
=
{ applying sum }
x +0
=
{ applying + }
x
=
Exercise 3
(1)
product [ ]
=
product (x : xs) =
1
x ∗ product xs
1
(2)
=
=
=
=
=
product [2, 3, 4]
{ applying product }
2 ∗ (product [3, 4])
{ applying product }
2 ∗ (3 ∗ product [4])
{ applying product }
2 ∗ (3 ∗ (4 ∗ product [ ]))
{ applying product }
2 ∗ (3 ∗ (4 ∗ 1))
{ applying ∗ }
24
Exercise 4
Replace the second equation by
qsort (x : xs) =
qsort larger ++ [x ] ++ qsort smaller
That is, just swap the occurrences of smaller and larger .
Exercise 5
Duplicate elements are removed from the sorted list. For example:
=
=
=
=
=
qsort [2, 2, 3, 1, 1]
{ applying qsort }
qsort [1, 1] ++ [2] ++ qsort [3]
{ applying qsort }
(qsort [ ] ++ [1] ++ qsort [ ]) ++ [2] ++ (qsort [ ] ++ [3] ++ qsort [ ])
{ applying qsort }
([ ] ++ [1] ++ [ ]) ++ [2] ++ ([ ] ++ [3] ++ [ ])
{ applying ++ }
[1] ++ [2] ++ [3]
{ applying ++ }
[1, 2, 3]
2
Chapter 2 - First steps
Exercise 1
(2 ↑ 3) ∗ 4
(2 ∗ 3) + (4 ∗ 5)
2 + (3 ∗ (4 ↑ 5))
Exercise 2
No solution required.
Exercise 3
n
= a ‘div ‘ length xs
where
a = 10
xs = [1, 2, 3, 4, 5]
Exercise 4
last xs
=
head (reverse xs)
last xs
=
xs !! (length xs − 1)
init xs
=
take (length xs − 1) xs
init xs
=
reverse (tail (reverse xs))
or
Exercise 5
or
3
Chapter 3 - Types and classes
Exercise 1
[Char ]
(Char , Char , Char )
[(Bool , Char )]
([Bool ], [Char ])
[[a ] → [a ]]
Exercise 2
[a ] → a
(a, b) → (b, a)
a → b → (a, b)
Num a ⇒ a → a
Eq a ⇒ [a ] → Bool
(a → a) → a → a
Exercise 3
No solution required.
Exercise 4
In general, checking if two functions are equal requires enumerating all possible argument values, and checking if the functions give the same result for each of these
values. For functions with a very large (or infinite) number of argument values, such
as values of type Int or Integer, this is not feasible. However, for small numbers of
argument values, such as values of type of type Bool , it is feasible.
4
Chapter 4 - Defining functions
Exercise 1
halve xs
= splitAt (length xs ‘div ‘ 2) xs
halve xs
= (take n xs, drop n xs)
where
n = length xs ‘div ‘ 2
or
Exercise 2
(a)
safetail xs
=
if null xs then [ ] else tail xs
(b)
safetail xs | null xs
| otherwise
=
=
[]
tail xs
(c)
safetail [ ]
safetail xs
=
=
[]
tail xs
or
safetail [ ]
=
safetail ( : xs) =
[]
xs
Exercise 3
(1)
False ∨ False
False ∨ True
True ∨ False
True ∨ True
=
=
=
=
False ∨ False
∨
= False
= True
False ∨ b
True ∨
b
True
False
True
True
True
(2)
(3)
=
=
(4)
b ∨ c | b == c
| otherwise
=
=
b
True
5
Exercise 4
a∧b
=
if a then
if b then True else False
else
False
=
if a then b else False
Exercise 5
a∧b
Exercise 6
mult
= λx → (λy → (λz → x ∗ y ∗ z ))
6
Chapter 5 - List comprehensions
Exercise 1
sum [x ↑ 2 | x ← [1 . . 100]]
Exercise 2
= [x |
replicate n x
← [1 . . n ]]
Exercise 3
pyths n
[(x , y, z ) | x
y
z
x
=
← [1 . . n ],
← [1 . . n ],
← [1 . . n ],
↑ 2 + y ↑ 2 == z ↑ 2]
Exercise 4
perfects n
=
[x | x ← [1 . . n ], sum (init (factors x )) == x ]
Exercise 5
concat [[(x , y) | y ← [4, 5, 6]] | x ← [1, 2, 3]]
Exercise 6
positions x xs
=
find x (zip xs [0 . . n ])
where n = length xs − 1
Exercise 7
scalarproduct xs ys
=
sum [x ∗ y | (x , y) ← zip xs ys ]
Exercise 8
shift
shift n c | isLower c
| isUpper c
| otherwise
::
=
=
=
Int → Char → Char
int2low ((low2int c + n) ‘mod ‘ 26)
int2upp ((upp2int c + n) ‘mod ‘ 26)
c
freqs
freqs xs
::
=
String → [Float ]
[percent (count x xs ) n | x ← [’a’ . . ’z’]]
where
xs = map toLower xs
n = letters xs
low2int
low2int c
::
=
Char → Int
ord c − ord ’a’
7
int2low
int2low n
::
=
Int → Char
chr (ord ’a’ + n)
upp2int
upp2int c
::
=
Char → Int
ord c − ord ’A’
int2upp
int2upp n
::
=
Int → Char
chr (ord ’A’ + n)
letters
letters xs
::
=
String → Int
length [x | x ← xs, isAlpha x ]
8
Chapter 6 - Recursive functions
Exercise 1
(1)
m ↑0
= 1
m ↑ (n + 1) = m ∗ m ↑ n
(2)
=
=
=
=
=
2↑3
{ applying ↑ }
2 ∗ (2 ↑ 2)
{ applying ↑ }
2 ∗ (2 ∗ (2 ↑ 1))
{ applying ↑ }
2 ∗ (2 ∗ (2 ∗ (2 ↑ 0)))
{ applying ↑ }
2 ∗ (2 ∗ (2 ∗ 1))
{ applying ∗ }
8
Exercise 2
(1)
=
=
=
=
=
length [1, 2, 3]
{ applying length }
1 + length [2, 3]
{ applying length }
1 + (1 + length [3])
{ applying length }
1 + (1 + (1 + length [ ]))
{ applying length }
1 + (1 + (1 + 0))
{ applying + }
3
(2)
drop 3 [1, 2, 3, 4, 5]
{ applying drop
drop 2 [2, 3, 4, 5]
=
{ applying drop
drop 1 [3, 4, 5]
=
{ applying drop
drop 0 [4, 5]
=
{ applying drop
[4, 5]
=
}
}
}
}
9
(3)
init [1, 2, 3]
{ applying init }
1 : init [2, 3]
=
{ applying init }
1 : 2 : init [3]
=
{ applying init }
1 :2 : []
=
{ list notation }
[1, 2]
=
Exercise 3
and [ ]
and (b : bs)
=
=
True
b ∧ and bs
concat [ ]
concat (xs : xss)
=
=
[]
xs ++ concat xss
replicate 0
replicate (n + 1) x
=
=
[]
x : replicate n x
(x : ) !! 0
( : xs) !! (n + 1)
=
=
x
xs !! n
elem x [ ]
elem x (y : ys) | x == y
| otherwise
=
=
=
False
True
elem x ys
Exercise 4
merge [ ] ys
merge xs [ ]
merge (x : xs) (y : ys)
= ys
= xs
= if x ≤ y then
x : merge xs (y : ys)
else
y : merge (x : xs) ys
Exercise 5
halve xs
= splitAt (length xs ‘div ‘ 2) xs
msort [ ]
= []
msort [x ] = [x ]
msort xs = merge (msort ys) (msort zs)
where (ys, zs) = halve xs
10
Exercise 6.1
Step 1: define the type
sum
:: [Int ] → Int
Step 2: enumerate the cases
sum [ ]
sum (x : xs)
=
=
Step 3: define the simple cases
sum [ ]
sum (x : xs)
= 0
=
Step 4: define the other cases
sum [ ]
sum (x : xs)
= 0
= x + sum xs
Step 5: generalise and simplify
sum
sum
::
=
Num a ⇒ [a ] → a
foldr (+) 0
Exercise 6.2
Step 1: define the type
take
:: Int → [a ] → [a ]
Step 2: enumerate the cases
take
take
take
take
0 []
0 (x : xs)
(n + 1) [ ]
(n + 1) (x : xs)
=
=
=
=
Step 3: define the simple cases
take
take
take
take
0 []
0 (x : xs)
(n + 1) [ ]
(n + 1) (x : xs)
=
=
=
=
[]
[]
[]
Step 4: define the other cases
take
take
take
take
0 []
0 (x : xs)
(n + 1) [ ]
(n + 1) (x : xs)
=
=
=
=
[]
[]
[]
x : take n xs
Step 5: generalise and simplify
take
::
=
take 0
take (n + 1) [ ]
=
take (n + 1) (x : xs) =
Int → [a ] → [a ]
[]
[]
x : take n xs
11
Exercise 6.3
Step 1: define the type
last
:: [a ] → [a ]
Step 2: enumerate the cases
last (x : xs) =
Step 3: define the simple cases
last (x : xs) | null xs
| otherwise
= x
=
Step 4: define the other cases
last (x : xs) | null xs
| otherwise
= x
= last xs
Step 5: generalise and simplify
last
::
last [x ]
=
last ( : xs) =
[a ] → [a ]
x
last xs
12
Chapter 7 - Higher-order functions
Exercise 1
map f (filter p xs)
Exercise 2
all p
=
and ◦ map p
any p
=
or ◦ map p
takeWhile [ ] = [ ]
takeWhile p (x : xs)
|px
= x : takeWhile p xs
| otherwise = [ ]
dropWhile [ ]
dropWhile p (x
|px
| otherwise
= []
: xs)
= dropWhile p xs
= x : xs
Exercise 3
map f
=
foldr (λx xs → f x : xs) [ ]
filter p
=
foldr (λx xs → if p x then x : xs else xs) [ ]
Exercise 4
dec2nat
foldl (λx y → 10 ∗ x + y) 0
=
Exercise 5
The functions being composed do not all have the same types. For example:
sum
:: [Int ] → Int
map (↑2)
:: [Int ] → [Int ]
filter even
:: [Int ] → [Int ]
Exercise 6
curry
curry f
::
=
((a, b) → c) → (a → b → c)
λx y → f (x , y)
uncurry
uncurry f
::
=
(a → b → c) → ((a, b) → c)
λ(x , y) → f x y
13
Exercise 7
chop8
=
unfold null (take 8) (drop 8)
map f
=
unfold null (f ◦ head ) tail
iterate f
=
unfold (const False) id f
Exercise 8
encode
encode
::
=
String → [Bit ]
concat ◦ map (addparity ◦ make8 ◦ int2bin ◦ ord )
decode
decode
::
=
[Bit ] → String
map (chr ◦ bin2int ◦ checkparity ) ◦ chop9
addparity
addparity bs
::
=
[Bit ] → [Bit ]
(parity bs) : bs
parity
::
parity bs | odd (sum bs) =
| otherwise
=
[Bit ] → Bit
1
0
chop9
chop9 [ ]
chop9 bits
::
=
=
[Bit ] → [[Bit ]]
[]
take 9 bits : chop9 (drop 9 bits)
checkparity
checkparity (b : bs)
| b == parity bs
| otherwise
::
[Bit ] → [Bit ]
=
=
bs
error "parity mismatch"
Exercise 9
No solution required.
14
Chapter 8 - Functional parsers
Exercise 1
int
=
do char ’-’
n ← nat
return (−n)
+++nat
Exercise 2
comment
=
do string "--"
many (sat (
= ’\n’))
return ()
Exercise 3
(1)
expr
KK
u
KK
u
u
zu
%
expr
exprI
+
uu III
u
zu
$
expr
expr
+
term
term
term factor
factor
factor
nat
2
nat
3
nat
4
(2)
expr I
ss III
yss
$
exprI
expr
+
uu III
zuu
$
expr
expr
+
term
factor
nat
2
term
factor
term
factor
nat
3
nat
4
15
Exercise 4
(1)
expr I
III
u
u
u
$
zu
expr
+
term
factor
term
factor
nat
nat
2
3
(2)
expr
termI
t
II
I$
yttt
∗
factor
termG
GGG
ww
w
G#
{
w
∗
factor
nat
term
factor
nat
2
nat
3
4
(3)
expr K
ss KKK
yss
%
expr
+
term
factorI
term
III
uuu
II
$
zuuu expr
)
factor
(
JJJ
tt
JJ
zttt
$
expr
+
term
nat
factor
nat
2
term
factor
nat
3
16
4
Exercise 5
Without left-factorising the grammar, the resulting parser would backtrack excessively
and have exponential time complexity in the size of the expression. For example, a
number would be parsed four times before being recognised as an expression.
Exercise 6
expr
= do t ← term
do symbol "+"
e ← expr
return (t + e)
+++ do symbol "-"
e ← expr
return (t − e)
+++ return t
term
= do f ← factor
do symbol "*"
t ← term
return (f ∗ t )
+++ do symbol "/"
t ← term
return (f ‘div ‘ t )
+++ return f
Exercise 7
(1)
factor
::=
atom (↑ factor | epsilon)
atom
::=
(expr ) | nat
factor
factor
:: Parser Int
= do a ← atom
do symbol "^"
f ← factor
return (a ↑ f )
+++ return a
(2)
atom
atom
::
=
Parser Int
do symbol "("
e ← expr
symbol ")"
return e
+++ natural
17
Exercise 8
(a)
expr
::=
expr − nat | nat
nat
::=
0 | 1 | 2 | ···
expr
= do e ← expr
symbol "-"
n ← natural
return (e − n)
+++ natural
(b)
(c)
The parser loops forever without producing a result, because the first
operation it performs is to call itself recursively.
(d)
expr
= do n ← natural
ns ← many (do symbol "-"
natural)
return (foldl (−) n ns)
18
Chapter 9 - Interactive programs
Exercise 1
readLine
= get ""
get xs
= do x ← getChar
case x of
’\n’ → return xs
’\DEL’ → if null xs then
get xs
else
do putStr "\ESC[1D \ESC[1D"
get (init xs)
→ get (xs ++ [x ])
Exercise 2
No solution available.
Exercise 3
No solution available.
Exercise 4
No solution available.
Exercise 5
No solution available.
Exercise 6
type Board
=
[Int ]
initial
initial
::
=
Board
[5, 4, 3, 2, 1]
finished
finished b
::
=
Board → Bool
all (== 0) b
valid
valid b row num
::
=
Board → Int → Int → Bool
b !! (row − 1) ≥ num
move
move b row num
::
=
newline
newline
::
=
Board → Int → Int → Board
[if r == row then n − num else n
| (r , n) ← zip [1 . . 5] b ]
IO ()
putChar ’\n’
19
putBoard
putBoard [a, b, c, d , e ]
::
=
Board → IO ()
do putRow 1 a
putRow 2 b
putRow 3 c
putRow 4 d
putRow 5 e
putRow
putRow row num
::
=
Int → Int → IO ()
do putStr (show row )
putStr ": "
putStrLn (stars num)
stars
stars n
::
=
Int → String
concat (replicate n "* ")
getDigit
getDigit prom
::
=
String → IO Int
do putStr prom
x ← getChar
newline
if isDigit x then
return (ord x − ord ’0’)
else
do putStrLn "ERROR: Invalid digit"
getDigit prom
nim
nim
::
=
IO ()
play initial 1
play
play board player
::
=
Board → Int → IO ()
do newline
putBoard board
if finished board then
do newline
putStr "Player "
putStr (show (next player ))
putStrLn " wins!!"
else
do newline
putStr "Player "
putStrLn (show player )
r ← getDigit "Enter a row number: "
n ← getDigit "Stars to remove : "
if valid board r n then
play (move board r n) (next player )
else
do newline
putStrLn "ERROR: Invalid move"
play board player
next
next 1
next 2
::
=
=
Int → Int
2
1
20
Chapter 10 - Declaring types and classes
Exercise 1
mult m Zero
mult m (Succ n)
= Zero
= add m (mult m n)
Exercise 2
occurs m (Leaf n)
=
occurs m (Node l n r ) =
m == n
case compare m n of
LT → occurs m l
EQ → True
GT → occurs m r
This version is more efficient because it only requires one comparison for each node,
whereas the previous version may require two comparisons.
Exercise 3
leaves (Leaf )
leaves (Node l r )
=
=
balanced (Leaf )
=
balanced (Node l r ) =
1
leaves l + leaves r
True
abs (leaves l − leaves r ) ≤ 1
∧ balanced l ∧ balanced r
Exercise 4
halve xs
=
balance [x ] =
balance xs =
splitAt (length xs ‘div ‘ 2) xs
Leaf x
Node (balance ys) (balance zs)
where (ys, zs) = halve xs
Exercise 5
data Prop
= · · · | Or Prop Prop | Equiv Prop Prop
eval s (Or p q)
eval s (Equiv p q)
= eval s p ∨ eval s q
= eval s p == eval s q
vars (Or p q)
vars (Equiv p q)
= vars p ++ vars q
= vars p ++ vars q
Exercise 6
No solution available.
21
Exercise 7
data Expr
= Val Int | Add Expr Expr | Mult Expr Expr
type Cont
= [Op ]
data Op
= EVALA Expr | ADD Int | EVALM Expr | MUL Int
eval
eval (Val n) ops
eval (Add x y) ops
eval (Mult x y) ops
::
=
=
=
Expr → Cont → Int
exec ops n
eval x (EVALA y : ops)
eval x (EVALM y : ops)
exec
exec
exec
exec
exec
exec
::
=
=
=
=
=
Cont → Int → Int
n
eval y (ADD n : ops)
exec ops (n + m)
eval y (MUL n : ops)
exec ops (n ∗ m)
[] n
(EVALA y : ops) n
(ADD n : ops) m
(EVALM y : ops) n
(MUL n : ops) m
:: Expr → Int
= eval e [ ]
value
value e
Exercise 8
instance Monad Maybe where
return
:: a → Maybe a
return x
= Just x
(>
>=)
Nothing >
>=
(Just x ) >
>= f
:: Maybe a → (a → Maybe b) → Maybe b
= Nothing
= f x
instance Monad [ ] where
return
:: a → [a ]
return x = [x ]
(>
>=)
xs >
>= f
:: [a ] → (a → [b ]) → [b ]
= concat (map f xs)
22
Chapter 11 - The countdown problem
Exercise 1
choices xs
=
[zs | ys ← subs xs, zs ← perms ys ]
Exercise 2
removeone x [ ]
= []
removeone x (y : ys)
| x == y
= ys
| otherwise
= y : removeone x ys
isChoice [ ]
isChoice (x : xs) [ ]
isChoice (x : xs) ys
= True
= False
= elem x ys ∧ isChoice xs (removeone x ys)
Exercise 3
It would lead to non-termination, because recursive calls to exprs would no longer be
guaranteed to reduce the length of the list.
Exercise 4
> length [e | ns ← choices [1, 3, 7, 10, 25, 50], e ← exprs ns ]
33665406
> length [e | ns ← choices [1, 3, 7, 10, 25, 50], e ← exprs ns, eval e
= [ ]]
4672540
Exercise 5
Modifying the definition of valid by
valid Sub x y
valid Div x y
= True
= y
= 0 ∧ x ‘mod ‘ y == 0
gives
> length [e | ns ← choices [1, 3, 7, 10, 25, 50], e ← exprs ns , eval e
= [ ]]
10839369
Exercise 6
No solution available.
23
Chapter 12 - Lazy evaluation
Exercise 1
(1)
2 ∗ 3 is the only redex, and is both innermost and outermost.
(2)
1 + 2 and 2 + 3 are redexes, with 1 + 2 being innermost.
(3)
1 + 2, 2 + 3 and fst (1 + 2, 2 + 3) are redexes, with the first of these being
innermost and the last being outermost.
(4)
2 ∗ 3 and (λx → 1 + x ) (2 ∗ 3) are redexes, with the first being innermost
and the second being outermost.
Exercise 2
Outermost:
fst (1 + 2, 2 + 3)
{ applying fst }
1+2
=
{ applying + }
3
=
Innermost:
fst (1 + 2, 2 + 3)
{ applying the first + }
fst (3, 2 + 3)
=
{ applying + }
fst (3, 5)
=
{ applying fst }
3
=
Outermost evaluation is preferable because it avoids evaluation of the second argument, and hence takes one less reduction step.
Exercise 3
mult 3 4
{ applying mult }
(λx → (λy → x ∗ y)) 3 4
=
{ applying λx → (λy → x ∗ y) }
(λy → 3 ∗ y) 4
=
{ applying λy → 3 ∗ y }
3∗4
=
{ applying ∗ }
12
=
24
Exercise 4
fibs
0 : 1 : [x + y | (x , y) ← zip fibs (tail fibs)]
=
Exercise 5
(1)
fib n
=
fibs !! n
(2)
head (dropWhile (≤ 1000) fibs)
Exercise 6
repeatTree
repeatTree x
:: a → Tree a
= Node t x t
where t = repeatTree x
takeTree
takeTree 0
takeTree (n + 1) Leaf
takeTree (n + 1) (Node l x r )
::
=
=
=
replicateTree
replicateTree n
:: Int → a → Tree a
= takeTree n ◦ repeatTree
Int → Tree a → Tree a
Leaf
Leaf
Node (takeTree n l ) x (takeTree n r )
25
Chapter 13 - Reasoning about programs
Exercise 1
last
::
last [x ]
=
last ( : xs) =
[a ] → a
x
last xs
init
::
=
init [ ]
init (x : xs) =
[a ] → [a ]
[]
x : init xs
or
or
foldr1
::
=
foldr1 [x ]
foldr1 f (x : xs) =
(a → a → a) → [a ] → a
x
f x (foldr1 f xs)
There are a number of other answers too.
Exercise 2
Base case:
add Zero (Succ m)
{ applying add }
Succ m
=
{ unapplying add }
Succ (add Zero m)
=
Inductive case:
add (Succ n) (Succ m)
{ applying add }
Succ (add n (Succ m))
=
{ induction hypothesis }
Succ (Succ (add n m))
=
{ unapplying add }
Succ (add (Succ n) m)
=
Exercise 3
Base case:
add Zero m
{ applying add }
m
=
{ property of add }
add m Zero
=
26
Inductive case:
add (Succ n) m
{ applying add }
Succ (add n m)
=
{ induction hypothesis }
Succ (add m n)
=
{ property of add }
add m (Succ n)
=
Exercise 4
Base case:
all (== x ) (replicate 0 x )
{ applying replicate }
all (== x ) [ ]
=
{ applying all }
True
=
Inductive case:
=
=
=
=
=
all (== x ) (replicate (n + 1) x )
{ applying replicate }
all (== x ) (x : replicate n x )
{ applying all }
x == x ∧ all (== x ) (replicate n x )
{ applying == }
True ∧ all (== x ) (replicate n x )
{ applying ∧ }
all (== x ) (replicate n x )
{ induction hypothesis }
True
Exercise 5.1
Base case:
=
[ ] ++ [ ]
{ applying ++ }
[]
Inductive case:
(x : xs) ++ [ ]
{ applying ++ }
x : (xs ++ [ ])
=
{ induction hypothesis }
x : xs
=
27
Exercise 5.2
Base case:
[ ] ++ (ys ++ zs)
{ applying ++ }
ys ++ zs
=
{ unapplying ++ }
([ ] ++ ys) ++ zs
=
Inductive case:
(x : xs) ++ (ys ++ zs)
{ applying ++ }
x : (xs ++ (ys ++ zs))
=
{ induction hypothesis }
x : ((xs ++ ys) ++ zs)
=
{ unapplying ++ }
(x : (xs ++ ys)) ++ zs
=
{ unapplying ++ }
((x : xs) ++ ys) ++ zs
=
Exercise 6
The three auxiliary results are all general properties that may be useful in other
contexts, whereas the single auxiliary result is specific to this application.
Exercise 7
Base case:
map f (map g [ ])
{ applying the inner map }
map f [ ]
=
{ applying map }
[]
=
{ unapplying map }
map (f ◦ g) [ ]
=
Inductive case:
=
=
=
=
=
map f (map g (x : xs))
{ applying the inner map }
map f (g x : map g xs)
{ applying the outer map }
f (g x ) : map f (map g xs)
{ induction hypothesis }
f (g x ) : map (f ◦ g) xs
{ unapplying ◦ }
(f ◦ g) x : map (f ◦ g) xs
{ unappling map }
map (f ◦ g) (x : xs)
28
Exercise 8
Base case:
take 0 xs ++ drop 0 xs
{ applying take, drop }
[ ] ++ xs
=
{ applying ++ }
xs
=
Base case:
take (n + 1) [ ] ++ drop (n + 1) [ ]
{ applying take, drop }
[ ] ++ [ ]
=
{ applying ++ }
[]
=
Inductive case:
take (n + 1) (x : xs) ++ drop (n + 1) (x : xs)
{ applying take, drop }
(x : take n xs) ++ (drop n xs)
=
{ applying ++ }
x : (take n xs ++ drop n xs)
=
{ induction hypothesis }
x : xs
=
Exercise 9
Definitions:
leaves (Leaf )
leaves (Node l r )
= 1
= leaves l + leaves r
nodes (Leaf )
nodes (Node l r )
= 0
= 1 + nodes l + nodes r
Property:
leaves t = nodes t + 1
Base case:
nodes (Leaf n) + 1
{ applying nodes }
0+1
=
{ applying + }
1
=
{ unapplying leaves }
leaves (Leaf n)
=
29
Inductive case:
nodes (Node l r ) + 1
{ applying nodes }
1 + nodes l + nodes r + 1
=
{ arithmetic }
(nodes l + 1) + (nodes r + 1)
=
{ induction hypotheses }
leaves l + leaves r
=
{ unapplying leaves }
leaves (Node l r )
=
Exercise 10
Base case:
comp (Val n) c
=
{ applying comp }
comp (Val n) ++ c
=
{ applying comp }
[PUSH n ] ++ c
=
{ applying ++ }
PUSH n : c
Inductive case:
=
=
=
=
=
=
comp (Add x y) c
{ applying comp }
comp (Add x y) ++ c
{ applying comp }
(comp x ++ comp y ++ [ADD ]) ++ c
{ associativity of ++ }
comp x ++ (comp y ++ ([ADD ] ++ c))
{ applying ++ }
comp x ++ (comp y ++ (ADD : c))
{ induction hypothesis for y }
comp x ++ (comp y (ADD : c))
{ induction hypothesis for x }
comp x (comp y (ADD : c))
In conclusion, we obtain:
comp (Val n) c
comp (Add x y) c
= PUSH n : c
= comp x (comp y (ADD : c))
30
