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

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:

give cs4161 a1 a1.thy a1.pdf

1. -Calculus (16 marks)

   1. Simplify the term (pq)(p.(q.(r.(q(rp))))) syntactically by applying the syntactic con- ventions and rules. Justify your answer. (2 marks)

   2. Restore the omitted parentheses in the term a(ab.(bc)a(bc))(b.cb) (but make sure you dont change the term structure). (2 marks)

   3. 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)

   4. Recall the encoding of natural numbers in lambda calculus (Church Numerals) seen in the lecture:

      1. f x. x

      2. f x. f x

      3. f x. f (f x)

      4. f x. f (f (f x)) …

         Define exp where exp m n beta-reduces to the Church Numeral representing mn. Provide a justification of your answer. (6 marks)

2. Types (20 marks)

   1. 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)

   2. Find a closed lambda term that has the following type:

      (a b) (c a) c b

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

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

   4. Find the normal form and its type of (fx.f (xx))(yz.z). (3 marks)

   5. Is (fx.f (xx))(yz.z) typable? Compare this situation with the Subject Reduction that you learned in the lecture. (5 marks)

3. Propositional Logic (29 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)	X X				(3 marks)
   (b)	(X Y X)	X		Y	(3 marks)
   (c)	A A				(4 marks)
   (d)	(A B) A	B			(4 marks)
   (e)	(A B) A				(4 marks)
   (f)	( A B) = ( (A	B))			(6 marks)
   (g)	(A B) ((B C)		A) B		(5 marks)

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

   1. ( x. P x) = ( x. P x) (4 marks)

   2. ( x y. P x y) = ( y x. P x y) (4 marks)

   3. ( x. P x Q) = (( x. P x) Q) (7 marks)

   4. (( x. P x) ( x. Q x)) = ( x. P x Q x) (7 marks)

   5. x. R x R (M x) = x. R x R (M x) (6 marks)

   6. [[ x. R x R (M x); x. R x]] = x. R x R (M (M x)) (7 marks)