Description

Paul Vrbik
Lambda Calculus
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)
Question 1. [1mark]
Give the λ-expression for NOT that takes True to False and vice-versa. Your solution should be in its β-normal form.
Question 2. [5marks]
Recall that ¬(p ∧ q) ≡¬p ∨¬q and thereby Or is redundant because
p ∨ q ≡¬(¬p ∧¬q).
Give the λ-expression for ¬(¬p ∧¬q) and show it is equivalent to Or.
Question 3. [4marks]
Reduce the following lambda expression to its β-normal form.
(λxy.x)(λabc.cab)z(λz.zz).
Principal Types
There is no partial credit for this section. You are not allowed to use undefined.
The answers for these questions can be checked automatically by Haskell so this “written” work will be submitted to the autograder via the PrincipalType.hs file.
The questions are given in ascending difficulty.
Question 4. [2marks]
Define a function f1 such that
> :type f1 f1 :: (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. [2marks]
Same instructions as Question 4 but with
f2 :: a -> (b, c) -> b
Question 6. [2marks]
Same instructions as Question 4 but with
f3 :: (a -> a) -> a -> [a]
Note. There are several ways to implement this function but we want most general one that produces the most meaningful result. Trivial implementations like f3 _ _ = [] will not be accepted since they are not general and do not produce anything meaningful.
Question 7. [2marks]
Same instructions as Question 4 but with
f4 :: (b -> r) -> (a -> b) -> (a -> r)
Question 8. [1mark]
Same instructions as Question 4 but with
f5 :: ((a, b, c) -> d) -> a -> b -> c -> d
Question 9. [1mark]
Same instructions as Question 4 but with
f5_inv :: (a -> b -> c -> d) -> (a, b, c) -> d
Principal Types: Extra
This is not part of the assignment, but rather some context which makes the previous page of questions more meaningful.
Question 4
Curry–Howard isomorphism or equivalence is the direct relationship between computer programs and mathematical proofs. It states that if there is a total program with a specific type, then the logical statement corresponding to that type is true. The function
f1 :: (a -> b, a) -> b
represents Modus Ponens. It states that
“If the statement ’A implies B’ is true and statement A is true, then statement B is also true.”
In the function type, a -> b corresponds to the statement A ⇒ B (A implies B) and a corresponds to statement A.
By implementing this function, you will prove Modus Ponens.
Question 8 and Question 9
These functions are another example of Curry-Howard isomorphism. By implementing them you will prove the powers law:
((da)b)c = dabc.
If there are m elements in the set A and n elements in the set B, then the number of functions from A to B (with type A → B) is nm. f5 receives a function of type
((a, b, c) -> d)
and returns a function
(a -> b -> c -> d)
The number of functions of type (a, b, c) -> d is dabc and the number of functions of type a -> b -> c -> d is ((da)b)c.

Blockus
There is a game called Blockus where players try and fill a grid of squares with Tetris-like pieces. One such piece is called “V3” and looks like. . .

If we remove a corner square from a 16 × 16 board we can cover what remains with V3 pieces.

Question 10. [10marks]
Most of the programs we write in Haskell will be recursive or inductive in nature. The purpose of this question is to help us get into the mindset of reasoning inductively.
Use the principle of mathematical induction to prove a 2n ×2n Blockus board with northwest corner removed can be covered with V3 pieces.
Note: This question will be marked very thoroughly. 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 or for making unsubstantiated claims. Every statement you write should be clearly inferred from the statements that precede it (not statements that come after).
Essentially we are looking for clear and concise proofs.
5