COMP4161 T3/2024 Advanced Topics in Software Verification - Assignment 1

1. λ-Calculus (16 marks)

(a) Simplify the term $(pq)(\lambda p\cdot(\lambda q\cdot(\lambda r\cdot(q(rp))))))))$ syntactically by applying the syntactic conventions and rules. Justify your answer. (2 marks)

(b) Restore the omitted parentheses in the term $a(\lambda a b.(bc)a(bc))(\lambda b.cb)$ (but make sure you don’t change the term structure). (2 marks)

(c) Find the normal form of $(\lambda f\cdot\lambda x\cdot f(fx))(\lambda g\cdot\lambda y\cdot 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)

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

• $0\equiv\lambda fx,x$
• $1\equiv\lambda fx.fx$
• $2\equiv\lambda fx.f(fx)$
• $3\equiv\lambda fx.f(f(fx))...$ Define exp where exp m n beta-reduces to the Church Numeral representing $m^{n}$. Provide a justification of your answer. (6 marks)

2. Types (20 marks)

(a) Provide the most general type for the term $\lambda a b c.a(x b b)(c b)$. 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\Rightarrow'b)\Rightarrow('c\Rightarrow'a)\Rightarrow'c\Rightarrow'b$ (You don’t need to provide a type derivation, just the term). (4 marks)

(c) Explain why $\lambda x.xx$ is not typable. (3 marks)

(d) Find the normal form and its type of $(\lambda f x.f(x x))(\lambda y z.z)$. (3 marks)

(e) Is $(\lambda f x.f(x x))(\lambda y z.z)$ typable? Compare this situation with the Subject Reduction that you learned in the lecture. (5 marks)

3. Propositional Logic (29 marks)

(a) $x\to\neg\neg x$ (3 marks)

(b) $(X\to Y\to\neg X)\to X\to\neg Y$ (3 marks)

(c) $\neg\neg A\to A$ (4 marks)

(d) $\neg(A\land B)\to\neg A\vee\neg B$ (4 marks)

(e) $\neg(A\to B)\to A$ (4 marks)

(f) (continued)

(g) $(A\to B)\to((B\to C)\to A)\to B$ (5 marks)

4. Higher-Order Logic (35 marks)

(a) $(\forall x.\neg Px)=(\nexists x.Px)$ (4 marks)

(b) $(\exists x y.Pxy)=(\exists y x.Pxy)$ (4 marks)

(c) $(\exists x.Px\to Q)=((\forall x.Px)\to Q)$ (7 marks)

(d) $((\forall x.Px)\to(\exists x.Qx))=(\exists x.Px\to Qx)$ (7 marks)

(e) $\forall x.\neg Rx\to R(Mx)\Rightarrow\forall x.Rx\vee R(Mx)$ (6 marks)

(f) $\llbracket\forall x.\neg Rx\to R(Mx);\exists x.Rx\rrbracket\Rightarrow\exists x.Rx\land R(M(Mx))$ (7 marks)