POPL Tutorial/CPS

From The Twelf Project
Jump to: navigation, search

CPS Conversion

%% Intuitionistic logic

iprop : type.                     %name iprop A'.

itop : iprop.
iimp : iprop -> iprop -> iprop.

%block ipb : block {X : iprop}.
%worlds (ipb) (iprop).

itrue : iprop -> type.

imt : itrue itop.
ilam : (itrue A -> itrue B) -> itrue (iimp A B).
iapp : itrue (iimp A B) -> itrue A -> itrue B.

%block itb : some {A : iprop} block {D : itrue A}.
%worlds (ipb | itb) (itrue _).

%% Classical logic

prop : type.                     %name prop A.

top : prop.
and : prop -> prop -> prop.
not : prop -> prop.

%block pb : block {X : prop}.
%worlds (pb) (prop).

conc : type.
true : prop -> conc. %prefix 2 true.
contra : conc.

>> : conc -> type. %prefix 3 >>.

mt : >> true top.
pair : >> true A -> >> true B -> >> true (and A B).
fst : >> true (and A B) -> >> true A.
snd : >> true (and A B) -> >> true B.
noti    : (>> true A -> >> contra) -> >> true (not A).
notcase : >> true (not A) -> ((>> true A -> >> contra) -> >> J) -> >> J.

letcc : ((>> true A -> >> contra) -> >> contra) -> >> true A.

%block tb : some {A : prop} block {D : >> true A}.
%block fb : some {A : prop} block {D : (>> true A -> >> contra)}.
%worlds (pb | tb | fb) (>> _).

%% Proposition translation

* : iprop -> prop -> type.
%mode * +A' -A.

*/top : * itop top.

*/imp : * (iimp A1' A2') (not (and A1 (not A2)))
         <- * A1' A1
         <- * A2' A2.

%worlds () (* _ _).
%total D (* D _).

%% Lemmas

eqprop : prop -> prop -> type.
eqprop_ : eqprop A A.

eqprop/and : eqprop A1 A2 -> eqprop A3 A4 -> eqprop (and A1 A3) (and A2 A4) -> type.
%mode eqprop/and +A +B -C.
- : eqprop/and eqprop_ eqprop_ eqprop_.

eqprop/not : eqprop A1 A2 -> eqprop (not A1) (not A2) -> type.

%mode eqprop/not +A -B.
- : eqprop/not eqprop_ eqprop_.

true_resp : >> true A -> eqprop A A' -> >> true A' -> type.
%mode true_resp +Dtrue +EQ -Dtrue'.
- : true_resp D eqprop_ D.

*_fun : * A' A1 -> * A' A2 -> eqprop A1 A2 -> type.
%mode *_fun +X +Y -Z.

- : *_fun */top */top eqprop_.

- : *_fun (*/imp (DB1:* B' B1) (DA1:* A' A1)) (*/imp (DB2:* B' B2) (DA2:* A' A2))
     (EQ:eqprop (not (and A1 (not B1))) (not (and A2 (not B2))))
     <- *_fun DA1 DA2 (EQA:eqprop A1 A2)
     <- *_fun DB1 DB2 (EQB:eqprop B1 B2)
     <- eqprop/not EQB (EQnotB:eqprop (not B1) (not B2))
     <- eqprop/and EQA EQnotB (EQand:eqprop (and A1 (not B1)) (and A2 (not B2)))
     <- eqprop/not EQand EQ.

*_gimme : {A1':iprop} {A1:prop} * A1' A1 -> type.
%mode *_gimme +A1' -A1 -DA1.

- : *_gimme itop top */top.

- : *_gimme (iimp A1' A2') (not (and A1 (not A2))) (*/imp DA2 DA1)
     <- *_gimme A1' A1 (DA1:* A1' A1)
     <- *_gimme A2' A2 (DA2:* A2' A2).

%worlds () (*_fun _ _ _) (eqprop/and _ _ _) (eqprop/not _ _).

%total D (eqprop/and D _ _).
%total D (eqprop/not D _).
%total D (*_fun D _ _).

%% CPS conversion

tocps : {Ditrue : itrue A'}
        {DA : * A' A}
        {Dtrue : >> true A}
        type.
%mode tocps +Ditrue -DA -Dtrue.

cps/top : tocps imt */top mt.

cps/lam : tocps (ilam (Ditrue : itrue A1' -> itrue A2'))
           (*/imp (DA2 : * A2' A2) (DA1 : * A1' A1))
           (noti ([Dtruep : >> true (and A1 (not A2))]
                    notcase (snd Dtruep) ([Dfalse : >> true A2 -> >> contra]
                                            Dfalse (Dtrue (fst Dtruep)))))
           <- *_gimme A1' A1 DA1
           <- ({Ditrue1 : itrue A1'}
                 {Dtrue1 : >> true A1}
                 {thm:tocps Ditrue1 DA1 Dtrue1}
                 tocps (Ditrue Ditrue1) DA2 (Dtrue Dtrue1)).

cps/app : tocps (iapp (Ditrue:itrue (iimp A1' A2')) (Ditrue1:itrue A1'))
           DA2
           (letcc [Ddn:>> true A2 -> >> contra]
              (notcase Dtrue ([Dfalse:>> true (and A1 (not A2)) -> >> contra]
                                Dfalse (pair Dtrue1 (noti Ddn)))))
           <- tocps Ditrue (*/imp DA2 DA1) (Dtrue:>> true (not (and A1 (not A2))))
           <- tocps Ditrue1 (DA10:* A1' A10) (Dtrue1':>> true A10)
           <- *_fun DA10 DA1 EQ
           <- true_resp Dtrue1' EQ (Dtrue1:>> true A1).

%block blocktrue :
              some {A' : iprop} {A : prop} {DA : * A' A}
              block
               {Ditrue : itrue A'}
               {Dtrue : >> true A}
               {thm:tocps Ditrue DA Dtrue}.

%worlds (blocktrue)
                 (tocps _ _ _)
                 (true_resp _ _ _)
                 (*_gimme _ _ _).

%total A (true_resp _ A _).
%total A (*_gimme A _ _).

%total A (tocps A _ _).