The Australian National University School of Computing
Dirk Pattinson and
Semester 2, 2021 Practical Session 4
Foundations of Computation
The practical contains a number of exercises designed for the students to practice the course content. During the practical session, the tutor will work through some of these exercises while students will be responsible for completing the remaining exercises in their own time. There is no expectation that all the exercises will be covered in the practical session.
Covers: Lecture Material Week 4
At the end of this tutorial, you will be able to prove programs by induction on lists and trees.
Exercise 1 Associativity of List Concatenation
We know that list concatenation is associative, i.e that
xs ++ (ys ++ zs) = (xs ++ ys) ++ zs holds for all lists xs, ys and zs. Prove this using list induction. Precisely state
• The property that you are proving, including all quantifiers
• What you need to show for the base case and in the inductive step • What you are assuming as induction hypothesis.
We show that
by list induction. That is, we use the induction rule to show
∀xs.∀ys.∀zs.xs ++ (ys ++ zs) = (xs ++ ys) ++ zs
∀xs.P (xs)
P(xs)=∀ys.∀zs.xs ++ (ys ++ zs) = (xs ++ ys) ++ zs An alternative (easier) way would be to treat ys and zs as constants and show that
∀xs.xs ++ (ys ++ zs) = (xs ++ ys) ++ zs and then argue that – since ys and zs were arbitrary, this holds for all ys and zs.
Base Case. We show that
P([])=∀ys.∀zs.[] ++ (ys ++ zs) = ([] ++ ys) ++ zs
Let zs and ys be arbitrary lists. Then
[] ++ (ys ++ zs) = ys ++ zs — by A1
= ([] ++ ys) ++ zs — by A1
Step Case. We show that ∀x.∀xs.P (xs) → P (x : xs). So let x and xs be arbitrary and assume the inductive hypothesis
∀ys.∀zs.xs ++ (ys ++ zs) = (xs ++ ys) ++ zs For arbitrary ys and zs we then need to show that
(x:xs) ++ (ys ++ zs)
We argue as follows:
(x:xs) ++ (ys ++ zs)
= ((x:xs) ++ ys) ++ zs
= x : (xs ++ (ys ++ zs))
= x : ((xs ++ ys) ++ zs)
= (x : (xs ++ ys)) ++ zs
= ((x:xs) ++ ys) ++ zs
which finishes the proof.
Exercise 2 Tree Induction
Consider the definition of binary trees given in the lectures
data Tree a = Nul | Node (Tree a) a (Tree a)
and the following two functions:
size :: Tree a -> Int
size Nul = 0
size (Node l x r) = 1 + size l + size r
mirror :: Tree a -> Tree a
mirror Nul = Nul
mirror (Node l x r) = Node (mirror r) x (mirror l)
— C1 — C2
— M1 — M2
size tcountsthenumberofnodesintandmirror tobtainsthemirroredtreet. Establish, using structural induction, that mirror preserves the size of the tree. Solution.
We establish that the following
P(t) = (size t = size (mirror t)) holds for all trees t by structural induction.
Base case: P(Nul). We show that
size Nul = size (mirror Nul)
by means of the following calculation:
size (mirror Nul)
= size Nul — by M1
Step case: We show that
∀t1.∀x.∀t2.P (t1) ∧ P (t2) → P (Node t1 x t2) We separate the induction hypothesis for the left and the right subtree:
size (mirror t1) = size t1
size (mirror t2) = size t2
Proof Goal. For arbitrary a, show that P
size (mirror (Node t1 x t2)) = size (Node t1 x t2)
size (mirror (Node t1 x t2))
= size (Node (mirror t2) x (mirror t1))
= 1 + size (mirror t2) + size (mirror t1)
= 1 + size (mirror t1) + size (mirror t2)
= 1 + size t1 + size (mirror t2)
= 1 + size t1 + size t2
= size (Node t1 x t2)
The proof is as follows:
— (we assume integers are commutative)
which finishes the proof.
Exercise 3 Euclid’s Algorithm
We can formulate Euclid’s Algorithm in Haskell as follows:
euclid :: Int -> Int -> Int
euclid n 0 = n
euclid 0 m = m
euclid n m = euclid (max n m – min n m) (min n m)
Our aim is to show that euclid terminates for all inputs n, m > 0.
1. Define a termination measure, that is, a function t : N × N → N such that t(n′, m′) < t(n, m) where n′ and m′ are theargumentsofarecursivecalltoeuclidinthedefinitionofeuclid n m,whenevertherecursivecallwould be evaluated.
2. Prove that your termination measure t, defined above, indeed has this property.
Solution. We put t(n, m) = n + m. For a recursive call, we then need to show that t(max(n, m) − min(n, m), min(n, m)) < t(n, m)
and we do this by distinguishing cases. Case 1: n ≥ m. Then
t(max(n, m) − min(n, m), min(n, m)) = t(n − m, m) = n − m + m = n < n + m = t(n, m) as m > 0 (as otherwise we would be in the base cse).
Case 2: n < m. Then similarly
t(max(n, m) − min(n, m), min(n, m)) = t(m − n, n) = m − n + n = m < m + n = t(n, m)
as n > 0 (as otherwise we would be in the other base case).
Exercise 4 A simple but useful fact
Showthatxs ++ [] = xsholdsforalllistsxs,usinglistinduction.
Wehavetoshowthat∀xs.xs ++ [] = xs.
BaseCase.Weshow[] ++ [] = [].ButthisispreciselythedefinitionofA1forys = [].
Step Case. We show that ∀xs.∀x.xs ++ [] = xs → (x:xs) ++ [] = x:xs. So let x and xs be arbitrary and assume the induction hypothesis
We show that This follows, as
(x:xs) ++ [] = x:(xs ++ [])
= x:xs — by IH
Exercise 5
xs ++ [] = xs. (IH) (x:xs) ++ [] = x:xs.
List Reversal and Concatenation
Consider the following definition of list reversal:
reverse [] = []
reverse (x : xs) = reverse xs ++ [x]
— R1 — R2
The aim of this exercise is to show that list reversal interacts with concatenation in the following way:
∀xs.∀ys.reverse (xs ++ ys) = reverse ys ++ reverse xs.
Uselistinductiontoestablishthatreverse (xs ++ ys) = reverse ys ++ reverse xsforalllistsxsand ys. You may find it helpful to use associativity of concatenation as well as other properties that we have proved in earlier exercises. Precisely state
• The property that you are proving, including all quantifiers
• What you need to show for the base case and in the inductive step • What you are assuming as induction hypothesis.
Weshowthat∀xs.∀ys.reverse (xs ++ ys) = reverse ys ++ reverse xs
Base Case. We show that ∀ys.reverse ([] ++ ys) = reverse ys ++ reverse []. Let ys be arbitrary.
reverse ([] ++ ys) = reverse (ys)
= reverse ys ++ []
= reverse ys ++ reverse []
as we had to show.
Step Case. We let x and xs be arbitrary and assume that
and show that
∀ys.reverse (xs ++ ys) = reverse ys ++ reverse xs (IH)
∀ys.reverse ((x:xs) ++ ys) = reverse ys ++ reverse (x:xs) So let ys be arbitrary. We have
reverse ((x:xs) ++ ys) = reverse (x:(xs ++ ys))
= reverse (xs ++ ys) ++ [x]
= (reverse ys ++ reverse xs) ++ [x]
= reverse ys ++ (reverse xs ++ [x])
= reverse ys ++ reverse (x:xs)
and the equality is proven.
Exercise 6 Arguing by Cases
–byA2 –byR2 –byIH
— assoc (Ex1) –byR2
elem z (xs ++ ys) = elem z xs || elem z ys
holds for all lists xs and ys and all z. Precisely state
• The property that you are proving, including all quantifiers
• What you need to show for the base case and in the inductive step • What you are assuming as induction hypothesis.
You will want to argue by cases.
We use list induction to show
∀xs.∀ys.∀z.elem z (xs ++ ys) = elem z xs || elem z ys.
Base Case. We show P ([]), that is
∀ys.∀z.elem z ([] ++ ys) = elem z [] || elem z ys
We let ys and z be arbitrary to obtain:
elem z ([] ++ ys) = elem z ys
= False || elem z ys
= elem z [] || elem z ys
Step Case. We assume that
P(xs)=∀ys.∀z.elem z (xs ++ ys) = elem z xs || elem z ys (IH)
and show P (x : xs), that is,
∀ys.∀z.elem z ((x:xs) ++ ys) = elem z (x:xs) || elem z ys.
We distinguish the following cases for arbitrary ys and z: • Case z == x
elem z ((x:xs) ++ ys)
• Case z /= x
elem z ((x:xs) ++ ys)
Exercise 7
z(x:(xs++ys))
z (x:xs) || elem z ys
z(x:(xs++ys)) z(xs++ys) zxs||elemzys
z (x:xs) || elem z ys
–byA2 –byE2 –byO1 –byE2
–byA2 –byE3 –byIH –byE3
Consider the following function slinky that you may recognise from an earlier exercise:
slinky :: [a] -> [a] -> [a]
slinky [] ys = ys
slinky (x:xs) ys = slinky xs (x:ys)
Prove each of the following equations
(a) slinky (slinky xs ys) zs = slinky ys (xs ++ zs)
(b) slinky xs (slinky ys zs) = slinky (ys ++ xs) zs
(c) slinky xs (ys ++ zs) = slinky xs ys ++ zs
by list induction, and state explicitly
• The property that you are proving, including all quantifiers
• What you need to show for the base case and in the inductive step • What you are assuming as induction hypothesis.
Hint. Think about precisely which variable is the variable you should induct on. Solution.
— S1 — S2
1. We show that
More Properties
∀xs.∀ys.∀zs.slinky (slinky xs ys) zs = slinky ys (xs ++ zs).
Base Case. Show that
∀ys.∀zs.slinky (slinky [] ys) zs = slinky ys ([] ++ zs).
slinky (slinky [] ys) zs
= slinky ys zs — S1
= slinky ys ([] ++ zs) — A1
Step Case. Let x and xs be arbitrary and assume the inductive hypothesis
∀ys.∀zs.slinky (slinky xs ys) zs = slinky ys (xs ++ zs) — (IH).
We have to show that
∀ys.∀zs.slinky (slinky (x:xs) ys) zs = slinky ys ((x:xs) ++ zs).
slinky (slinky (x:xs) ys) zs
= slinky (slinky xs (x:ys)) zs
= slinky (x:ys) (xs ++ zs)
= slinky ys (x:(xs ++ zs))
= slinky ys ((x:xs) ++ zs)
2. Here, we consider xs as a constant, and show that the property
P(ys) = ∀zs. slinky xs (slinky ys zs) = slinky (ys ++ xs) zs holds for all ys.
Base Case. Show that
slinky xs (slinky [] zs)
This is just a matter of unfolding equations:
slinky xs (slinky [] zs)
Step Case.
= slinky ([] ++ xs) zs
= slinky xs zs
= slinky ([] ++ xs) zs
Assume the inductive hypothesis for an arbitrary list as in place of ys:
∀zs. slinky xs (slinky as zs) = slinky (as ++ xs) zs — (IH).
∀zs. slinky xs (slinky (a:as) zs) = slinky ((a:as) ++ xs) zs. slinky xs (slinky (a:as) zs) = slinky xs (slinky as (a:zs)) — by S2
= slinky (as ++ xs) (a:zs)
= slinky (a:(as ++ xs)) zs
= slinky ((a:as) ++ xs) zs
(*) Note, zs in the IH is instantiated to a : zs when it is used in the proof 3. Here, we treat zs as a constant and establish that the property
— by IH (*)
P(xs)=∀ys. slinky xs (ys ++ zs) = slinky xs ys ++ zs holds for all lists xs. We do this by induction on xs.
Base Case. Show that
slinky [] (ys ++ zs)
We prove this by unfolding equations:
slinky [] (ys ++ zs)
Step Case.
Assume the inductive hypothesis
= slinky [] ys ++ zs
= ys ++ zs
= slinky [] ys ++ zs
∀ys. slinky as (ys ++ zs) = slinky as ys ++ zs — (IH).
Prove that, for any a,
∀ys. slinky (a:as) (ys ++6zs) = slinky (a:as) ys ++ zs.
slinky (a:as) (ys ++ zs) = slinky as (a:(ys ++ zs))
= slinky as ((a:ys) ++ zs)
= slinky as (a:ys) ++ zs
= slinky (a:as) ys ++ zs
(*) Note, ys in the IH is instantiated to a : ys when it is used in the proof
Exercise 8 More Efficient List Reversal
Consider the following, more efficient, version of list reversal:
— by IH (*)
rev_a [] ys = ys
rev_a (x:xs) ys = rev_a xs (x:ys)
— RA1 — RA2
rev2 xs = rev_a xs []
Theaimofthisexerciseistoshowthat∀xs.reverse xs = rev2 xs.Noticethatrev2isdefinedintermsofreva
and that the second (accumulating) argument of rev a changes in the recursive call.
1. Find a property that describes the relationship between reverse and rev a where the second argument is an
explicit variable. This property will have the form
∀xs.∀ys…. reverse xs … ys … = … rev a xs ys … .
2. Establish this property by list induction.
3. Use the validity of this property to establish the original goal, that is, ∀xs.reverse xs = rev2 xs.
Hint. In the proof, you may (and probably want to) use some of the equations that have been established in earlier
exercises. Also note that [x] is just a notation for the list x:[].
1. We find the property
∀xs.∀ys.reverse xs ++ ys = rev a xs ys.
2. We show the above property by list induction.
Base Case. Show that ∀ys.rev a [] ys = reverse [] ++ ys. Let ys be arbitrary. Then we have
rev_a [] ys
= [] ++ ys
= reverse [] ++ ys
Step Case. We show that
∀xs.∀x(∀ys.rev a xs ys = reverse xs ++ ys) → (∀ys.rev a (x:xs) ys = reverse (x:xs) ++ ys)
So let x and xs be arbitrary and assume that
∀ys.rev a xs ys = reverse xs ++ ys (IH).
We show that this property also holds for x:xs in place of xs. Let ys be arbitrary.
rev_a (x:xs) ys
= rev_a xs (x:ys) — RA2
= reverse xs ++ (x:ys) — IH
= reverse xs ++ x:([] ++ ys) — A1
= reverse xs ++ ([x] ++ ys) — A2
= (reverse xs ++ [x]) ++ ys — assoc (Ex1)
= reverse (x:xs) ++ ys — R2
which finishes the proof.
3. We now show that reverse xs = rev2 xs for all lists xs.
= rev_a xs [] — RR
=reversexs++[] –aswehaveshowninpart2 = reverse xs — Ex4
Exercise 9
Double List Reversal
Consider the definition of list reversal given in the previous exercise, i.e. the function
reverse [] = [] — R1
reverse (x : xs) = reverse xs ++ [x] — R2
The aim of this exercise is to show that
As for the other exercises, precisely state
reverse (reverse xs) = xs.
• The property that you are proving, including all quantifiers
• What you need to show for the base case and in the inductive step • What you are assuming as induction hypothesis.
Hint. In the proof, you may (and probably want to) use some of the equations that have been established in earlier exercises. Also note that [x] is just a notation for the list x:[].
Weprove∀xs.reverse (reverse xs) = xs. BaseCase.Weshowthatreverse (reverse []) = []:
reverse (reverse [])
= reverse [] — R1
= [] — R1
Step Case. We show that
∀xs.∀x.((reverse (reverse xs) = xs) → (reverse (reverse (x:xs)) = x:xs))
So let x and xs be arbitrary. We assume that
reverse (reverse xs) = xs (IH)
and show that the same property also holds with x:xs in place of xs. The argument is the following:
reverse (reverse (x:xs))
= reverse ((reverse xs) ++ [x])
= reverse [x] ++ reverse (reverse xs)
= reverse (x:[]) ++ xs
= (reverse [] ++ [x]) ++ xs
= ([] ++ [x]) ++ xs
= (x:[]) ++ xs
= x:([] ++ xs)
Appendix: Function definitions
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)
elem :: Eq a => a -> [a] -> Bool
elem y [] = False
elem y (x:xs)
| x == y = True
| otherwise = elem y xs
(||) :: Bool -> Bool -> Bool True || _ = True False || x =x
reverse :: [a] -> [a]
reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
map :: (a -> b) -> [a] -> [b]
map f [] = []
map f (x:xs) = (f x):(map f xs)
pref :: a -> [a] -> [a]
pref x l = x:l
— A1 — A2
— E2 — E3
— O1 — O2
— R1 — R2
— M1 — M2