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