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.
Define ! in ISWIM using Yv.
Prove |- ! '3' =v '6' using the fixpoint theorem for Yv.
Due: Wed 23-1-2002. Brief class discussion.
Develop a module for finite functions. The module should support the
module type FF =
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
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.
- 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