Jason (jcreed) wrote,

Figured out how to do the inverse of the CPS translation, which Twelf happily accepts as total since enough ordered-context information is present to show that you can only use the continuation linearly.

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
(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
(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 _).

Tags: cps, logic, ordered, twelf

  • (no subject)

    Open-plan offices are potentially distracting, and the timesnpr is on it.

  • (no subject)

    Oh boy they replaced the burnt-out lights in my office. It is so much nicer in here now. Like night and day, I tell ya. In that, in particular, it is…

  • (no subject)

    Some time early last week, the ceiling in the hall outside of my office began leaking water. A janitor came by and placed a bucket under the leak.…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded