COMP3400
Assignment 1 Written
Paul Vrbik
March 11, 2022
Lambda Calculus
Question 1. [2 marks]
We can encode boolean logic in lambda calculus as follows:
True = λx.(λy.x) False = λx.(λy.y)
And = λp.(λq.(pq)p) Or = λp.(λq.(pp)q)
Give the λ-expression for NOT that takes True to False and vice-versa. Your solution
should be in its β-normal form.
Question 2. [5 marks]
We can encode boolean logic in lambda calculus as follows:
True = λx.(λy.x) False = λx.(λy.y)
And = λp.(λq.(pq)p) Or = λp.(λq.(pp)q)
The implies operator =⇒ has the following definition:
p =⇒ q ≡ ¬p ∨ q
Give a λ-expression for encoding Imp (implies) and reduce it to its β-normal form.
Question 3. [3 marks]
Prove that
Imp False
is a tautology (i.e. a function that maps everything to True).
1
Principal Types
There is no partial credit for this section. You are not allowed to use undefined.
Question 4. [2 marks]
Define a function q1 such that
> :type q0
q0 :: (a -> [b]) -> [a] -> [b]
up to renaming of the type variables. Your function does not have to be total but
should not be undefined.
Question 5. [2 marks]
Same instructions as Question 4 but with
q1 :: (a, b) -> (c, d) -> ((b, d), (a, c))
Question 6. [2 marks]
Same instructions as Question 4.
q2 :: (a -> b) -> ((a -> c) -> c) -> ((b -> c) -> c)
Question 7. [2 marks]
Same instructions as Question 4 but with
q3 :: (a -> b -> c) -> (a -> b) -> a -> c
Question 8. [2 marks]
Same instructions as Question 4 but with
q4 :: ((a -> b -> c) -> a) -> (a -> c) -> c
2
Induction
Question 9. [10 marks]
Equilateral triangles can be tiled with smaller triangles in the following way:
T0 T1 T2 T3
and so on.
Note each triangle (asides T0) is comprised of four copies of the previous triangle.
Prove Tn can be covered with the following tile so that only the top triangle is left uncovered.
For example, for T1 and T2 can be covered in the following way
Note: This question will be marked very strictly. We will be looking for the presence
of all necessary components of induction to be stated clearly. You will be marked
down for being unnecessarily verbose. Every statement you write should be clearly
inferred from the statements that precede it (not statements that come after).