C machine and focusing

C Machine and Focusing

Syntax

%sort pos %.
%name pos %.
%sort neg %.
%name neg %.
%term down %pi neg %-> pos %.
%term plus %pi pos %-> pos %-> pos %.
%term times %pi pos %-> pos %-> pos %.
%term zero pos %.
%term one pos %.
%term up %pi pos %-> neg %.
%term arr %pi pos %-> neg %-> neg %.
%term with %pi neg %-> neg %-> neg %.
%term top neg %.
%inline conc neg %.
%sort val+ {_ pos} %.
%sort cont- {_ neg} {_ conc} %.
%sort cont+ {_ pos} {_ conc} %.
%sort val- {_ neg} %.
%sort exp {_ conc} %.
%% positive values
%term mt+ val+ one %.
%% no rule for zero
%term pair+ %pi (val+ A) %-> (val+ B) %-> (val+ (times A B)) %.
%term inl %pi (val+ A) %-> (val+ (plus A B)) %.
%term inr %pi (val+ B) %-> (val+ (plus A B)) %.
%term delay- %pi (exp A-) %-> (val+ (down A-)) %.
%% positive continuations (shallow matching)
%% positive conts
%term let1 %pi (exp C) %-> (cont+ one C) %.
%% no rule for zero
%term split %pi (%pi (val+ A) %-> (val+ B) %-> (exp C)) %-> (cont+ (times A B) C) %.
%term case
  %pi (%pi (val+ A) %-> (exp C))
  %-> (%pi (val+ B) %-> (exp C))
  %-> (cont+ (plus A B) C) %.
%term force- %pi (cont- A- C) %-> (cont+ (down A-) C) %.
%% wait to peel off the shift until you're ready to focus.
%% negative continuations
%term app %pi (val+ A+) %-> (cont- B C) %-> (cont- (arr A+ B) C) %.
%term fst %pi (cont- A C) %-> (cont- (with A B) C) %.
%term snd %pi (cont- B C) %-> (cont- (with A B) C) %.
%term force+ %pi (%pi (val+ A+) %-> (exp C)) %-> (cont- (up A+) C) %.
%% internalize identity so we don't need to eta-expand
%term id- cont- A A %.
%% negative values (shallow)
%term lam %pi (%pi (val+ A+) %-> (exp B-)) %-> (val- (arr A+ B-)) %.
%term pair- %pi (exp A-) %-> (exp B-) %-> (val- (with A- B-)) %.
%term mt- val- top %.
%term delay+ %pi (val+ A+) %-> (val- (up A+)) %.
%% wait to peel off shift until focus
%% neutral sequents
%term return %pi (val- A) %-> (exp A) %.
%% canonical when the value is a variable;
%% non-canonical otherwise
%term cut+ %pi (val+ A+) %-> (cont+ A+ C) %-> (exp C) %.
%% non-canonical
%term cut- %pi (val- A-) %-> (cont- A- C) %-> (exp C) %.
%% value variables can be used to stop right focus early
%block valb [A] {x val+ A}%.
%worlds (valb) (cont+ _ _) (cont- _ _) (val+ _) (exp _) (val- _) %.

Operational Semantics

Composition

%sort comp+- {_ cont+ A+ B-} {_ cont- B- C-} {_ cont+ A+ C-} %.
%mode comp+- %in %in %out %.
%sort compe- {_ exp A-} {_ cont- A- C-} {_ exp C-} %.
%mode compe- %in %in %out %.
%sort comp-- {_ cont- A- B-} {_ cont- B- C-} {_ cont- A- C-} %.
%mode comp-- %in %in %out %.
%% + -
%term comp+-/let1 %pi (comp+- (let1 E) K (let1 E')) %<- (compe- E K E') %.
%term comp+-/split %pi (comp+- (split E) K (split E')) %<- ({x} {y} compe- (E x y) K (E' x y)) %.
%term comp+-/case
  %pi (comp+- (case E1 E2) K (case E1' E2'))
  %<- ({x} compe- (E1 x) K (E1' x))
  %<- ({x} compe- (E2 x) K (E2' x)) %.
%term comp+-/force %pi (comp+- (force- K-) K (force- K-')) %<- (comp-- K- K K-') %.
%% e -
%term compe-/return compe- (return V) K (cut- V K) %.
%term compe-/cut- %pi (compe- (cut- V K1) K2 (cut- V K3)) %<- (comp-- K1 K2 K3) %.
%term compe-/cut+ %pi (compe- (cut+ V K1) K2 (cut+ V K3)) %<- (comp+- K1 K2 K3) %.
%% - -
%term comp--/app %pi (comp-- (app V K1) K2 (app V K3)) %<- (comp-- K1 K2 K3) %.
%term comp--/fst %pi (comp-- (fst K1) K2 (fst K3)) %<- (comp-- K1 K2 K3) %.
%term comp--/snd %pi (comp-- (snd K1) K2 (snd K3)) %<- (comp-- K1 K2 K3) %.
%term comp--/force %pi (comp-- (force+ E) K2 (force+ E')) %<- ({x} compe- (E x) K2 (E' x)) %.
%term comp--/id comp-- id- K2 K2 %.
%worlds (valb) (comp+- _ _ _) (comp-- _ _ _) (compe- _ _ _) %.
%total (D1 D2 D3) (comp+- D1 _ _) (comp-- D3 _ _) (compe- D2 _ _) %.

Stack Machine

%% the sum type that you'd define for progress is
%% (val C) + (exp C)
%% so let's just abuse exp C for this sum and write the
%% operational semantics as the progress proof.
%% the only downside is that you can't tell whether an expression
%% took a real step towards a value or already was a value.
%sort step {_ exp C} {_ exp C} %.
%mode step %in %out %.
%term step/return step (return V) (return V) %.
%term step/let1 step (cut+ mt+ (let1 E)) E %.
%term step/split step (cut+ (pair+ V1 V2) (split E)) (E V1 V2) %.
%term step/case1 step (cut+ (inl V1) (case E1 E2)) (E1 V1) %.
%term step/case2 step (cut+ (inr V2) (case E1 E2)) (E2 V2) %.
%term step/force- %pi (step (cut+ (delay- E) (force- K)) E') %<- (compe- E K E') %.
%term step/app %pi (step (cut- (lam E) (app V K)) E') %<- (compe- (E V) K E') %.
%term step/fst %pi (step (cut- (pair- E1 E2) (fst K)) E') %<- (compe- E1 K E') %.
%term step/snd %pi (step (cut- (pair- E1 E2) (snd K)) E') %<- (compe- E2 K E') %.
%term step/force+ step (cut- (delay+ V) (force+ E)) (E V) %.
%term step/id step (cut- V id-) (return V) %.
%worlds () (step _ _) %.
%total D (step D _) %.