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.