September 1st, 2012

beartato phd

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

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 )