Jim's
Tutorials

Chapter 29: Exceptions

29.1

The theorem is imprecisely stated; the ok judgment is never defined for XPCF. However, a natural definition would be to first extend the K machine’s ~> judgment to raise and try frames in the obvious way and then extend its ok judgment by a rule

k ◁: τ    e : τ_exn    e val
----------------------------
          k ◀ e ok 

Note that the τ in k ◁: τ does not occur in the conclusion; we only care that it holds for some τ—i.e., that k is well-typed.

1. All of the rules inherited from the original K machine can be proven safe in the same way as before. This leaves rules (29.5) to be accounted for.
   1. This follows immediately from inversion on the premise that the old state is ok (and subsequent inversion on the resulting typing judgments), followed by application of ~>’s extension to raise frames.
   2. Inversion on ok, plus the extension of ok to ◀ states.
   3. Inversion on ok, plus the extension of ~> to try frames.
   4. Ditto.
   5. Ditto, plus the substitution property of typing.
   6. Inversion on ok, plus the extension of ok to ◀ states.

2. We first consider states k ▷ e. As for the K machine, such a state can always take a step using the unique rule applicable to e’s form. We next consider states k ◁ e. If k does not end in a raise or try frame, then the same arguments used in progress for K apply, and if it does end in one of these, then one of rules (29.5b) and (29.5d) applies. We lastly consider states k ◀ e. If k is empty, then this is a final state. If k ends in a non-try frame, then rule (29.5f) applies. Finally, if k ends in a try frame, then rule (29.5c) applies.

These proofs do not rely on any properties of τ_exn.

29.2

We can extend an evaluation dynamics for ordinary PCF with some more rules. We start with the basic rules for raise and try:

    e ⇓ v
------------
raise(e) ⇑ v

      e_1 ⇓ v_1
---------------------
try(e_1; x.e_2) ⇓ v_1

e_1 ⇑ v_1    [v_1/x]e_2 ⇓ v_2
-----------------------------
    try(e_1; x.e_2) ⇓ v_2

We must then add rules for propagating exceptions upward when subexpressions produce them. For each rule other than the second one above, we need to add propagation rules corresponding to each ⇓ premise. The second rule above is excluded because it is precisely the case when an exception shouldn’t propagate upward. Here are a few example propagation rules; the rest are very similar.

For the rule

e_1 ⇓ lam{τ_2}(x.e)    [e_2/x]e ⇓ v
-----------------------------------
        ap(e_1; e_2) ⇓ v

we must add two propagation rules:

     e_1 ⇑ v_1
------------------
ap(e_1; e_2) ⇑ v_1

e_1 ⇓ lam{τ_2}(x.e)    [e_2/x]e ⇑ v
-----------------------------------
        ap(e_1; e_2) ⇑ v

For the rule

   e ⇓ v
-----------
s(e) ⇓ s(v)

we must add one propagation rule:

 e ⇑ v
--------
s(e) ⇑ v

29.3

TODO

Chapter 30: Continuations

30.1

TODO

30.2

TODO

30.3

TODO