COMP4630/8670 (Semester 2, 2019)
Assignment for Typed Lambda Calculus
Due: Friday 25 October 2019, 11:59am
Submission information: Submit your assignment either
• preferably on paper, to a lecturer of the course, or in the assignment submission boxes on the
ground floor of the CSIT building, or
• as a PDF file (scanned handwritten papers are acceptable, provided they are written using a dark
pen, on white paper, and are otherwise readable, A4 size (or smaller), leaving a reasonable margin
to permit printing, etc) via email to [email protected]
by the due date.
Please note:
• some, but not all, questions about unification or finding a principal type specifically ask you to
show all the steps used in applying an algorithm discussed in lectures. For other questions, simply
show clearly how you obtained your answers.
• the allocation of marks to questions may be varied
Question 1 (5 marks) Consider the term x (λx. x) y
(a) In this term, identify the free and bound occurrences of x
(b) Give a typing derivation for this term (Hint: you may need to use α-equivalence)
(c) Find a term in the Church-style calculus which corresponds to the Curry-style term x (λx. x) y
and which has the type you found in (b).
Question 2 (10 marks) Find a most general unifier for the set of pairs
E = {(α→ θ, β → δ), (ψ → β, α→ γ → θ)}
. Show all the steps of the unification algorithm shown in lectures and tutorials.
Question 3 (15 marks) Recall that ¬P is the same as P → ⊥. For each formula given:
• Use truth tables to show that it is valid in classical logic.
• Determine whether it is valid in intuitionistic logic. If so, prove it; if not provide a Kripke
model showing that it is not valid.
(a) (P → Q)→ (¬P ∨Q)
(b) (¬P ∨Q)→ (P → Q)
Question 4 (15 marks) (a) For the following proposition in intuitionistic logic, find a proof for it.
(D → (A→ C)→ A)→ (A→ C)→ D → C
(b) Thence, using the Curry-Howard correspondence, find a λ-calculus term which has the type
(δ → (α→ γ)→ α)→ (α→ γ)→ δ → γ
and a typing derivation for it, which correspond to the proof you gave in part (a).
1
Question 5 (15 marks)
(a) For the following typed term, give a typing derivation for it:
λu. λv. v (λy. u y (λx. v (λz. x))) : (α→ (β → γ)→ β)→ ((α→ β)→ γ)→ γ
(b) Write out the term in Church-style, ie, including the type of each λ-bound variable.
(c) Use the Curry-Howard correspondence to produce a corresponding proof, in intuitionistic
logic, of the formula
(A→ (B → C)→ B)→ ((A→ B)→ C)→ C
Question 6 (15 marks) We had an example in lectures of M −→β N , where N is typeable but M is
not. In that example, the explanation was that M is an abstraction which ignored its argument,
and N is an untypeable argument. Here is an example with a different explanation of how this can
happen.
(a) Show that (λx. x x) (λy. y) is not typeable. (Show specifically where the Principal Type
algorithm gives failure).
(b) Find its β-normal form.
(c) Using the Principal Type algorithm, show that its β-normal form is typeable. Show all steps
of the Principal Type algorithm.
(d) Write out the term in Church form.
(e) Can you explain how β-reduction changes an untypeable term to a typeable one in this case?
Question 7 (15 marks) (a) Show that (¬P → P ) → P holds in classical logic. Does it hold in
intuitionistic logic? Prove or disprove it.
(b) Now consider (¬¬P → ¬P ) → ¬P Prove this in intuitionistic logic. (Hint: you could first
prove (P → ¬P )→ ¬P , also prove P → ¬¬P , and combine these proofs).
By replacing ⊥ by Q, your proof can similarly be used to prove
(((P → Q)→ Q)→ (P → Q))→ (P → Q)
Thence, using the Curry-Howard isomorphism, find a term of type
(((α→ β)→ β)→ (α→ β))→ (α→ β)
and show that it has this type.
(c) The principal type of this term may be a type more general than
(((α→ β)→ β)→ (α→ β))→ (α→ β)
Look through the typing deduction to see if some but not all of the occurrences of α can be
changed to a different type variable, and likewise for the occurrences of β.
Question 8 (10 marks) As discussed in lectures, the term λx. x can be given any of the following
types: α→ α or (for example) (α→ β)→ α→ β or (β → β)→ β → β (etc)
Can you find terms whose principal type is
(a) (α→ β)→ α→ β (Hint: consider how η-reduction changes the principal type of a term)
(b) (β → β)→ β → β (Hint: consider Church numerals)
2