COMP4161 T3/2024 Advanced Topics in Software Verification
Assignment 1
This assignment starts on Thursday 19th September 2024 and is due on Thursday 26th Septem- ber 2024 23:59:59. We will accept plain text (.txt) files, PDF (.pdf) files, and Isabelle theory (.thy) files. You are allowed to make late submissions up to five days (120 hours) after the deadline, but at a cost: -5 marks per day.
The assignment is take-home. This does NOT mean you can work in groups. Each submission is personal. For more information, see the plagiarism policy: https://student.unsw.edu.au/plagiarism
Copyright By PowCoder代写 加微信 powcoder
You are not allowed to use AI tools (such as ChatGPT or GitHub Copilot) to help you with technical content, or to develop definitions and proofs.
Submit using give on a CSE machine: give cs4161 a1 files …
For example:
(a) (b) (c)
give cs4161 a1 a1.thy a1.pdf
λ-Calculus (16 marks)
Simplify the term (pq)(λp.(λq.(λr.(q(rp))))) syntactically by applying the syntactic con-
ventions and rules. Justify your answer. (2 marks)
Restore the omitted parentheses in the term a(λab.(bc)a(bc))(λb.cb) (but make sure you don’t change the term structure). (2 marks)
Find the normal form of (λf.λx.f(fx))(λg.λy.g(g(gy))). Justify your answer by showing the reduction sequence. Each step in the reduction sequence should be a single β-reduction step. Underline or otherwise indicate the redex being reduced for each step. (6 marks)
Recall the encoding of natural numbers in lambda calculus (Church Numerals) seen in the lecture:
Define exp where exp m n beta-reduces to the Church Numeral representing mn. Provide a justification of your answer. (6 marks)
Types (20 marks)
Provide the most general type for the term λabc.a(xbb)(cb). Show a type derivation tree to justify your answer. Each node of the tree should correspond to the application of a single typing rule, and be labeled with the typing rule used. Under which contexts is the term type correct? (5 marks)
0 ≡ 1 ≡ 2 ≡ 3≡
λfx.fx λfx.f(fx)
λf x.f (f (f x))…
Find a closed lambda term that has the following type:
(’a ⇒ ’b) ⇒ (’c ⇒ ’a) ⇒ ’c ⇒ ’b
(You don’t need to provide a type derivation, just the term). (4 marks)
Explain why λx.xx is not typable. (3 marks)
Find the normal form and its type of (λfx.f(xx))(λyz.z). (3 marks)
Is (λfx.f(xx))(λyz.z) typable? Compare this situation with the Subject Reduction that you learned in the lecture. (5 marks)
Propositional Logic (29 marks)
(c) (d) (e)
Prove each of the following statements, using only the proof methods: rule, erule, assumption, cases, frule, drule, rule tac, erule tac, frule tac, drule tac, rename tac, and case tac; and using only the proof rules: impI, impE, conjI, conjE, disjI1, disjI2, disjE, notI, notE, iffI, iffE, iffD1, iffD2, ccontr, classical, FalseE, TrueI, conjunct1, conjunct2, and mp. You do not need to use all of these methods and rules.
(a) X −→ ¬ ¬ X
(b) (X −→ Y −→ ¬ X) −→ X −→ ¬ Y
(c) ¬ ¬ A −→ A
(d) ¬ (A ∧ B) −→ ¬ A ∨ ¬ B
(e) ¬ (A −→ B) −→ A
(f) (¬ A ∧ ¬ B) = (¬ (A ∨ B))
(g) (A −→ B) −→ ((B −→ C) −→ A) −→ B
4 Higher-Order Logic (35 marks)
(3 marks) (3 marks) (4 marks) (4 marks) (4 marks) (6 marks) (5 marks)
Prove each of the following statements, using only the proof methods and proof rules stated in the previous question, plus any of the following proof rules: allI, allE, exI, and exE. You do not need to use all of these methods and rules. You may use rules proved in earlier parts of the question when proving later parts.
(a) (∀x. ¬ P x) = P x)
(b) (∃x y. P x y) = (∃y x. P x y)
(c) (∃x. P x −→ Q) = ((∀x. P x) −→ Q)
(d) ((∀x. P x) −→ (∃x. Q x)) = (∃x. P x −→ Q x)
(e) ∀x. ¬ R x −→ R (M x) =⇒ ∀x. R x ∨ R (M x)
(f) [∀x. ¬ R x −→ R (M x); ∃x. R x] =⇒ ∃x. R x ∧ R (M (M x))
(4 marks) (4 marks) (7 marks) (7 marks) (6 marks) (7 marks)
程序代写 CS代考 加微信: powcoder QQ: 1823890830 Email: powcoder@163.com