Assignments

Assignment 1: Exercises 1.15, 1.16, 1.17, and 1.18 of EoPL (pp.24-27) Please keep track of your type errors.
Due: Wed 23-1-2002. Brief class discussion of select exercises.
Assignment 2: Define ! in ISWIM using Yv. Prove |- ! '3' =v '6' using the fixpoint theorem for Yv.
Due: Wed 23-1-2002. Brief class discussion.
Assignment 3: Develop a module for finite functions. The module should support the following signature:
```
   module type FF = 
     sig
       type ('a,'b) F_F
       val empty : ('a,'b) F_F
       val extend : ('a,'b) F_F * 'a * 'b -> ('a,'b) F_F
       val apply :  ('a,'b) F_F * 'a -> 'b
       val domain : ('a,'b) F_F -> 'a list
     end;; 
```
Explain why you can't use plain functions to represent finite functions. Use functions from 'a to 'b to represent the functional aspect of the type F_F anyway.
Also see my Scheme implementation.
Due: Mon 4-2-2002. Brief class discussion.
Assignment 4:
- Prove that fix! computes a fixpoint of functionals.
- Write a diverging program using SML's STLC core and exceptions. Explain why it is impossible to write this program in OCAML.
- Exhibit (or find) two CR rewriting systems on the same term set such that the combined systems are not CR.
- Design an extension of STLC with higher-order ref cells such that the language is SN. (No proof necessary.) Discuss whether it is a useful language.