Observational equivalence for Godel's T and System F
====================================================
* Read / internalize chapter 49 of Harper.
* Write out the full proof of theorem 49.10, Reflexivity of Logical
Equivalence. (Try to do this without peeking at Harper's proof.)
* Prove rule 49.9 in section 49.4.2.
* Read chapter 51 of Harper.
* Extend the development in chapter 51 of Harper to include a product type
constructor with pairing and projection term constructors. Write out the
new cases for all [and only!] the interesting proofs. Use your own
judgement about what counts as interesting.
* Prove the following:
THEOREM: Let
e : All t. t->t->t
be an arbitrary term of the type of Church booleans. Then either
e =~ tru
or
e =~ fls
where =~ is observational equivalence and tru and fls are the Church
booleans (tru = /\t. \x:t. y:t. x and fls = /\t. \x:t. y:t. y).