(no subject)
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:
( Collapse )
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.
( Collapse )
