User:Rsimmons/Handled exceptions

This is Literate Twelf Code: here Status: %% OK %% Output: here.

Syntax

Types

ty : type.
ty/nat : ty.               % nat
ty/arrow : ty -> ty -> ty. % tau1 tau2
ty/mayraise : ty -> ty.    % [*] tau

We have to pick some type associated with exceptions. Here, we'll just use nat.

ty/exn = ty/nat.

Type equality

eqty : ty -> ty -> type.
eqty/refl : eqty T T.

Terms

tm : type.
tm/lam : ty -> (tm -> tm) -> tm.
tm/app : tm -> tm -> tm.
tm/z : tm.
tm/s : tm -> tm.
tm/if : tm -> tm -> (tm -> tm) -> tm.
tm/fix : ty -> (tm -> tm) -> tm.
tm/raise : tm -> tm.
tm/handle : tm -> (tm -> tm) -> tm.
tm/susp : tm -> tm.
tm/unsusp : tm -> tm.
tm/let : tm -> ty -> (tm -> tm) -> tm = [e][t][f] tm/app (tm/lam t f) e.

Static semantics

of : tm -> ty -> type.   % Will not throw exceptions
of* : tm -> ty -> type.  % May or may not throw exceptions

of*/weaken : of E T -> of* E T.

of/lam : ({x} of x T -> of (E x) T') -> of (tm/lam T E) (ty/arrow T T').
of/app : of E1 (ty/arrow T T') -> of E2 T -> of (tm/app E1 E2) T'.
of/z : of tm/z ty/nat.
of/s : of E ty/nat -> of (tm/s E) ty/nat.
of/if : of E ty/nat -> of E1 T -> ({x} of x ty/nat -> of (E2 x) T) 
 -> of (tm/if E E1 ([x] E2 x)) T. 
of/fix : ({x} of x T -> of (E x) T) -> of (tm/fix T ([x] E x)) T.
of/handle : of* E T -> ({x} of x ty/exn -> of (E' x) T) 
 -> of (tm/handle E ([x] E' x)) T.
of/susp : of* E T -> of (tm/susp E) (ty/mayraise T).

of*/app : of* E1 (ty/arrow T T') -> of* E2 T -> of* (tm/app E1 E2) T'.
of*/s : of* E ty/nat -> of* (tm/s E) ty/nat.
of*/if : of* E ty/nat -> of* E1 T -> ({x} of x ty/nat -> of* (E2 x) T) 
 -> of* (tm/if E E1 ([x] E2 x)) T. 
of*/raise : of* E ty/exn -> of* (tm/raise E) T.
of*/handle : of* E T -> ({x} of x ty/exn -> of* (E' x) T) 
 -> of* (tm/handle E ([x] E' x)) T.
of*/unsusp : of* E (ty/mayraise T) -> of* (tm/unsusp E) T.

Dynamic semantics

Values

v : tm -> type.
v/lam : v (tm/lam T ([x] E x)).
v/z : v tm/z.
v/s : v E -> v (tm/s E).
v/susp : v (tm/susp E).

Small-step evaluation

step : tm -> tm -> type.
step/app1   : step E1 E1' -> step (tm/app E1 E2) (tm/app E1' E2).
step/app1x  : v E -> step (tm/app (tm/raise E) _) (tm/raise E).
step/app2   : v E1 -> step E2 E2' -> step (tm/app E1 E2) (tm/app E1 E2').
step/app2x  : v E -> v E1 -> step (tm/app E1 (tm/raise E)) (tm/raise E).
step/appr   : v E2 -> step (tm/app (tm/lam T ([x] E x)) E2) (E E2).
step/s      : step E E' -> step (tm/s E) (tm/s E').
step/sx     : v E -> step (tm/s (tm/raise E)) (tm/raise E).
step/if     : step E E' -> step (tm/if E E1 ([x] E2 x))(tm/if E' E1 ([x] E2 x)).
step/ifz    : step (tm/if tm/z E1 ([x] E2 x)) E1.
step/ifs    : v E -> step (tm/if (tm/s E) E1 ([x] E2 x)) (E2 E). 
step/ifx    : v E -> step (tm/if (tm/raise E) E1 ([x] E2 x)) (tm/raise E).
step/fix    : step (tm/fix T ([x] E x)) (E (tm/fix T ([x] E x))).
step/raise  : step E E' -> step (tm/raise E) (tm/raise E').
step/raisex : v E -> step (tm/raise (tm/raise E)) (tm/raise E).
step/handle : step E1 E1' -> step (tm/handle E1 ([x] E2 x)) (tm/handle E1' E2).
step/handler: v E -> step (tm/handle E _) E.
step/handlex: v E -> step (tm/handle (tm/raise E) ([x] E2 x)) (E2 E).
step/unsusp : step E E' -> step (tm/unsusp E) (tm/unsusp E').
step/unsuspr: step (tm/unsusp (tm/susp E)) E.
step/unsuspx: v E -> step (tm/unsusp (tm/raise E)) (tm/raise E).

Progress

Not stuck

nstuck : tm -> type.
nstuck/step  : step E E' -> nstuck E.
nstuck/value : v E -> nstuck E.

nstuck* : tm -> type.
nstuck*/step  : step E E' -> nstuck* E.
nstuck*/value : v E -> nstuck* E.
nstuck*/raise : v E -> nstuck* (tm/raise E).

ns-weaken : nstuck E -> nstuck* E -> type.
- : ns-weaken (nstuck/step E) (nstuck*/step E).
- : ns-weaken (nstuck/value V) (nstuck*/value V).
%mode ns-weaken +A -B. %worlds () (ns-weaken _ _). %total {} (ns-weaken _ _).

Mobile value

This theorem really isn't as interesting as its name makes it sound, though it is necessary in one place. Otherwise, all of the little factoring lemmas are only case analysis, not induction.

mobile : v E -> of* E T -> of E T -> type.
- : mobile v/lam (of*/weaken (of/lam F)) (of/lam F).
- : mobile v/z (of*/weaken of/z) of/z.
- : mobile (v/s V) (of*/weaken (of/s S)) (of/s S).
- : mobile (v/s V) (of*/s S) (of/s S') <- mobile V S S'.
- : mobile v/susp (of*/weaken (of/susp T)) (of/susp T).
%mode mobile +A +B -C. %worlds () (mobile _ _ _). %total T (mobile T _ _).

Progress

progress : of E T -> nstuck E -> type.
progress* : of* E T -> nstuck* E -> type.
%mode progress +A -B.
%mode progress* +A -B.

- : progress* (of*/weaken T) NS* <- progress T NS <- ns-weaken NS NS*.

- : progress (of/lam _) (nstuck/value v/lam).
p0 : of E (ty/arrow T1 T2)
      -> nstuck E -> nstuck E' -> nstuck (tm/app E E') -> type.
- : p0 _ (nstuck/step E) _ (nstuck/step (step/app1 E)).
- : p0 _ (nstuck/value V) (nstuck/step E) (nstuck/step (step/app2 V E)).
- : p0 (of/lam _) (nstuck/value _) (nstuck/value V) (nstuck/step (step/appr V)).
%mode p0 +A +B +C -D. %worlds () (p0 _ _ _ _). %total {} (p0 _ _ _ _).
- : progress (of/app T1 T2) NS 
     <- progress T1 NS1 <- progress T2 NS2 <- p0 T1 NS1 NS2 NS.
- : progress of/z (nstuck/value v/z).
p1 : of E ty/nat -> nstuck E -> nstuck (tm/s E) -> type.
- : p1 _ (nstuck/step E) (nstuck/step (step/s E)).
- : p1 _ (nstuck/value V) (nstuck/value (v/s V)).
%mode p1 +A +B -C. %worlds () (p1 _ _ _). %total {} (p1 _ _ _). 
- : progress (of/s T) NS <- progress T NS1 <- p1 T NS1 NS.
p2 : {E1}{E2} of E ty/nat -> nstuck E -> nstuck (tm/if E E1 ([x] E2 x)) -> type.
- : p2 _ _ _ (nstuck/step E) (nstuck/step (step/if E)).
- : p2 _ _ _ (nstuck/value v/z) (nstuck/step step/ifz).
- : p2 _ _ _ (nstuck/value (v/s V)) (nstuck/step (step/ifs V)).
%mode p2 +E +F +A +B -C. %worlds () (p2 _ _ _ _ _). %total {} (p2 _ _ _ _ _).
- : progress (of/if T T1 T2) NS <- progress T NS1 <- p2 _ _ T NS1 NS.
- : progress (of/fix T) (nstuck/step step/fix).
p3 : {E'} of* E T -> nstuck* E -> nstuck (tm/handle E E') -> type.
- : p3 _ _ (nstuck*/step E) (nstuck/step (step/handle E)).
- : p3 _ _ (nstuck*/value V) (nstuck/step (step/handler V)).
- : p3 _ _ (nstuck*/raise V) (nstuck/step (step/handlex V)).
%mode p3 +A +B +C -D. %worlds () (p3 _ _ _ _). %total {} (p3 _ _ _ _).
- : progress (of/handle T T2) NS <- progress* T NS1 <- p3 _ T NS1 NS.
- : progress (of/susp _) (nstuck/value v/susp).

p9 : of* E (ty/arrow T1 T2)
      -> nstuck* E -> nstuck* E' -> nstuck* (tm/app E E') -> type.
- : p9 _ (nstuck*/step E) _ (nstuck*/step (step/app1 E)).
- : p9 _ (nstuck*/raise V) _ (nstuck*/step (step/app1x V)).
- : p9 _ (nstuck*/value V) (nstuck*/step E) (nstuck*/step (step/app2 V E)).
- : p9 _ (nstuck*/value V') (nstuck*/raise V) (nstuck*/step (step/app2x V V')).
- : p9 (of*/weaken T) (nstuck*/value V1) (nstuck*/value V2) NS*
     <- p0 T (nstuck/value V1) (nstuck/value V2) NS <- ns-weaken NS NS*.
%mode p9 +A +B +C -D. %worlds () (p9 _ _ _ _). %total {} (p9 _ _ _ _).
- : progress* (of*/app T1 T2) NS 
     <- progress* T1 NS1 <- progress* T2 NS2 <- p9 T1 NS1 NS2 NS.
p5 : of* E ty/nat -> nstuck* E -> nstuck* (tm/s E) -> type.
- : p5 _ (nstuck*/step E) (nstuck*/step (step/s E)).
- : p5 _ (nstuck*/value V) (nstuck*/value (v/s V)).
- : p5 _ (nstuck*/raise V) (nstuck*/step (step/sx V)).
%mode p5 +A +B -C. %worlds () (p5 _ _ _). %total {} (p5 _ _ _).
- : progress* (of*/s T) NS <- progress* T NS1 <- p5 T NS1 NS.
p6 : {E1}{E2} of* E ty/nat -> nstuck* E -> nstuck* (tm/if E E1 E2) -> type.
- : p6 _ _ _ (nstuck*/step E) (nstuck*/step (step/if E)).
- : p6 _ _ T* (nstuck*/value V) NS*
     <- mobile V T* T <- p2 _ _ T (nstuck/value V) NS <- ns-weaken NS NS*.
- : p6 _ _ _ (nstuck*/raise V) (nstuck*/step (step/ifx V)).
%mode p6 +A +B +C +D -E. %worlds () (p6 _ _ _ _ _). %total {} (p6 _ _ _ _ _).
- : progress* (of*/if T T1 T2) NS <- progress* T NS1 <- p6 _ _ T NS1 NS.
pA : nstuck* E -> nstuck* (tm/raise E) -> type.
- : pA (nstuck*/step E) (nstuck*/step (step/raise E)).
- : pA (nstuck*/value V) (nstuck*/raise V).
- : pA (nstuck*/raise V) (nstuck*/step (step/raisex V)).
%mode pA +A -B. %worlds () (pA _ _). %total {} (pA _ _).
- : progress* (of*/raise T) NS <- progress* T NS1 <- pA NS1 NS.
- : progress* (of*/handle T T2) NS 
     <- progress* T NS1 <- p3 _ T NS1 NS* <- ns-weaken NS* NS.
p7 : v E -> of E (ty/mayraise T) -> step (tm/unsusp E) E' -> type.
- : p7 _ _ step/unsuspr.
%mode p7 +A +B -C. %worlds () (p7 _ _ _). %total {} (p7 _ _ _).
p8 : of* E (ty/mayraise T) -> nstuck* E -> nstuck* (tm/unsusp E) -> type.
- : p8 _ (nstuck*/step E) (nstuck*/step (step/unsusp E)).
- : p8 (of*/weaken T) (nstuck*/value V) (nstuck*/step E) <- p7 V T E.
- : p8 _ (nstuck*/raise V) (nstuck*/step (step/unsuspx V)).
%mode p8 +A +B -C. %worlds () (p8 _ _ _). %total {} (p8 _ _ _).
- : progress* (of*/unsusp T) NS <- progress* T NS1 <- p8 T NS1 NS.

%worlds () (progress _ _) (progress* _ _). 
%total (T T*) (progress T _) (progress* T* _).

Preservation

Inversion

inv-lam : of* (tm/lam T' E) T
           -> ({x} of x T' -> of (E x) T'') -> eqty T (ty/arrow T' T'') -> type.
- : inv-lam (of*/weaken (of/lam F)) F eqty/refl.
%mode inv-lam +A -B -C. %worlds () (inv-lam _ _ _). %total {} (inv-lam _ _ _).

inv-app : of* (tm/app E1 E2) T -> of* E1 (ty/arrow T' T) -> of* E2 T' -> type.
- : inv-app (of*/app T1 T2) T1 T2.
- : inv-app (of*/weaken (of/app T1 T2)) (of*/weaken T1) (of*/weaken T2).
%mode inv-app +A -B -C. %worlds () (inv-app _ _ _). %total {} (inv-app _ _ _).

inv-s : of* (tm/s E) T -> of* E ty/nat -> eqty T ty/nat -> type.
- : inv-s (of*/s T) T eqty/refl.
- : inv-s (of*/weaken (of/s T)) (of*/weaken T) eqty/refl.
%mode inv-s +A -B -C. %worlds () (inv-s _ _ _). %total {} (inv-s _ _ _).

inv-if : of* (tm/if E E1 E2) T 
   -> of* E ty/nat -> of* E1 T -> ({x} of x ty/nat -> of* (E2 x) T) -> type.
- : inv-if (of*/if T T1 T2) T T1 T2.
- : inv-if (of*/weaken (of/if T T1 T2)) 
     (of*/weaken T) (of*/weaken T1) ([x][d] of*/weaken (T2 x d)).
%mode inv-if +A -B -C -D. %worlds () (inv-if _ _ _ _). 
%total {} (inv-if _ _ _ _).

inv-raise : of* (tm/raise E) T -> of* E ty/exn -> type.
- : inv-raise (of*/raise T) T.
%mode inv-raise +A -B. %worlds () (inv-raise _ _). %total {} (inv-raise _ _).

inv-handle : of* (tm/handle E ([x] H x)) T 
              -> of* E T -> ({x} of x ty/exn -> of* (H x) T) -> type.
- : inv-handle (of*/handle T H) T H.
- : inv-handle (of*/weaken (of/handle T H)) T
     ([x][d] (of*/weaken (H x d))).
%mode inv-handle +A -B -C. %worlds () (inv-handle _ _ _). 
%total {} (inv-handle _ _ _).

inv-susp : of* (tm/susp E) T -> of* E T' -> eqty T (ty/mayraise T') -> type.
- : inv-susp (of*/weaken (of/susp T)) T eqty/refl.
%mode inv-susp +A -B -C. %worlds () (inv-susp _ _ _). 
%total {} (inv-susp _ _ _).

inv-unsusp : of* (tm/unsusp E) T -> of* E (ty/mayraise T) -> type.
- : inv-unsusp (of*/unsusp T) T.
%mode inv-unsusp +A -B. %worlds () (inv-unsusp _ _). %total {} (inv-unsusp _ _).

Preservation

preservation: step E E' -> of E T -> of E' T -> type.
preservation*: step E E' -> of* E T -> of* E' T -> type.
%mode preservation +A +B -C.
%mode preservation* +A +B -C.

Application

- : preservation (step/app1 E) (of/app T1 T2) (of/app T1' T2)
     <- preservation E T1 T1'.
- : preservation (step/app2 V E) (of/app T1 T2) (of/app T1 T2')
     <- preservation E T2 T2'.
- : preservation (step/appr V) (of/app (of/lam Tf) (T2 : of E T)) (Tf E T2).

- : preservation* (step/app1 E) T (of*/app T1' T2)
     <- inv-app T T1 T2 <- preservation* E T1 T1'.
- : preservation* (step/app1x V) T (of*/raise Texn)
     <- inv-app T T1 T2 <- inv-raise T1 Texn.
- : preservation* (step/app2 V E) T (of*/app T1 T2')
     <- inv-app T T1 T2 <- preservation* E T2 T2'.
- : preservation* (step/app2x V V') T (of*/raise Texn)
     <- inv-app T T1 T2 <- inv-raise T2 Texn.
q2 : eqty (ty/arrow T3 T4) (ty/arrow T1 T5)
      -> ({x} of x T1 -> of (E2 x) T5)
      -> of E6 T3
      -> of (E2 E6) T4 -> type.
- : q2 eqty/refl F E (F _ E).
%mode q2 +A +B +C -D. %worlds () (q2 _ _ _ _). %total {} (q2 _ _ _ _).
- : preservation* (step/appr V) T (of*/weaken Tres)
     <- inv-app T T1 T2* <- mobile V T2* T2 
     <- inv-lam T1 F Eq <- q2 Eq F T2 Tres.

Natural numbers

- : preservation (step/s E) (of/s T) (of/s T') <- preservation E T T'.
- : preservation (step/if E) (of/if T T1 T2) (of/if T' T1 T2)
     <- preservation E T T'.
- : preservation (step/ifz) (of/if of/z T1 _) T1.
- : preservation (step/ifs V) (of/if (of/s T) _ T2) (T2 _ T).

q1 : of* E ty/nat -> eqty T ty/nat -> of* (tm/s E) T -> type.
- : q1 T _ (of*/s T). 
%mode q1 +A +B -C. %worlds () (q1 _ _ _). %total {} (q1 _ _ _).
- : preservation* (step/s E) Ts Ts'
     <- inv-s Ts T Eq <- preservation* E T T' <- q1 T' Eq Ts'.
q3 : of* (tm/raise E) ty/nat -> eqty TN ty/nat -> of* (tm/raise E) TN -> type.
- : q3 T _ T.
%mode q3 +A +B -C. %worlds () (q3 _ _ _). %total {} (q3 _ _ _).
- : preservation* (step/sx V) DTs DT'
   <- inv-s DTs (DT: of* (tm/raise E) ty/nat) (Eq: eqty TN ty/nat)
   <- q3 DT Eq DT'.
- : preservation* (step/if E) Tif (of*/if T' T1 T2)
     <- inv-if Tif T T1 T2 <- preservation* E T T'.
- : preservation* (step/ifz) Tif T1
     <- inv-if Tif (DT: of* tm/z ty/nat) (T1: of* E1 T) _.
- : preservation* (step/ifs (V: v N)) DTif (T2 N Tn)
     <- inv-if DTif Tsn* T1 (T2: {x} of x ty/nat -> of* (E2 x) T)
     <- inv-s Tsn* (Tn* : of* N ty/nat) _
     <- mobile V Tn* Tn.
- : preservation* (step/ifx V) DTif (of*/raise DTexn)
     <- inv-if DTif DT _ _
     <- inv-raise DT DTexn.

Fix/raise/handle

- : preservation (step/fix) (of/fix F) (F _ (of/fix F)).
- : preservation (step/handle E) (of/handle T* T) (of/handle T'* T)
     <- preservation* E T* T'*.
- : preservation (step/handler V) (of/handle T* T) T' <- mobile V T* T'.
- : preservation (step/handlex V) (of/handle (of*/raise Texn*) T) (T _ Texn)
     <- mobile V Texn* Texn.

- : preservation* (step/fix) (of*/weaken T) (of*/weaken T')
     <- preservation step/fix T T'.
- : preservation* (step/raise E) (of*/raise T) (of*/raise T')
     <- preservation* E T T'.
- : preservation* (step/raisex E) (of*/raise T) (of*/raise Texn)
     <- inv-raise T Texn.
- : preservation* (step/handle DE) (DT: of* (tm/handle E H) T) 
     (of*/handle DT1' DT2)
     <- inv-handle DT DT1 DT2 
     <- preservation* DE DT1 DT1'.
- : preservation* (step/handler V) (DT) DT1
     <- inv-handle DT DT1 DT2.
- : preservation* (step/handlex V) (DT: of* (tm/handle (tm/raise E) H) T) 
     (DT2 E DTexn')
     <- inv-handle DT (DT1 : of* (tm/raise E) T) DT2
     <- inv-raise DT1 (DTexn : of* E ty/exn)
     <- mobile V DTexn DTexn'.
- : preservation* (step/unsusp DE) (DT: of* (tm/unsusp E) T) (of*/unsusp DT'')
     <- inv-unsusp DT (DT': of* E (ty/mayraise T))
     <- preservation* DE DT' (DT'': of* E' (ty/mayraise T)).
d4 : eqty (ty/mayraise T) (ty/mayraise T') -> of* E T' -> of* E T -> type.
- : d4 _ T T. %mode d4 +A +B -C. %worlds () (d4 _ _ _). %total {} (d4 _ _ _).
- : preservation* (step/unsuspr) (DT: of* (tm/unsusp (tm/susp E)) T) DT'''
     <- inv-unsusp DT (DT': of* (tm/susp E) (ty/mayraise T))
     <- inv-susp DT' (DT'': of* E T') 
        (Eq: eqty (ty/mayraise T) (ty/mayraise T'))
     <- d4 Eq DT'' DT'''.
- : preservation* (step/unsuspx V) DT (of*/raise DTexn)
     <- inv-unsusp DT (DT' : of* (tm/raise E) (ty/mayraise T))
     <- inv-raise DT' (DTexn : of* E ty/exn).

%worlds () (preservation _ _ _) (preservation* _ _ _).
%total (E E*) (preservation E _ _) (preservation* E* _ _).