COMP3400 Assignment 1 Written
Paul Vrbik March 5, 2023
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. [1 mark]
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]
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. [4 marks]
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. [2 marks] Define a function f1 such that
> :type f1
f1 :: (a -> b, a) -> b
up to renaming of the type variables. Your function should be total and not be unde- fined.
Question 5. [2 marks] Same instructions as Question
f2 :: a -> (b, c) -> b
Question 6. [2 marks] Same instructions as Question
f3 :: (a -> a) -> a -> [a]
4 but with
4 but with
Note. There are several ways to implement this function but we want most gen- eral 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. [2 marks]
Same instructions as Question 4 but with
f4 :: (b -> r) -> (a -> b) -> (a -> r)
Question 8. [1 mark]
Same instructions as Question 4 but with
f5 :: ((a, b, c) -> d) -> a -> b -> c -> d
Question 9. [1 mark]
Same instructions as Question 4 but with
f5_inv:: (a->b->c->d)->(a,b,c)->d
Programming Help, Add QQ: 749389476
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 state-
ment 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 implement-
ing 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 oftypea -> b -> c -> dis((da)b)c.
Computer Science Tutoring
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. [10 marks]
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 north-
west 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.
程序代写 CS代考 加微信: cstutorcs