Reference no: EM13585149

1) β -reduction

(a) Underline the free variables in the term: (λy x. x y) (a. a x )

(b) β-reduce that term to its normal form.

2) Simply Typed -Calculus

(a) Write down the (most general) type of the following term: (λx. x ) (λy. y)

(b) Give a pen-and-paper proof of your answer to (a).

(c) For the term (λx. x ) (λy: y), write down the type of the following sub-term: (λx. x ) — that is, the type that the sub-term has within the larger term.