CS代考 THE AUSTRALIAN NATIONAL UNIVERSITY – cscodehelp代写
THE AUSTRALIAN NATIONAL UNIVERSITY
Second Semester 2019
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 (PL)
Q1 (FOL)
Q3 (SI)
Q4 (HL)
Q5 (FSA)
Q6 (G)
Q7 (TM)
COMP1600/COMP6260 (Foundations of Computation) Page 1 of 32
Total
QUESTION 1 [14 marks] Propositional Logic
Consider the following formulae:
• ¬(p∧¬q)→(¬p∨q)
• (p→(q→p))∧((q→p)→p) • (¬p∨q)∧¬(p→q)
(a) Identify a formula in the given set of formulae above that is a contingency. Describe in one sentence what it means that a formula is a contingency. Hence, or otherwise, establish that the formula you have identified is a contingency.
QUESTION 1(a) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 2 of 32
(b) Identify a formula in the given set of formulae above that is a tautology. Give a proof of this formula in the calculus of natural deduction (using only the rules provided in Appendix 1, and justifying every inference step). Explain in one sentence why a natural deduction proof of a formula establishes that it is a tautology.
QUESTION 1(b) [5 marks]
(c) Identify a formula in the given set of formulae above that is a contradiction. Give a proof of the negation of this formula in the calculus of natural deduction (using only the rules provided in Appendix 1, and justifying every inference step). Describe in one sentence what it means that a formula is a contradiction.
QUESTION 1(c) [5 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 3 of 32
QUESTION 2 [13 marks]
A relation R ⊂ X × X is called Euclidean if it satisfies the formula ∀x∀y∀z(R(x,y) ∧ R(x,z) → R(y,z))
and recall that a relation is called symmetric if it satisfies ∀ x ∀ y(R(x, y) → R(y, x)),
reflexive if the formula ∀ x(R(x, x))
is valid for the relation, and connected if ∀x∀y(R(x,y) ∨ R(y,x))
is true for R.
(a) Consider the set X = N = {0, 1, 2 . . . } of natural numbers. Is the relation R, defined by
R(x, y) if and only if x ≤ y, a Euclidean relation? Justify your answer.
QUESTION 2(a) [3 marks]
First Order Logic
COMP1600/COMP6260 (Foundations of Computation) Page 4 of 32
(b) It is known that every symmetric relation is reflexive. Give a proof of this fact, that is, a proof of the rule
∀x∀y(R(x,y) ∨ R(y,x)) ∀ xR(x, x)
in natural deduction (using only the rules provided in Appendix 1, and justifying every inference step).
QUESTION 2(b) [4 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 5 of 32
(c) It is also known that every relation that is both Euclidean and reflexive is in fact symmet- ric. Give a proof of this fact, that is, a proof of the rule
(∀x∀y∀z(R(x,y) ∧ R(x,z) → R(y,z))) ∧ (∀x(R(x,x))) ∀x∀y(R(x,y) → R(y,x))
in natural deduction (using only the rules provided in Appendix 1, and justifying every inference step).
QUESTION 2(c) [6 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 6 of 32
QUESTION 3 [18 marks] Structural Induction
(a) Consider the following data type of integer-labelled binary trees data Tree = Nul | Node Tree Int Tree
and the functions
add :: Tree -> Int
add Nul = 0
add (Node l i r) = i + (add l) + (add r)
swap :: Tree -> Tree
swap Nul = Nul
swap (Node l i r) = Node ((swap r) i (swap l)) — S1.
The aim of this question is to show that swapping subtrees does not affect the sum of the values in the tree, i.e. to prove the formula
∀t(add t = add (swap t))
where t is of type Tree, by structural induction.
(i) State and prove the base case goal. QUESTION 3(a)(i)
[2 marks]
— A0 — A1
— S0
(ii) State the inductive hypotheses. QUESTION 3(a)(ii)
[1 mark]
COMP1600/COMP6260 (Foundations of Computation) Page 7 of 32
(iii) State the step case goal, including all quantifiers, and prove the step case goal. QUESTION 3(a)(iii) [4 marks]
(b) The evaluation of polynomials can be defined in Haskell using the function ev below ev :: [Int] -> Int -> Int
ev l x = pev l x 0
pev :: [Int] -> Int -> Int -> Int
pev [] x n = 0
pev (a:as) x n = a * (x ^ n) + (pev as x (n+1))
— E
— P0 — P1
where x^n is exponentiation in Haskell, i.e. x^n = xn.
Here polynomials are given as a list of coefficients, that is, given l = [a0, a1, …, an] the
function ev l x returns ni=0 ai · xi.
A different (and more efficient) way to evaluate polynomials is given by the so-called
that can be defined as follows:
hor :: [Int] -> Int -> Int
hor [] x = 0 — H0 hor(a:as)x=a+x* (horasx) –H1
The goal of this question is to prove that the Horner scheme indeed delivers the same value as the above sum. The first goal is to show that
∀l∀x∀n(pevlxn=xn *(horlx)) (†) by structural induction.
COMP1600/COMP6260 (Foundations of Computation) Page 8 of 32
(i) State and prove the base case goal, including all quantifiers, required to prove (†) by structural induction.
QUESTION 3(b)(i) [2 marks]
(ii) State the inductive hypothesis, including all quantifiers.
QUESTION 3(b)(ii) [1 mark]
(iii) State the step case goal, including all quantifiers, and prove the step case goal. QUESTION 3(b)(iii) [6 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 9 of 32
(iv) Hence, or otherwise, prove that ev l x = hor l x for all lists l of integers, and for all integers x.
QUESTION 3(b)(iv) [2 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 10 of 32
QUESTION 4 [15 marks] Hoare Logic (a) Consider the following program called log, where all variables are natural numbers:
while3*x < ado d := d + 1; x := x * 3
Starting with initial values d = 0 and x = 1, log calculates the integer logarithm of a to base 3, that is, the largest natural number d such that 3d ≤ a.
We wish to use Hoare Logic (Appendix 3) to show that:
{d=0 ∧ x=1 ∧ a>0}log{3d ≤a}
(i) Complete the table below by filling in the values of d and x after the first, second, etc. iteration of the loop, assuming that the loop executes at least four times. The initial values for d and x are given by the precondition of log.
QUESTION 4(a)(i) [1 mark]
loop iteration d x 001 1
2
3 4
(ii) Using the table above, derive an invariant P, that is, a relation between x, d and a, that holds both before the loop is being entered, and after each iteration of the loop body. The invariant needs to have the following three properties:
• it needs to be strong enough to imply the postcondition if the loop condition is
false:
P∧¬(3∗x
{P∧(3∗x
QUESTION 4(a)(iii) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 12 of 32
(b) Consider the following (annotated) program called NpowerM
[m ≥ 0 ∧ n > 0 ∧ r = 1 ∧ i = 0] whilei < mdo
r := r * n;
i := i + 1
[r = nm]
The function computes the nth power of m and leaves the result in r.
(i) Complete the table below by filling in the values of r and i after the first, second, etc. iteration of the loop, assuming that the loop executes at least four times. The initial values of r and i are given by the precondition of NpowerM.
QUESTION 4(b)(i) [1 mark]
loop iteration r i 010 1
2
3 4
(ii) Identify an invariant P for the loop. The invariant needs to have the following three properties:
• it needs to be strong enough to imply the postcondition if the loop condition is
false:
P ∧ ¬(i < m) → r = nm
• it needs to be weak enough so that it is implied by the precondition:
m≥0∧n>0∧r=1∧i=0→P • it must be an invariant, i.e
{P ∧ (i < m)} r := r * n; i := i + 1 {P}
must be provable.
State the invariant, no formal proof is required yet.
QUESTION 4(b)(ii)
[2 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 13 of 32
(iii) Identify a variant E for the loop. Using the same invariant P as in the previous exercise, the variant needs to have the following two properties:
• it must be ≥ 0 when the loop is entered, i.e.
P ∧ (i < m) → E ≥ 0
• it must decrease every time the loop body is executed, i.e.
[P∧i
QUESTION 6(b)(i) [3 marks]
(ii) Give a trace to show that your push-down automaton accepts the string 0011111# and another trace to show that it rejects the string 001111#.
QUESTION 6(b)(ii) [1 mark]
COMP1600/COMP6260 (Foundations of Computation) Page 21 of 32
(c) Consider the following Context Free grammar S→ S⊗S|T
T→p|q
over the alphabet Σ = {⊗, p, q}. Demonstrate that this grammar is ambiguous.
QUESTION 6(c) [2 marks]
(d) Give a context-free grammar that generates precisely the language given by the grammar in QUESTION 6(c) (above), but is not ambiguous, and give a parse tree that shows that your grammar generates the string p ⊗ q ⊗ p.
QUESTION 6(d) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 22 of 32
(e) Followingthealgorithmpresentedinlectures,convertthefollowingcontext-freegrammar to a non-deterministic PDA
S→ S⊗S|T T→p|q
QUESTION 6(e) [2 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 23 of 32
QUESTION 7 [12 marks] Turing Machines
(a) The following diagram shows a Turing machine. The input string is a string of 0’s and 1’s and the tape is blank to the left and to the right of the input string. Initially the head is at the leftmost character of the input string.
(i) For each of the strings 0101, 10110 and 1111000 determine the content of the tape after the machine has terminated with the given string as an input.
QUESTION 7(a)(i) [3 marks]
(ii) Given an arbitrary input string s, describe the content of the tape after the machine has terminated in terms of the input string s.
QUESTION 7(a)(ii) [3 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 24 of 32
(b) Design a Turing Machine that takes a string of the form s# where s ∈ {a, b}∗ and converts it to uppercase and mirrors it after the hash symbol #. For example, abbaa# should be replaced by ABBAA#AABBA on the tape. Assume that the tape is empty apart from the input and that the tape head is at the hash symbol initially. Include a brief description of the purpose of the individual states.
QUESTION 7(b) [6 marks]
COMP1600/COMP6260 (Foundations of Computation) Page 25 of 32
Additional answers. Clearly indicate the corresponding question and part.
Additional answers. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 26 of 32
Additional answers. Clearly indicate the corresponding question and part.
Additional answers. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 27 of 32
Additional answers: deliberately left like this for use in landscape mode. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 28 of 32
Additional answers: deliberately left like this for use in landscape mode. Clearly indicate the corresponding question and part.
COMP1600/COMP6260 (Foundations of Computation) Page 29 of 32
Appendix 1 — Natural Deduction Rules Propositional Calculus
(∧I)
(∨I)
(→I)
(¬I)
(¬E)
pq p∧qp∧q (∧ E)
p∧qpq [p] [q]
pp(∨E) p∨q q∨p
[p] .
. .
p∨qrr r
p p→q p→q q
q (→E)
[p] [¬p]
. .
F (PC) F ¬p p
(∀ I)
P(a)
(a arbitrary) ∀ x. P(x)
p ¬p F
(T)
(∀ E)
∃ x. P(x)
q (aisnotfreeinq)
Predicate Calculus
T
∀ x. P(x) P(a)
[P(a)] .
(∃ I) P(a) ∃x.P(x)
(∃ E)
q (a arbitrary)
COMP1600/COMP6260 (Foundations of Computation) Page 30 of 32
Appendix 2 — Truth Table Values
pqp∨qp∧qp→q¬pp⇔q TTTTTFT TFTFFFF FTTFTTF FFFFTTT
COMP1600/COMP6260 (Foundations of Computation) Page 31 of 32
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}
• While Loop (Total Correctness):
P ∧ b → E ≥ 0 [P ∧ b ∧ E = n] S [P ∧ E < n] [P] while b do S [P ∧ ¬ b]
where n is an auxiliary variable not appearing anywhere else.
COMP1600/COMP6260 (Foundations of Computation) Page 32 of 32
