For each of the following simply-typed applied lambda calculus expressions, give a typing derivation or show that the expression is ill-typed by showing that there can't exist a typing derivation for it.

a) if (if true then false else true) then false else true

b) (x: num). x + x * 3

c) (a: bool). if a then 1 else a

d) ((f: num -> bool) (a: num). if f a then a + 1 else a + 2) ((x: num). false)

HINT:

Please, TYPE the answer CLEARLY with some explanation if possible.

All typing rules (so far) T-Boo1 T-Num T-Var n : num el : num Fe, : num T-Plus T-Times (e1 + e2) : num 2 T-If (if e1 then e2 else e3) : t T-Lam T-App r - (e, e2 All typing rules (so far) T-Boo1 T-Num T-Var n : num el : num Fe, : num T-Plus T-Times (e1 + e2) : num 2 T-If (if e1 then e2 else e3) : t T-Lam T-App r - (e, e2