Consider the following lambda expression:
(λ (x: Integer) . (x + 1))((λ (y: Integer) . (y + 2)) 4)
Give all possible reductions of this lambda expression to its normal form. Show each step of the reduction in detail (i.e., all the substitutions, etc.)
Does this lambda expression, (λ x. (x x))(λ x. (x x)), have a normal form? Why or why not?
Chapter 9 uses three notations for "type variables": λ (as in λvk on page 142), Λ (as in Λvk as on page 146) and upside-down-A (as on page 145). Explain how they are different giving examples to illustrate your answer.
The text describes and uses two abbreviations (functions that take multiple arguments and let expressions) gives their "expanded forms". The expanded forms for functions taking multiple arguments is given first in the text and uses substitution. Give an expansion of functions with multiple arguments that use let expressions instead of substitution. Argue that the expansion using let expressions and the expansion using substitution are the same.
One of the things that makes lambda calculus (and by extension functional languages) so powerful is that they treat functions as first-class values. In other words, one can compute with functions as if they were ordinary values, such as integer. For example, one can pass functions as arguments or return them as a result. Consider, for example, the problem of writing a "compose" function. This function takes two functions as arguments (e.g., f and g) and returns a new function that is the composition of the two. For example, let's suppose one has functions add1 and mult2, where add1 adds 1 to its argument and mult2 multiplies its argument by 2. Consider:
let t = compose(add1, mult2) in t(5)
The result of the call to compose is a function that will first apply add1 to its argument and then apply mult2 to the result of the call to add1. In the above call (t(5)), we will effectively compute mult2(add1(5)), which evaluates to 12. (i) Write a function "compose" in polymorphic lambda calculus. Your function should not be restricted to composing functions of a fixed (e.g., integer) type: it must be polymorphic. (ii) Give the type of this function.