COMP4161 T3/2025 Advanced Topics in Software Verification Assignment 1

Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

COMP4161 T3/2025

Advanced Topics in Software Verification

Assignment 1

This assignment starts on Tuesday 23rd September 2025 and is due on Friday 3rd October 2025 23:59:59  (Sydney time).  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 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.

We expect that submitted Isabelle proofs work.  We do not expect to see “red” error markers in Isabelle/jEdit.  Incomplete proofs can be skipped using sorry so that other parts can be marked. We may choose not to continue marking after encountering errors.

Submit using give on a CSE machine:

give  cs4161  a1 files . . .

For example:

give  cs4161  a1  a1.thy  a1.pdf

1 λ-Calculus (18 marks)

(a)  Simplify the term  (x(yz))(λz.(λy.(λx.((xy)z)))) syntactically by applying the syntactic conventions and rules. Justify your answer.  (3 marks)

(b)  Restore the omitted parentheses in the term pqr(λr.pq)(λpq.r(pq)r) (but make sure you don’t change the term structure).  (3 marks)

(c) Find the β-normal form of (λf.λx.f (f (f (fx))))(λg.λy.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)

(d)  Recall the encoding of booleans and their operations in lambda calculus seen in the lecture:

true        =    λx y. x

false      =    λx y. y

ifthen    =    λz x y. z x y

Define (in Isabelle) the operators for implication imply, and exclusive or exclusive_or using the definitions of true, false and ifthen.  (4 marks)

(e) We have provided in Isabelle a proof of the lemma that ifthen  true  false  x = false using unfold and refl.  Explain (informally) what the refl theorem states and explain why it can be used to prove the lemma.  (2 marks)

2 Types (20 marks)

(a)  Provide the most general type for the term λfxy.g(yx)(fy).  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)

(b) Find a closed lambda term that has the following type:

('a ⇒ 'b) ⇒ ('b ⇒ 'a ⇒ 'c) ⇒ 'a ⇒ 'c

(You don’t need to provide a type derivation, just the term).  (4 marks)

(c) Explain why λx.xx is not typable.  (3 marks)

(d) Find the βη-normal form and its type of (λfx.x)(λyz.zzy).  (3 marks)

(e) Is (λfx.x)(λyz.zzy) typable? Compare this situation with the Subject Reduction that you learned in the lecture.  (5 marks)

3 Propositional Logic (30 marks)

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)  A  -→  →  →  A                                                                                                                         (3 marks)

(b)  →  →  A  -→  A                                                                                                                         (3 marks)

(c)  (A  -→  →  B  -→  →  A)  -→  A  -→  B                                                                                 (4 marks)

(d)  →  (X  Λ  Y)  -→  →  Y  V  → X                                                                                               (4 marks)

(e)  →  (X  -→  Y)  -→  X                                                                                                             (4 marks)

(f)  (→  X  Λ  → Y)  =   (→  (Y  V  X))                                                                                            (6 marks)

(g) X  =  Y  -→  ((Y  -→  Z)  -→  X)  -→  Y                                                                             (6 marks)

4 Higher-Order Logic (32 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.

(a)  (∀ x  y .  P  x  y)  =   (∀ y  x .  P  x  y)                                                                                    (4 marks)

(b)  (∃ x .  P  x)  =   (¬  (∀ x .  ¬ P  x))                                                                                     (5 marks)

(c)  (∀ x .  P  x)  —→  Q  =⇒  ∃ x .  P  x  —→  Q                                                                             (5 marks)

(d)  (∀ x .  P  x)  —→  (∃ x .  Q  x)  =⇒  ∃ x .  P  x  —→  Q  x                                                           (5 marks)

(e) ∀ x .  ¬ P  x  —→  P   (Q  x)  =⇒  ∀ x .  P  x  ∨  P   (Q  x)                                                           (6 marks)

(f)  [[∀ x .  P  x  ∨  P   (Q  x);  ∃ x .  P  x]]  =⇒  ∃ x .  P  x  ∧  P   (Q  (Q  x))                                   (7 marks)





2025-09-29

Discrete Mathematics