bug fix 1 (Mon 1:27pm):
Figure 1 now includes the appropriate rules for the
operational semantics for regular expressions.
clarification (Mon 1:27pm) on problem 2b: Prove that if
(R,s,nil) evaluates to b, then (b = true iff s is in R[R])
bug fix 2 (Tue 2:33pm):
In question 2e, that should've read: "Your function should have
the property that if (R,s,nil) evaluates to b, then the ML
expression match R s (fun [] => true | fn _ => false) should
evaluate to b. (I had "reg" instead of "match").
bug fix 3 (Tue 2:33pm):
Questions 3a and 3b were not stated properly. They should've read:
(a) If |- e : int, e = E[i], and E[I] -> e', then |- e' : int.
(b) If |- e : int, then either e = i or else there exists an E, I, and e'
such that e = E[I] and E[I] -> e'.
bug fix 4 (Wed 3:29pm):
Figure 2. We need a technical side condition that the variable
used to plug the whole in the continuation is "fresh" (i.e., does
not occur elsewhere in the context.)