1. Show the derivation tree for obtaining the value of the expression
(\x -> (\x -> x)) 1 2
with both call-by-value and call-by-name strategies.
2. Let expressions, also known as local definitions, are expressions of form
let x = d in e
where x is a variable and d and e are expressions. For example,
let x = 5 in x + 6 * x
computes to 35. Write the typing and operational semantic rules for let expressions.
3. Consider the polymorphic functions
id : a -> a
flip : (a -> b -> c) -> b -> a -> c
Show the most general types of
id id
id id id
flip flip
flip id
4. Recall the Church booleans:
True = \x -> \y -> x
False = \x -> \y -> y
and = \x -> \y -> x y x
or = \x -> \y -> x x y
Show that the representation is equivalent to the ordinary booleans by
computing the truth tables of and and or.
5. The SKI combinator system consists of three functions:
S = \x -> \y -> \z -> x z (y z)
K = \x -> \y -> x
I = \x -> x
This system is equivalent to lambda calculus, in the sense that any closed lambda expression without constants can be written by using only applications of these 3 functions - without any abstractions or variables. Show how to do this for the Church numerals 0, 1 and 2, that is, for
0 = \f -> \n -> n
1 = \f -> \n -> f n
2 = \f -> \n -> f (f n)