THE AUSTRALIAN NATIONAL UNIVERSITY
Second Semester 2018
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.
The following spaces are for use by the examiners.
Q1 (Logic)
COMP1600/COMP6260 (Foundations of Computation) Page 1 of 27
QUESTION 1 [14 marks] Logic
Recall that two formulae are equivalent if they have have the same truth values for all variable assignments, and consider the following set of formulae:
• (p∧q)∨(¬p∧¬q) • ¬(p∨q)
• ¬p∨q • (q∧p)∨¬p
• (p∨¬q)∧(q∨¬p)
(a) Identify two formulae in the above set of formulae that are equivalent, and demonstrate their equivalence by means of a truth table.
QUESTION 1(a) [4 marks]
(b) Identify two formulae in the above set of formulae that are not equivalent, and demon- strate the fact that they are not equivalent by a variable assignment.
QUESTION 1(b) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 2 of 27
(c) State whether the following formulae are true or false where x, y and z range over the integers, and justify your answer briefly.
(1). ∀x∃y(2x−y)=0 (2). ∃x∀y(2x−y)=0 (3). ∀x∃y(x−2y)=0
QUESTION 1(c) [6 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 3 of 27
QUESTION 2 [16 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 the formula p ∨ (p → q). In this proof, you may use the law of excluded middle (LEM) p ∨ ¬p in addition to the rules provided in the appendix. That is, you may state p ∨ ¬p at any line in the proof, where p can stand for an arbitrary formula, and justify this by (LEM).
QUESTION 2(a) [8 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 4 of 27
(b) Give a natural deduction proof of the rule ∃xP(x) ∧ ∀x∀y(R(x,y) → P(y))
∃ x ∀ y(R(x, y) → P(y)) using only the rules in the appendix.
QUESTION 2(b) [8 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 5 of 27
QUESTION 3 [16 marks] Structural Induction (a) Consider the function subl that computes the list of sub-lists of a given list:
subl :: [a] -> [[a]]
subl [] = [[]] — S1
subl (x:xs) = (subl xs) ++ map (pref x) (subl xs) — S2
where the functions map, pref and ++ are given by:
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
(++) :: [a] -> [a] -> [a]
[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)
Show, using structural induction, that
length (subs l) = 2length l for all lists l of type a.
— M1 — M2
— A1 — A2
Here, we assume the standard definition of the length function
length [] = 0 — L1
length (x:xs) = 1 + length xs — L2
and you may use the fact that map preserves length, and the fact that length is compatible with concatenation, that is the equations
length (map f xs) = length xs — LM
length (xs ++ ys) = length xs + length ys — LA
in your proof, with justification as indicated.
In all proofs indicate the justification (eg, the line of a definition used) for each step.
COMP1600/COMP6260 (Foundations of Computation) Page 6 of 27
(i) State and prove the base case. QUESTION 3(a)(i)
(ii) State the inductive hypothesis. QUESTION 3(a)(ii)
(iii) State and prove the step case goal. QUESTION 3(a)(iii)
COMP1600/COMP6260 (Foundations of Computation) Page 7 of 27
(b) Give an inductive proof the fact that left folding is compatible with list concatenation. Consider the following definition of left folding:
foldl :: :: (b -> a -> b) -> b -> [a] -> b
foldl f z [] = z — F1
foldl f z (x:xs) = foldl f (f z x) xs — F2
and consider a fixed function f (of type b -> a -> b) and a fixed list ys (of elements of type b) and show that
P(xs)≡∀z(foldl f z (xs ++ ys) = foldl f (foldl f z xs) ys) holds for all lists xs (of elements of type a).
(i) State and prove the base case goal
QUESTION 3(b)(i) [2 marks]
(ii) State the inductive hypothesis
QUESTION 3(b)(ii) [1 mark]
COMP1600/COMP6260 (Foundations of Computation) Page 8 of 27
(iii) State and prove the step case goal.
QUESTION 3(b)(iii) [5 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 9 of 27
QUESTION 4 [16 marks] Hoare Logic (a) Specify a precondition P and a postcondition Q such that the Hoare-Triple {P} S {Q}
holds precisely for all programs S that never terminate. QUESTION 4(a)
(b) The following piece of code is called Rem
while (r >= n)
r := r – n;
q := q + 1
and computes two numbers, q and r, where • q is the integer quotient of x by n
• r is the remainder of the division of x by n.
We wish to use Hoare Logic (Appendix 3) to show that:
{True} Rem {x = n ∗ q + r}
In the questions below (and your answers), we may refer to the loop code as Loop, the body of the loop (i.e. r:-r-n;q:=q+1) as Body, and the initialisation assignments (i.e. r:=x;q:=0) as Init.
(i) Given the desired postcondition {x = n ∗ q + r}, what is a suitable invariant I for Loop?
QUESTION 4(b)(i) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 10 of 27
(ii) Prove that your answer to the previous question is indeed a loop invariant. That is, if we call your invariant I, show that {I} Body {I}. 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} Rem {x = n ∗ q + r}
Be sure to properly justify each step of your proof.
QUESTION 4(b)(iii)
COMP1600/COMP6260 (Foundations of Computation) Page 11 of 27
(iv) Explain why the corresponding Hoare-triple for total correctness, that is
[True]Rem[x = n ∗ q + r]
is not valid by giving a counter-example that shows that the triple above does not
hold in general.
QUESTION 4(b)(iv) [2 marks]
(v) Identify a precondition P such that the Hoare triple [P]Rem[x = n ∗ q + r]
is valid. Explain why the Hoare-triple now holds (no formal proof in Hoare Logic required).
QUESTION 4(b)(v) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 12 of 27
QUESTION 5 [13 marks] Finite State Automata (a) DesignaFiniteStateAutomatonthatrecognisesthelanguageofallstringsoverthealpha-
bet Σ = {a, b, c} where both the string ’abc’ and the string ’cba’ occurs as a substring. Here, a string s is a substring of a string w if w can be written as w1sw2.
QUESTION 5(a) [3 marks]
(b) Is your Finite State Automaton (above) deterministic or non-deterministic? Explain. QUESTION 5(b) [1 mark]
COMP1600/COMP6260 (Foundations of Computation) Page 13 of 27
(c) What language is recognised by the following Finite State Automaton?
Describe the language in English, and give a regular expression defining the language. QUESTION 5(c) [3 marks]
(d) Consider the statement ∀w∈Σ∗ .N∗(q2,w)=q2
Express this property in English. Why might it be relevant? QUESTION 5(d)
COMP1600/COMP6260 (Foundations of Computation) Page 14 of 27
(e) For the Finite State Automaton above, prove that ∀n ∈ N . N∗(q1,(aa)n) = q1
and hence, or otherwise, conlude that
∀n ∈ N . N∗(q0,(aa)n+1) = q1
QUESTION 5(e) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 15 of 27
QUESTION 6 [13 marks] Context-Free Grammars (a) Design a push-down automaton that recongnises precisely the language
{ambn | n>m>0}
QUESTION 6(a) [4 marks]
(b) Is your automaton deterministic, or non-deterministic? Briefly justify your answer. QUESTION 6(b) [1 mark]
(c) Demonstrate, using the pigeon hole principle or otherwise, that the language given above is not regular.
QUESTION 6(c) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 16 of 27
(d) Give a context-free grammar that generates precisely the language given above. QUESTION 6(d) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 17 of 27
QUESTION 7 [12 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 is a string of 0’s and 1’s and the tape is blank to
(d)(TutrhiengleMftacnhdintoesthI)eTrihgehftoolflotwheinignpTutrisntrginmg.acIhniintiealelxyptehcetshteoadfinisd,soamsietwshinepreuto,natshinegilneput binary number. There are no embedded blanks and nothing else on the tape.
00 ✣✢1 1 ✣✢Λ
❅’❅ ❅0,S Λ,L ✻ 0,S
0,S❅❅❅ ✄& ” 0 ❅❅ ❅ 0,R
❅✤✜Λ ✤✜Λ ✤✜ ❘❅ ✠’ ❘❅✛✘
❘❅ Λ,L Λ,S
✲ ✲ ✲✚✙ S S halt
✒’ ■❅ ✒’ ✒’
‘✻❅ ‘ ‘1❅1’
‘ ❅ Λ,L ‘ Λ” 1,R
1,S” ❅❅ ” ‘
1 ✤ ✜1 , S Λ , L ✤❄ ✜1 , S
(i) For each of the strings 010101, 101100010 and 1111000 determine the content of
(i) Fortheeactahpoefatfhterinthpeutmsac0h1i0n1e0h1a,st1e0rm11i0n0at0e1d0wainthdth1e11g1iv0e0n0s,twrihnagtawsiallnbienpthuet.onthe
tape when the Turing machine halts.
QUESTION 7(a)(i)
QUESTION 5(d)(i)
(ii) What does this machine do, in general? QUESTION 5(d)(ii)
COMP1600/COMP6260 (Foundations of Computation) Page 18 of 27
COMP2600 (Formal Methods in Software Engineering) Page 24 of 32
(ii) Givenaninputstrings,describetheoutputafterthemachinehasterminatedoninput string s.
QUESTION 7(a)(ii) [3 marks]
(iii) Explain (no formal proof required) why the machine will always terminate, regard- less of the given input string.
QUESTION 7(a)(iii) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 19 of 27
(b) DesignaTuringMachinethatwilltakeapairofbinarynumbers,separatedbyahashsym- bol (#), and reverses their order. That is, 0101#1111 should be replaced by 1111#0101 on the tape. Assume that the tape is empty apart from the input and that the tape head is somewhere over the input initially. Include a brief description of the purpose of the individual states.
QUESTION 7(b) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 20 of 27
Additional answers. Clearly indicate the corresponding question and part.
Additional answers. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 21 of 27
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 27
Additional answers: deliberately left like this for use in landscape mode. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 23 of 27
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 27
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 25 of 27
Appendix 2 — Truth Table Values
pqp∨qp∧qp→q¬pp⇔q TTTTTFT TFTFFFF FTTFTTF FFFFTTT
COMP1600/COMP6260 (Foundations of Computation) Page 26 of 27
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 27 of 27