Polarized PCF

Polarized PCF with a stack machine semantics

• Interalizes the composition/leftist substitution principles (left-commutative cuts), so there are no meta-ops in evaluation other than LF substitution
• force+ binds a positive value variable, rather than requiring an immediate left inversion
• Proves completeness of focusing, so you can see what direct-style terms mean
• Does purely negative stream using (non-canonical) negative continuation variables; completeness of focusing does some sort of CPS conversion

Syntax

%sort pos %.
%sort neg %.
%term down %pi neg %-> pos %.
%term nat pos %.
%term up %pi pos %-> neg %.
%term arr %pi pos %-> neg %-> neg %.
%term stream %pi neg %-> neg %.
%sort val+ {_ pos} %.
%sort cont+ {_ pos} {_ pos} %.
%sort val- {_ neg} %.
%sort cont- {_ neg} {_ pos} %.
%sort exp {_ pos} %.
%% positive values
%term zero val+ nat %.
%term succ %pi (val+ nat) %-> (val+ nat) %.
%term delay- %pi (val- A-) %-> (val+ (down A-)) %.
%% positive conts
%term ifz %pi (exp A+) %-> (%pi (val+ nat) %-> (exp A+)) %-> (cont+ nat A+) %.
%term force- %pi (%pi (val- A-) %-> (exp C+)) %-> (cont+ (down A-) C+) %.
%% internalize composition
%term comp+ %pi (cont+ A+ B+) %-> (%pi (val+ B+) %-> (exp C+)) %-> (cont+ A+ C+) %.
%% negative values
%term lam %pi (%pi (val+ A+) %-> (val- B-)) %-> (val- (arr A+ B-)) %.
%term delay+ %pi (exp A+) %-> (val- (up A+)) %.
%term fix %pi (%pi (val- A-) %-> (val- A-)) %-> (val- A-) %.
%term cons
  %pi ({C+} %pi (cont- A- C+) %-> (exp C+))
  %-> ({C+} %pi (cont- (stream A-) C+) %-> (exp C+))
  %-> (val- (stream A-)) %.
%% negative conts
%term app %pi (val+ A+) %-> (cont- B- C+) %-> (cont- (arr A+ B-) C+) %.
%term force+ %pi (%pi (val+ A+) %-> (exp C+)) %-> (cont- (up A+) C+) %.
%% internalize composition
%term comp- %pi (cont- A- B+) %-> (%pi (val+ B+) %-> (exp C+)) %-> (cont- A- C+) %.
%term head %pi (cont- A- C+) %-> (cont- (stream A-) C+) %.
%term tail %pi (cont- (stream A-) A+) %-> (cont- (stream A-) A+) %.
%% expressions
%term ret %pi (val+ A+) %-> (exp A+) %.
%% internalize arbitrary cuts.
%% these two are canonical when the value is a variable,
%% but if we'ere only running closed terms, then that
%% distinction is moot.
%term cut+ %pi (val+ A+) %-> (cont+ A+ C+) %-> (exp C+) %.
%term cut- %pi (val- A-) %-> (cont- A- C+) %-> (exp C+) %.
%% internalize composition
%term let %pi (exp A+) %-> (%pi (val+ A+) %-> (exp C+)) %-> (exp C+) %.
%% these terms are not eta-long, because we use the same
%% val judgements on the left as on the right
%block posb [A+ pos] {x val+ A+}%.
%block negb [A- neg] {x val- A-}%.
%block negcb [A- neg] {A+ pos} {k cont- A- A+}%.
%worlds (posb negb negcb) (val+ _) (cont+ _ _) (val- _) (cont- _ _) (exp _) %.
%% FIXME: weirldly asymetric: we need both pos and neg assumptions,
%% but not both kinds of conclusion??

Step

Note that all rules are axioms.

%sort step {_ exp A+} {_ exp A+} %.
%mode step %in %out %.
%term step/ifz-0 step (cut+ zero (ifz E0 E1)) E0 %.
%term step/ifz-1 step (cut+ (succ V) (ifz E0 E1)) (E1 V) %.
%term step/force- step (cut+ (delay- V-) (force- E)) (E V-) %.
%term step/fix step (cut- (fix E) K-) (cut- (E (fix E)) K-) %.
%term step/app step (cut- (lam V-) (app V+ K-)) (cut- (V- V+) K-) %.
%term step/force+ step (cut- (delay+ E1) (force+ E)) (let E1 E) %.
%term step/head step (cut- (cons E1 E2) (head K-)) (E1 _ K-) %.
%term step/tail step (cut- (cons E1 E2) (tail K-)) (E2 _ K-) %.
%% left commutative cuts:
%term step/letret step (let (ret V+) E2) (E2 V+) %.
%term step/letcut+ step (let (cut+ V+ K+) E2) (cut+ V+ (comp+ K+ E2)) %.
%term step/letcut- step (let (cut- V- K-) E2) (cut- V- (comp- K- E2)) %.
%term step/letlet step (let (let E1 E2) E3) (let E1 ([x] let (E2 x) E3)) %.
%term step/cconv-ifz step (cut+ V+ (comp+ (ifz E0 E1) E)) (cut+ V+ (ifz (let E0 E) ([y] let (E1 y) E))) %.
%term step/cconv-force- step (cut+ V+ (comp+ (force- E1) E)) (cut+ V+ (force- ([y] let (E1 y) E))) %.
%term step/cconv-comp+ step (cut+ V+ (comp+ (comp+ E1 E2) E)) (cut+ V+ (comp+ E1 ([y] let (E2 y) E))) %.
%term step/cconv-app step (cut- V- (comp- (app V+ K-) E)) (cut- V- (app V+ (comp- K- E))) %.
%term step/cconv-force+ step (cut- V- (comp- (force+ E1) E)) (cut- V- (force+ ([y] let (E1 y) E))) %.
%term step/cconv-comp- step (cut- V- (comp- (comp- K- E1) E2)) (cut- V- (comp- K- ([y] let (E1 y) E2))) %.
%term step/cconv-head step (cut- V- (comp- (head K-) E)) (cut- V- (head (comp- K- E))) %.
%term step/cconv-tail step (cut- V- (comp- (tail K-) E)) (cut- V- (tail (comp- K- E))) %.
%worlds () (step _ _) %.

Progress

%sort ok {_ exp A+} %.
%term ok/final ok (ret V+) %.
%term ok/step %pi (ok E) %<- (step E E') %.
%sort progress {E exp A+} {_ ok E} %.
%mode progress %in %out %.
%term _ progress _ ok/final %.
%term _ progress _ (ok/step step/ifz-0) %.
%term _ progress _ (ok/step step/ifz-1) %.
%term _ progress _ (ok/step step/force-) %.
%term _ progress _ (ok/step step/fix) %.
%term _ progress _ (ok/step step/app) %.
%term _ progress _ (ok/step step/force+) %.
%term _ progress _ (ok/step step/head) %.
%term _ progress _ (ok/step step/tail) %.
%term _ progress _ (ok/step step/letret) %.
%term _ progress _ (ok/step step/letcut+) %.
%term _ progress _ (ok/step step/letcut-) %.
%term _ progress _ (ok/step step/letlet) %.
%term _ progress _ (ok/step step/cconv-ifz) %.
%term _ progress _ (ok/step step/cconv-force-) %.
%term _ progress _ (ok/step step/cconv-comp+) %.
%term _ progress _ (ok/step step/cconv-app) %.
%term _ progress _ (ok/step step/cconv-force+) %.
%term _ progress _ (ok/step step/cconv-head) %.
%term _ progress _ (ok/step step/cconv-tail) %.
%term _ progress _ (ok/step step/cconv-comp-) %.
%worlds () (progress _ _) %.
%total {} (progress _ _) %.

EL

Syntax

%sort etp %.
%name etp %.
%term enat etp %.
%term earr %pi etp %-> etp %-> etp %.
%term estream %pi etp %-> etp %.
%sort eexp {_ etp} %.
%name eexp %.
%prec %postfix 1 eexp %.
%term ez enat eexp %.
%term es %pi (enat eexp) %-> (enat eexp) %.
%term eifz %pi (enat eexp) %-> (T eexp) %-> (%pi (enat eexp) %-> (T eexp)) %-> (T eexp) %.
%term efun {T1 etp} {T2 etp} %pi (%pi (earr T1 T2 eexp) %-> (T1 eexp) %-> (T2 eexp)) %-> (earr T1 T2 eexp) %.
%term eapp %pi (earr T1 T2 eexp) %-> (T1 eexp) %-> (T2 eexp) %.
%term econs %pi (T eexp) %-> (estream T eexp) %-> (estream T eexp) %.
%term estreamfix %pi (%pi (estream T eexp) %-> (estream T eexp)) %-> (estream T eexp) %.
%term ehead %pi (estream T eexp) %-> (T eexp) %.
%term etail %pi (estream T eexp) %-> (estream T eexp) %.

Completeness of focusing

%sort poltp {_ etp} {_ pos} %.
%mode poltp %in %out %.
%term poltp/nat poltp enat nat %.
%term poltp/arr
  %pi (poltp (earr T1 T2) (down (arr A1 (up A2))))
  %<- (poltp T1 A1)
  %<- (poltp T2 A2) %.
%term poltp/stream %pi (poltp (estream T) (down (stream (up A)))) %<- (poltp T A) %.
%worlds () (poltp _ _) %.
%total T (poltp T _) %.
%unique poltp %in %out %.
%sort can-poltp {T} {_ poltp T A} %.
%mode can-poltp %in %out %.
%worlds () (can-poltp _ _) %.
% not really a trustme: Twelf proved this totality above!
%total {} (can-poltp _ _) %.
%sort id {_ pos} {_ pos} %.
%term refl id A A %.
%sort unique-poltp {_ poltp T A'} {_ poltp T A} {_ id A A'} %.
%mode unique-poltp %in %in %out %.
%worlds () (unique-poltp _ _ _) %.
% not really a trustme: Twelf proved this totality above!
%total {} (unique-poltp _ _ _) %.
%sort retype {_ exp A} {_ id A A'} {_ exp A'} %.
%mode retype %in %in %out %.
%term _ retype D refl D %.
%worlds (posb negb) (retype _ _ _) %.
%total {} (retype _ _ _) %.
%sort complete {_ poltp T A} {_ T eexp} {_ exp A} %.
%mode complete %in %in %out %.
%term complete/z complete poltp/nat ez (ret zero) %.
%term complete/s
  %pi (complete poltp/nat (es E) (let E' ([x] ret (succ x))))
  %<- (complete poltp/nat E E') %.
%term complete/ifz
  %pi (complete (%the (poltp T A) Dpol) (eifz E E0 E1) (let E' ([x] cut+ x (ifz E0' E1'))))
  %<- (complete poltp/nat E E')
  %<- (complete Dpol E0 E0')
  %<- ({x enat eexp} {x' val+ nat} {d {A1' pos} {D' poltp enat A1'} {Did id nat A1'} {E exp A1'}
  %pi (complete D' x E)
  %<- (unique-poltp D' poltp/nat Did)
  %<- (retype (ret x') Did E)} complete Dpol (E1 x) (E1' x')) %.
%term complete/fun
  %pi (complete (poltp/arr (%the (poltp T2 A2) Dp2) (%the (poltp T1 A1) Dp1)) (efun T1 T2 E) (ret (delay- (fix ([f'] lam ([x'] delay+ (E' (delay- f') x')))))))
  %<- ({f earr T1 T2 eexp} {f' val+ (down (arr A1 (up A2)))} {d {A1' pos} {D' poltp (earr T1 T2) A1'} {Did id (down (arr A1 (up A2))) A1'} {E exp A1'}
  %pi (complete D' f E)
  %<- (unique-poltp D' (poltp/arr Dp2 Dp1) Did)
  %<- (retype (ret f') Did E)} {x T1 eexp} {x' val+ A1} {d {A1' pos} {D' poltp T1 A1'} {Did id A1 A1'} {E exp A1'} %pi (complete D' x E) %<- (unique-poltp D' Dp1 Did) %<- (retype (ret x') Did E)} complete Dp2 (E f x) (E' f' x')) %.
%term complete/app
  %pi (complete (%the (poltp T A) D) (eapp (%the (earr T2 T eexp) E1) E2) (let E1' ([f] let E2' ([x] cut+ f (force- ([y] cut- y (app x (force+ ([z] ret z)))))))))
  %<- (can-poltp T2 (%the (poltp T2 A2) Dp2))
  %<- (complete (poltp/arr D Dp2) E1 E1')
  %<- (complete Dp2 E2 E2') %.
%% cons is lazy in both components
%term complete/cons
  %pi (complete (poltp/stream Dp) (econs E1 E2) (ret (delay- (cons ([C+] [k] let E1' ([y] cut- (delay+ (ret y)) k)) ([C+] [k] let E2' ([y] cut+ y (force- ([w] cut- w k))))))))
  %<- (complete Dp E1 E1')
  %<- (complete (poltp/stream Dp) E2 E2') %.
%term complete/head
  %pi (complete D (ehead E) (let E' ([x] cut+ x (force- ([y] cut- y (head (force+ ([z] ret z))))))))
  %<- (complete (poltp/stream D) E E') %.
%term complete/tail
  %pi (complete (poltp/stream D) (etail E) (let E' ([x] cut+ x (force- ([y] ret (delay- (cons ([C] [hobs] cut- y (tail (head hobs))) ([C] [tobs] cut- y (tail (tail tobs))))))))))
  %<- (complete (poltp/stream D) E E') %.
%term complete/streamfix
  %pi (complete (poltp/stream D) (estreamfix E1) (ret (delay- (fix ([f] cons ([C] [hobs] let (E1' (delay- f)) ([r] cut+ r (force- ([r'] cut- r' (head hobs))))) ([C] [tobs] let (E1' (delay- f)) ([r] cut+ r (force- ([r'] cut- r' (tail tobs))))))))))
  %<- ({x _ eexp} {x' val+ _} {d {A1' pos} {D' poltp _ A1'} {Did id _ A1'} {E exp A1'}
  %pi (complete D' x E)
  %<- (unique-poltp D' (poltp/stream D) Did)
  %<- (retype (ret x') Did E)} complete (poltp/stream D) (E1 x) (E1' x')) %.
%block completeb [T1 etp] [A1 pos] [D poltp T1 A1] {x T1 eexp} {x' val+ A1} {d {A1' pos} {D' poltp T1 A1'} {Did id A1 A1'} {E exp A1'} %pi (complete D' x E) %<- (unique-poltp D' D Did) %<- (retype (ret x') Did E)}%.
%worlds (completeb) (complete _ E _) %.
%total (E) (complete _ E _) %.