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)