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.