The Austalian National University School of Computing
Victor Rivera and
Semester 2, 2021 Assignment 2
Release: Due: Mode: Submit:
Friday, 03 September, 2021, 18:00 AEST
Friday, 01 October, 2021, 23:55 AEST
individual submissions only
as single pdf file via Wattle (scans of legible handwritten solutions are perfectly acceptable), here.
Foundations of Computation
Pledge of Academic Integrity and Originality statement1
I am committed to being a person of integrity. I pledge, as a member of the Australian National University community, to abide by and uphold the standards of academic integrity outlined in the ANU statement on honesty and plagiarism. I understand that it is wrong to ever misrepresent another person’s work as my own.
I am aware of the relevant legislation, and understand the consequences of me breaching those rules. I have read the COMP1600/COMP6260 academic integrity and pledge to abide by it.
I declare that everything I have submitted in this assignment was entirely my own work.
Name: UID:
Signature:
1Submissions without your name, UID and signature will not be marked. 1
Question 1 Structural induction over lists [3 + 6 + 3 + 13 Credits] Consider the functions tail and length defined on lists of an arbitrary type a
tail :: [a] -> [a]
tail [] = []
tail (x:xs) = xs
— T1 — T2
length :: [a] -> Int
length [] = 0 — L1
length (x:xs) = 1 + length xs — L2
together with the following function overlay that takes two lists (of an arbitrary type a) and puts the first list on top of the second:
overlay :: [a] -> [a] -> [a]
overlay [] ys = ys — O1
overlay (x:xs) ys = x:(overlay xs (tail ys)) — O2
The goal of this exercise is to show that
length (overlay xs ys) = max (length xs) (length ys) holds for all lists xs and ys.
a) What precisely should we prove by induction? State a property P(xs), including possible quan- tifiers, so that proving this property by induction implies the (above) goal of this exercise.
b) For your chosen property P, state (including possible quantifiers) and prove the base case goal.
c) State (including possible quantifiers) the inductive hypothesis of the proof.
d) State (including possible quantifiers) and prove the step case goal.
In all proofs indicate the justification (e.g. the line of a definition used) for each step. You may assume basic properties of the max function that computes the maximum of two numbers that you can justify with math.
a) As the argument ys changes in the recursive call, choose
P(xs)≡∀ys.length (overlay xs ys) = max (length xs) (length ys)
and show ∀xs.P(xs) by structural induction.
b) The base case goal is
∀ys.length (overlay [] ys) = max (length []) (length ys). To see that the base case goal holds, let ys be arbitrary. Then
length (overlay [] ys) = length ys
= max 0 (length ys)
= max (length []) (length ys)
c) The inductive hypothesis is
∀ys.length (overlay xs ys) = max (length xs) (length ys). 2
d) Our step case goal is to show
∀x.∀ys.length (overlay (x:xs) ys) = max (length (x:xs)) (length ys).
Let x and ys be arbitrary. We distinguish two cases and first consider that ys
length (overlay (x:xs)) ys = length (overlay (x:xs) []
= length (x:(overlay xs (tail [])))
= 1 + length (overlay xs (tail []))
= 1 + length (overlay xs [])
= 1 + max (length xs) (length [])) = 1 + max (length xs) 0 =1+lengthxs
= length (x:xs)
= max (length x:xs) 0
= max (length x:xs) (length [])
Now assume that ys = z:zs is a non-empty list. Then
length (overlay (x:xs)) ys = length (overlay (x:xs) (z:zs)
= length (x:(overlay xs (tail (z:zs))) — O2
= 1 + length (overlay xs (tail (z:zs)))– L2
= 1 + length (overlay xs zs) — T2
= 1 + max (length xs) (length zs) — IH, ys = zs
= max (1 + length xs) (1 + length zs) — math
= max (length x:xs) (1 + length zs) — L2
= max (length x:xs) (length z:zs) — L2
so that we get the desired result in both cases.
Question 2 Structural Induction on Trees [5 + 6 + 3 + 11 Credits]
Consider the following definition of binary trees of an arbitrary type a which only have elements at the leaves:
data LTree a = Leaf a | LNode (LTree a) (LTree a)
together with the functions height and leaves that compute the height, and the number of leaf nodes
in a tree, respectively.
height :: LTree a -> Int
height (Leaf x) = 0 — H1
height (LNode l r) = 1 + max (height l) (height r) — H2
leaves :: LTree a -> Int
leaves (Leaf x) = 1 — LE1
leaves (LNode l r) = leaves l + leaves r — LE2
The type LTree is different from the type Tree discussed in the lectures. An LTree is either a Leaf (that carries an element of type a), or an LNode, consisting of a right and left subtree (but no element of type a). Given that all elements of type LTree a have to be constructed in this way, this question is about identifying, the correct induction principle for LTrees, and using it to show that the property
P(t)≡leaves t≤2height t holds for all elements t of type LTree a.
= []. Then:
— as ys = []
— T1 –IH,ys=[] — L1
— as ys = z:zs
a) What induction principle allows us to prove that a property P(t) holds for all elements t of type LTree a?
State the premisses P1 and P2, including possible quantifiers, so that P1 P2 is a valid induction ∀t.P (t)
principle for LTrees, and briefly justify your answer.
To show that P(t) holds for all elements t of type LTree a, we use structural induction (and the
induction principle identified above in (a)).
b) State (including possible quantifiers) and prove the base case goal.
c) State (including possible quantifiers) the inductive hypotheses of the proof.
d) State (including possible quantifiers) and prove the step case goal.
In all proofs indicate the justification (e.g. the line of a definition used) for each step. You may assume basic properties of the max function that computes the maximum of two numbers that you can justify with math.
a) The induction principle is
∀x.P (leaf x) ∀l∀r.P (l) ∧ P (r) → P (LNode l r) .
Justification. Every element of LTree has to be constructed using a (finite) number of applications
of the two constructors.
For every element of LTree that we can can construct, we can construct the element and prove the property at the same time. For the first constructor, Leaf, this is given by the first premiss. If we use the second constructor, LNode, we are taking two elements of type LTree, for which we have already proved the property. Instantiating the universal quantifiers in the right hand premiss, we obtain that the property holds for the newly constructed element.
b) Base case goal: forall x. leaves (leaf x) <= 2^(height (leaf x)).
Let x be arbitrary. Then:
leaves (leaf x) = 1 -- LE1
= 2^0 -- maths
= 2^(height (leaf x)-- H1
c) Inductive Hypothesis: leaves l <= 2^(height l) /\ leaves r <= 2^(height r)
d) Step case goal: leaves (LNode l r) <= 2^(height (LNode l r)).
leaves (LNode l r) = leaves l + leaves r -- LE2
Question 3
= 2^(height (LNode l r)) --LE2.
Hoare Logic (partial correctness)
[5 + 15 + 5 Credits]
<= 2^(height l) + 2^(height r)-- IH
<= 2^(max (height l)(height r))
+ 2^(max (height l)(height r)) -- maths
<= 2^(max (height l)(height r) + 1) -- maths
The program below, called foo, calculates xn and stores the value in j (‘%’ is the modulo operation, e.g. 345 % 10 = 5, and ‘/’ is integer division – division without reminder, e.g. 345 / 10 = 34):
while (i > 0)
if i%2=0 then
v:=v*v;
i := i/2 body
j:=j*v;
(You may use the abbreviation ‘body’ to refer to the program inside the while loop.)
The goal of this exercise is to show that foo conforms to its specification, i.e. to show that the Hoare triple
{n ≥ 0 ∧ j = 1 ∧ i = n ∧ v = x} foo {j = xn}
a) Starting with the equation xn = j ∗ vi, find a suitable loop invariant I. Here suitable means
1. The invariant is established: n ≥ 0 ∧ j = 1 ∧ i = n ∧ v = x → I. 2. The postcondition is established: I ∧ ¬b → j = xn.
3. The invariant is invariant: {I ∧ b}body{I}.
where b ≡ i > 0 is the loop condition. State the invariant, no proof required (yet).
b) Using invariant I found in (a), or otherwise, prove that
{I ∧ b} body {I}
is valid in the Hoare-calculus for partial correctness. Justify each step in your proof.
c) Continue the proof in (b) to prove that
{n ≥ 0 ∧ j = 1 ∧ i = n ∧ v = x} foo {j = xn}
is valid in the Hoare-calculus for partial correctness. Justify each step in your proof.
a) We need to strengthen the given equation to be able to prove the validity of the tiple I ≡ xn = j ∗ vi ∧ i ≥ 0
b) Proving that {I ∧ b} body {I} is valid in the Hoare calculus
1. {xn =j∗vi−1∧i−1≥0}i := i-1{xn =j∗vi∧i≥0}(Assignment)
2. {xn =(j∗v)∗vi−1∧i−1>=0}j := j*v{xn =j∗vi−1∧i−1>=0}(Assignment)
3. xn =j∗vi∧i>=0∧i>0∧¬(i%2=0)→xn =(j∗v)∗vi−1∧i−1>=0(Logic)
Notingthat(j∗v)∗vi−1 =j∗v∗vi−1 =j∗vi (byMaths)hence
xn = j ∗ vi (which also appears in the LHS).
4. {xn =j∗vi∧i≥0∧i>0∧¬(i%2=0)} j := j*v;{xn =j∗vi−1∧i−1≥0} (Prec. Stre. 2, 3)
5.{xn =j∗vi∧i≥0∧i>0∧¬(i%2=0)}j:=j*v;i:=i-1{xn =j∗vi∧i≥0} (Sequence, 4, 1)
6. {xn =j∗vi/2∧i/2≥0}i := i/2{xn =j∗vi∧i≥0}(Assignment)
7. {xn =j∗(v∗v)i/2∧i/2≥0}v := v*v{xn =j∗vi/2∧i/2≥0}(Assignment)
8. xn =j∗vi∧i≥0∧i>0∧i%2=0→xn =j∗(v∗v)i/2∧i/2≥0(Logic)
Notingthatj∗(v∗v)i/2 =j∗(v2)i/2 =j∗(v(2∗i)/2)=j∗vi (byMaths)hence
xn = j ∗ vi (which also appears in the LHS).
9. {xn =j∗vi∧i≥0∧i>0∧i%2=0}v := v*v{xn =j∗vi/2∧i/2≥0}(Pre.Stre.7,8)
10. {xn =j∗vi∧i≥0∧i>0∧i%2=0}v := v*v;i := i/2{xn =j∗vi∧i≥0}(Sequence, 9, 6)
11. {xn =j∗vi∧i≥0∧i>0}body{xn =j∗vi∧i≥0}(Conditional,5,10)
c) Finishing up the proof
12. {xn =j∗vi∧i≥0}foo{xn =j∗vi∧i≥0∧¬(i>0)}(While,11).
13. n≥0∧j=1∧i=n∧v=x→xn =j∗vi∧i≥0(Logic)
14. {n≥0∧j=1∧i=n∧v=x}foo{xn =j∗vi∧i≥0∧¬(i>0)}(Prec.Stre.,12,13)
15. xn =j∗vi∧i≥0∧¬(i>0)→j=xn (Logic)
Noting that
i ≥ 0 ∧ ¬(i > 0) ↔ i≥0∧i≤0↔ i=0
16. {n≥0∧j=1∧i=n∧v=x}foo{j=xn}(Post.Weak.,14,15).
Question 4 Hoare Logic (total correctness) [5 + 15 + 5 Credits]
Consider the (same) program foo:
while (i > 0)
if i%2=0 then
v:=v*v;
i := i/2 body
j:=j*v;
We now only want to prove that this program terminates, i.e. without making guarantees about the variables after execution. In other words, we want to show that the triple
[True] foo [True]
is provable in the Hoare-calculus for total correctness.
a) Identify and state a suitable invariant I and variant E for the loop. Here suitable means
1. The invariant is established: True → I
2. The postcondition is established: I ∧ ¬b → True 3. Thevariantispositive:I∧b→E≥0
4. The variant decreases, and the invariant is invariant: [I ∧ b ∧ E = n] body [I ∧ E < n]. 6
where b ≡ i > 0 is the loop condition. State the variant and invariant, no proof is required (yet).
b) Using your variant E and invariant I in (a) give a proof of the Hoare triple
[I ∧ b ∧ E = n] body [I ∧ E < n]
in the Hoare-calculus for total correctness. Justify each step of your proof.
c) Continue the proof in (b) to prove that
[True] foo [True]
in the Hoare-calculus for total correctness. Justify each step of your proof.
a) WeuseI≡TrueandE≡i.
b) Proving
[I ∧ b ∧ E = n] body [I ∧ E < n] in the Hoare-calculus for total correctness
1. [True∧i−1
13. [T rue] foo [T rue ∧ ¬(i > 0)] (While, 12, 11) 14. True ∧ ¬(i > 0) → True (Logic)
15. [True] foo [True] (Post. Weak., 12, 14).
Appendix — Hoare Logic Rules (partial correctness)
Assignment:
{Q(e)} x := e {Q(x)}
Precondition Strengthening:
Ps →Pw {Pw}S{Q} {Ps} S {Q}
You can always replace predicates by equivalent predicates,
i.e. if Ps ↔ Pw; just label your proof step with ‘precondition equivalence’.
Postcondition Weakening:
{P}S{Qs} Qs →Qw {P} S {Qw}
You can always replace predicates by equivalent predicates,
i.e. if Qs ↔ Qw; just label your proof step with ‘postcondition equivalence’.
{P} S1 {Q} {Q} S2 {R} {P}S1;S2 {R}
Conditional:
{P ∧b} S1 {Q} {P ∧¬b} S2 {Q} {P} if b then S1 else S2 {Q}
While Loop:
{I ∧ b} S {I}
{I} while b do S {I ∧ ¬b}
Appendix — Hoare Logic Rules (total correctness)
Assignment:
[Q(e)] x := e [Q(x)]
Precondition Strengthening:
Ps →Pw [Pw]S[Q]
[Ps] S [Q]
You can always replace predicates by equivalent predicates,
i.e. if Ps ↔ Pw; just label your proof step with ‘precondition equivalence’. Postcondition Weakening:
[P]S[Qs] Qs →Qw [P] S [Qw]
You can always replace predicates by equivalent predicates,
i.e. if Qs ↔ Qw; just label your proof step with ‘postcondition equivalence’.
[P] S1 [Q] [Q] S2 [R]
[P]S1;S2 [R] Conditional:
[P ∧b] S1 [Q] [P ∧¬b] S2 [Q] [P] if b then S1 else S2 [Q]
While Loop (Total Correctness):
I ∧ b → E ≥ 0 [I ∧ b ∧ E = n] S [I ∧ E < n]
[I] while b do S [I ∧ ¬b]
where n is an auxiliary variable not appearing anywhere else.