Homework 3

1. Show how to formulate the evaluation rules for \(\lambda\)-terms in big-step style. (Pierce 5.3.8)
2. The \(\lambda_\rightarrow\) with no base types is degenerate, in the sense that it has no well-typed terms at all. Why? (Pierce 9.2.1)
3. Is there any context \(\Gamma\) of type \(T\) such that \(\Gamma\vdash x\ x:T\)? If so, provide \(\Gamma\) and \(T\) and show the typing derivation. If not, prove it. (Pierce 9.2.2, tricky)
4. Do \(t\rightarrow t'\) and \(\Gamma\vdash t':T\) imply \(\Gamma\vdash t:T\)? (Pierce 9.3.10)
5. Give typing and evaluation rules for wildcard abstractions and prove they can be derived from the derived form from class.