Turns out the logic is even more refined than nonassociative ordered logic: there's two classes of hypotheses, continuations and intermediate results, and while the intermediate results form a stack, the continuation is always at the base of it, and there's only ever one of 'em. So I have two sorts of worlds, wd and vd.
Didn't prove that the two translations are inverse, but a sanity check on an example works:
in = (dlam [y] e2r (t2e (dlam [x] e2r (dapp (t2e y) (dapp (t2e y) (t2e x)))))). %define out = V %solve _ : cps/t in V. %define out2 = V %solve _ : ds/t out V. == : dt A -> dt A -> type. refl : == X X. check : {X}{Y} == X Y -> type. / : check in out2 refl.
o : type. % simple types a : o. => : o -> o -> o. %infix right 30 =>. %name o A. % Direct-style types dr : o -> type. % roots de : o -> type. % expressions dt : o -> type. % terms %name dr DR dr. %name de DE de. %name dt DT dt. % Direct-style terms t2e : dt A -> de A. e2r : de A -> dr A. dapp : de (A => B) -> de A -> de B. dlam : (dt A -> dr B) -> dt (A => B). % Substructural logic wd : type. %name wd W w. vd : type. %name vd V v. * : wd -> vd -> wd. %infix none 30 *. % CPS-style types cr : o -> type. % roots ce : wd -> type. % expressions ci : o -> vd -> type. % intermediate value on the stack ct : o -> type. % closed trivial value cc : o -> wd -> type. % continuations %name cr CR r. %name ce CE e. %name ct CT t. %name ci CI i. %name cc CC c. % CPS-style terms klam : ({w} cc A w -> ce w) -> cr A. kapp : ct A -> cc A W -> ce W. app : cc B W -> ci (A => B) V1 -> ci A V2 -> ce ((W * V1) * V2). lam : (ct A -> cr B) -> ct (A => B). vlam : ({v} ci A v -> ce (W * v)) -> cc A W. % klam : (cc ->> ce) -> cr % kapp : ct -> cc ->> ce % app : cc -o ci ->> ci ->> ce % lam : (ct -> cr) -> ct % vlam : (ci ->> ce) -o cc % CPS translation cps/r : dr A -> cr A -> type. cps/e : de A -> cc A W -> ce W -> type. cps/t : dt A -> ct A -> type. / : cps/r (e2r E) (klam E') <- {wc}{c} cps/e E c (E' wc c). / : cps/e (t2e T) C (kapp T' C) <- cps/t T T'. / : cps/e (dapp E1 E2) C E1' <- ({vf:vd} {f:ci _ vf} cps/e E2 (vlam [vx] [x] app C f x) (E2' vf f)) <- cps/e E1 (vlam [vf] [f] E2' vf f) E1'. / : cps/t (dlam R) (lam R') <- {t:dt A} {t':ct A} {d: cps/t t t'} cps/r (R t) (R' t'). % DS translation wof : wd -> o -> type. wof/cons : wof (W * V) A <- wof W A. ds/r : cr A -> dr A -> type. ds/e : ce W -> wof W A -> de A -> type. ds/c : cc B W -> wof W A -> de B -> de A -> type. ds/t : ct A -> dt A -> type. ds/i : ci A V -> de A -> type. pop : wof (W * V) B -> wof W B -> type. pop/ : pop (wof/cons M) M. / : ds/t (lam R) (dlam R') <- {x:ct A} {x':dt A} {d: ds/t x x'} ds/r (R x) (R' x'). / : ds/r (klam E') (e2r E) <- {wc}{c}{d:wof wc _}{d2: {dex} ds/c c d dex dex} ds/e (E' wc c) d E. / : ds/e (kapp V C) M E <- ds/t V V' <- ds/c C M (t2e V') E. / : ds/e (app C I1 I2) M E <- pop M M' <- pop M' M'' <- ds/i I2 E2 <- ds/i I1 E1 <- ds/c C M'' (dapp E1 E2) E. / : ds/c (vlam ([vi][i] E vi i)) M (E0 : de B) (E' : de A) <- {vi}{i}{d:ds/i i E0} ds/e (E vi i) (wof/cons M) E'. % Theorem: CPS translation is total %mode (cps/r +R -R') (cps/e +E +C -E') (cps/t +T -T'). %block b1 : some {A:o} block {x:dt A} {x':ct A} {d: cps/t x x'}. %block b2 : some {A:o} block {vx:vd} {x:ci A vx}. %block b3 : some {A:o} block {wc:wd} {x:cc A wc}. %worlds (b1 | b2 | b3) (cps/r R R') (cps/e E C E') (cps/t T T'). %total (R E T) (cps/r R R') (cps/e E C E') (cps/t T T'). % Theorem: DS translation is total %mode (ds/r +R -R') (ds/e +E +M -E') (ds/c +C +M +E -E') (ds/t +T -T') (ds/i +I -E) (pop +M -M'). %block d1 : some {A:o} block {x:ct A} {x':dt A} {d: ds/t x x'}. %block d2 : some {A:o} block {wc : wd}{c : cc A wc}{d : wof wc A}{d2: {dex:de A} ds/c c d dex dex}. %block d3 : some {A:o} {E0:de A} block {vi:vd} {i : ci A vi} {d : ds/i i E0}. %worlds (d1 | d2 | d3) (ds/r R R') (ds/e E M E') (ds/c C M E E') (ds/t T T') (ds/i I E) (pop M M'). %total (M) (pop M _). %total (R E C T I) (ds/r R _) (ds/e E _ _) (ds/c C _ _ _) (ds/t T _) (ds/i I _).