THE AUSTRALIAN NATIONAL UNIVERSITY
Second Semester 2017
COMP1600/COMP6260 (Foundations of Computation)
Writing Period: 3 hours duration
Study Period: 15 minutes duration
Permitted Materials: One A4 page with hand-written notes on both sides Answer ALL questions
Total marks: 100
The questions are followed by labelled blank spaces into which your answers are to be written.
Additional answer panels are provided (at the end of the paper) should you wish to use more space for an answer than is provided in the associated labelled panels. If you use an additional panel, be sure to indicate clearly the question and part to which it is linked.
Student Number:
The following spaces are for use by the examiners.
Q1 (Logic)
COMP1600/COMP6260 (Foundations of Computation) Page 1 of 28
QUESTION 1 [8 marks] Logic (a) Consider the truth value assignment v that assigns the following truth values to the atomic
propositions p, q and r: v(p) = F, v(q) = T, v(r) = T.
Which of the following formulae evaluate to T under the assignment v, i.e. when the truth
values of p, q and r are given according to v? (1). (p→¬q)∨¬(r∧q)
(2). (¬p∨¬q)→(p∨¬r) QUESTION 1(a)
(3). ¬(¬p→q)∧r (4). ¬(¬p→q∧¬r)
(b) Consider the boolean function given by the following truth table:
x y z f(x,y,z) FFF T FFT F FTF F FTT T
x y z f(x,y,z) TFF F TFT T TTF T TTT T
Give a formula (in variables x, y and z) that represents the boolean function given above. Briefly argue why the formula indeed represents the boolean function.
QUESTION 1(b) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 2 of 28
QUESTION 2 [14 marks] Natural Deduction
The following questions ask for proofs using natural deduction. Present your proofs in the Fitch style as used in lectures. You may only use the introduction and elimination rules given in Appendix 1. Number each line and include justifications for each step in your proofs.
(a) Give a natural deduction proof of ¬a ∧ ¬b → ¬(a ∨ b)
QUESTION 2(a) [8 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 3 of 28
(b) Give a natural deduction proof of ∀ x(P(x) → ∃ y.P(y)).
QUESTION 2(b) [2 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 4 of 28
(c) Give a natural deduction proof of ∀ z.((∀ x.P(x) → Q(x)) ∧ ¬Q(z) → ¬P(z)). QUESTION 2(c) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 5 of 28
QUESTION 3 [16 marks] Structural Induction (a) Give an inductive proof the fact that consecutively mapping two functions over a list is
equivalent to 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 (g x)
(i) State and prove the base case goal QUESTION 3(a)(i)
— M1 — M2 — C
(ii) State the inductive hypothesis QUESTION 3(a)(ii)
COMP1600/COMP6260 (Foundations of Computation) Page 6 of 28
(iii) State and prove the step case goal.
QUESTION 3(a)(iii) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 7 of 28
(b) 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. (i) State and prove the base case of the proof of P:
QUESTION 3(b)(i) [2 marks]
(ii) State the inductive hypotheses of the proof of P.
QUESTION 3(b)(ii) [1 mark]
COMP1600/COMP6260 (Foundations of Computation) Page 8 of 28
(iii) State and prove the step case goal of the proof of P.
QUESTION 3(b)(iii) [6 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 9 of 28
QUESTION 4 [18 marks]
(a) For which programs S does {False} S {True} hold?
QUESTION 4(a)
(b) The following piece of code is called Half :
while (x < a)
x := x + 2;
y := y + 1;
We wish to use Hoare Logic (Appendix 3) to show that:
{True} Half {x = 2 ∗ y}
Hoare Logic
In the questions below (and your answers), we may refer to the loop code as Loop, the body of the loop (i.e. x:=x+2;y:=y+1;) as Body, and the initialisation assignments (i.e. x:=0;y:=0;) as Init.
(i) Given the desired postcondition {x = 2 ∗ y}, what is a suitable invariant for Loop? (Hint: notice that the postcondition is independent of the value of a.)
QUESTION 4(b)(i) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 10 of 28
(ii) Prove that your answer to the previous question is indeed a loop invariant. That is, if we call your invariant P, show that {P} Body {P}. Be sure to properly justify each step of your proof.
QUESTION 4(b)(ii)
(iii) Using the previous result and some more proof steps show that
{True} Half {x = 2 ∗ y}
Be sure to properly justify each step of your proof.
QUESTION 4(b)(iii)
COMP1600/COMP6260 (Foundations of Computation) Page 11 of 28
(iv) To prove total correctness of the program Half, identify and state a suitable variant for the loop. Using the same invariant P as above, the variant E should have the following two properties:
• itshouldbe≥0whentheloopisentered,i.e.P∧(x
(b) Demonstrate that the following grammar is ambiguous: E→0|1|E&E|(E)
QUESTION 6(b)
COMP1600/COMP6260 (Foundations of Computation) Page 16 of 28
(c) Give a grammar that generates the same language as above, but is not ambiguous. QUESTION 6(c) [3 marks]
(d) Demonstrate that the language generated by the grammar above is not regular. QUESTION 6(d) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 17 of 28
QUESTION 7 [19 marks] Turing Machines
(a) The following diagram shows a Turing machine, whose purpose is either to accept or reject the input string. The input string consists of ‘a’s and ‘b’s, and the rest of the tape is blank. (A string accepted if the machine reaches the halt state and rejected if the machine gets stuck in another state.) Initially the head is somewhere on the input string.
c E S2 ‘ b,R
Λdb c
(i) Give a general description of the purpose of states S0 and S1.
QUESTION 7(a)(i)
COMP1600/COMP6260 (Foundations of Computation) Page 18 of 28
(ii) What change is accomplished on the tape if the machine moves from state S1 to state S4?
QUESTION 7(a)(ii) [3 marks]
(iii) What is the language accepted by this machine?
QUESTION 7(a)(iii) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 19 of 28
(b) Design a Turing Machine which adds an even parity check bit to the right hand end of a bit string. The tape initially contains a non-empty string of binary digits and the read head is somewhere on the string. If there is an odd number of 1s in the string, the machine adds another 1 to the right hand end of the string and halts. If there is an even number of 1s in the string, the machine adds a 0 to the right hand end of the string and halts. For example:
0011000 =⇒ 0011000 0011010 =⇒ 0011010 0000000 =⇒ 0000000
QUESTION 7(b) [5 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 20 of 28
(c) Answer the following questions in one sentence.
(i) What is the class of languages recognised by Turing machines?
QUESTION 7(c)(i) [2 marks]
(ii) If a language L is recursively enumerable but not recursive, is the problem PL of L decidable?
QUESTION 7(c)(ii) [2 marks]
(iii) Are decidable problems easy to solve? If not, give an example that is hard to solve. QUESTION 7(c)(iii) [2 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 21 of 28
Additional answers. Clearly indicate the corresponding question and part.
Additional answers. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 22 of 28
Additional answers. Clearly indicate the corresponding question and part.
Additional answers. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 23 of 28
Additional answers: deliberately left like this for use in landscape mode. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 24 of 28
Additional answers: deliberately left like this for use in landscape mode. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 25 of 28
Appendix 1 — Natural Deduction Rules Propositional Calculus
pq p∧qp∧q (∧ E)
p∧qpq [p] [q]
pp(∨E) p∨q q∨p
p p→q p→q q
F (PC) F ¬p p
(a arbitrary) ∀ x. P(x)
q (aisnotfreeinq)
Predicate Calculus
∀ x. P(x) P(a)
(∃ I) P(a) ∃x.P(x)
q (a arbitrary)
COMP1600/COMP6260 (Foundations of Computation) Page 26 of 28
Appendix 2 — Truth Table Values
pqp∨qp∧qp→q¬pp⇔q TTTTTFT TFTFFFF FTTFTTF FFFFTTT
COMP1600/COMP6260 (Foundations of Computation) Page 27 of 28
Appendix 3 — Hoare Logic Rules
• Precondition Strengthening:
Ps → Pw {Pw}S{Q} {Ps} S {Q}
• Postcondition Weakening:
{P}S{Qs} Qs → Qw {P} S {Qw}
• Assignment:
{Q(e)} x := e {Q(x)} • Sequence:
{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:
{P ∧ b} S {P}
{P} while b do S {P ∧ ¬ b}
COMP1600/COMP6260 (Foundations of Computation) Page 28 of 28