CSE526: Principles of Programming Languages
			      Scott Stoller
	     hw2: denotational semantics in ocaml, part 2
			version: 1am,16feb2004
			   due: 19 feb 2004

1. Write an alternative implementation of state.mli, in which a state is
represented as a list of records with fields "var" and "value".  A
record { var=v; value=i } represents a binding of variable v to integer
i.  The list should not contain multiple records for the same variable;
thus, if the list contains a record for variable v, and the value of v
is updated, the old record for v should be removed from the list.  Do
not use mutable records in your solution to this problem.  Write a few
test cases to check that state.ml is working correctly.

note: typically one would use a pair of type string*int instead of a
record in this data structure, but the goal here is for you to practice
using records in ocaml.

2. Modify your solution to problem 1 so that it uses records with a
mutable "value" field.  Thus, if the list contains a record for
variable v, and the value of v is updated, the value field of that
record should be updated.

3. Using the direct denotational semantics in Sections 2.2-2.4, prove
that the equation above equation (2.2) on [Reynolds, p. 28] holds, i.e.,

  [[while b do c]] sigma = [[if b then (c; while b do c) else skip]] sigma

In other words, when we have defined the meaning of "while" loops using
equation (2.4) on [Reynolds, p. 36], we should be able to prove that
the above equation holds, as a way of checking that equation (2.4) has
the desired meaning.

Hint: First expand the meaning of the right side of (2.2) using the
semantic equations for "if..then", ";", and "while"; this produces an
equation of the form

  [[ if b then (c; while b do c) else skip ]] sigma = PHI1

where formula PHI1 contains Y F  (actually, that Y should have
a subscript "Sigma -> Sigma_bot").

Second, expand the meaning of the left side of (2.2) using the semantics 
equation for "while".  Then re-write that equation using the fact that
(by definition of fixed-point) Y F sigma = F (Y F) sigma.  Try to
make the result look like PHI1.