See https://gist.github.com/bleis-tift/99875ff6fbc2c3861b8907bf7b2336f7

cps

[| x     |] = λk.k x                              ・・・val
[| λx.t |] = λk.k (λx.[|t|])                      ・・・lam
[| π t  |] = λk.[|t|] (λa.k (π a))                ・・・app1
[| t1 t2 |] = λk.[|t1|] (λf.[|t2|] (λa.f a k))    ・・・app2
[| Sx.t  |] = λk.[x↦λa.λk'.k' (k a)]([|t|] (λv.v))・・・shift
[| <t>   |] = λk.k ([|t|] (λv.v))                 ・・・reset

変換対象: <add10 (Sx.x (x 100))>

[|<add10 (Sx.x (x 100))>|]
reset -> λk1.k1 ([|add10 (Sx.x (x 100))|] id)
app1  -> λk1.k1 ((λk2.[|Sx.x (x 100)|] (λa1.k2 (add10 a1))) id)
shift -> λk1.k1 ((λk2.(λk3.[x↦λa.λk'.k' (k3 a)]([|x (x 100)|] id)) (λa1.k2 (add10 a1))) id)
app2  -> λk1.k1 ((λk2.(λk3.[x↦λa.λk'.k' (k3 a)]((λk4.[|x|] (λf1.[|(x 100)|] (λa2.f1 a2 k4))) id)) (λa1.k2 (add10 a1))) id)
val   -> λk1.k1 ((λk2.(λk3.[x↦λa.λk'.k' (k3 a)]((λk4.(λk5.k5 x) (λf1.[|(x 100)|] (λa2.((f1 a2) k4)))) id)) (λa1.k2 (add10 a1))) id)
app2  -> λk1.k1 ((λk2.(λk3.[x↦λa.λk'.k' (k3 a)]((λk4.(λk5.k5 x) (λf1.(λk6.[|x|] (λf2.[|100|] (λa3.((f2 a3) k6)))) (λa2.((f1 a2) k4)))) id)) (λa1.k2 (add10 a1))) id)
val   -> λk1.k1 ((λk2.(λk3.[x↦λa.λk'.k' (k3 a)]((λk4.(λk5.k5 x) (λf1.(λk6.(λk7.k7 x) (λf2.[|100|] (λa3.((f2 a3) k6)))) (λa2.((f1 a2) k4)))) id)) (λa1.k2 (add10 a1))) id)
val   -> λk1.k1 ((λk2.(λk3.[x↦λa.λk'.k' (k3 a)]((λk4.(λk5.k5 x) (λf1.(λk6.(λk7.k7 x) (λf2.(λk8.k8 100) (λa3.((f2 a3) k6)))) (λa2.((f1 a2) k4)))) id)) (λa1.k2 (add10 a1))) id)
ここで [x↦(λa.λk'.k' (k3 a))]
         λk1.k1 ((λk2.(λk3.((λk4.(λk5.k5 (λa4.λk9.k9 (k3 a4))) (λf1.(λk6.(λk7.k7 (λa5.λk10.k10 (k3 a5))) (λf2.(λk8.k8 100) (λa3.((f2 a3) k6)))) (λa2.((f1 a2) k4)))) id)) (λa1.k2 (add10 a1))) id) ...(1)
(1) を外側のλk1以外簡約
-> λk1.k1 ((λk3.((λk4.(λk5.k5 (λa4.λk9.k9 (k3 a4))) (λf1.(λk6.(λk7.k7 (λa5.λk10.k10 (k3 a5))) (λf2.(λk8.k8 100) (λa3.((f2 a3) k6)))) (λa2.((f1 a2) k4)))) id)) (λa1.id (add10 a1)))
-> λk1.k1 (((λk4.(λk5.k5 (λa4.λk9.k9 ((λa1.id (add10 a1)) a4))) (λf1.(λk6.(λk7.k7 (λa5.λk10.k10 ((λa1.id (add10 a1)) a5))) (λf2.(λk8.k8 100) (λa3.((f2 a3) k6)))) (λa2.((f1 a2) k4)))) id))
-> λk1.k1 ((λk5.k5 (λa4.λk9.k9 ((λa1.id (add10 a1)) a4))) (λf1.(λk6.(λk7.k7 (λa5.λk10.k10 ((λa1.id (add10 a1)) a5))) (λf2.(λk8.k8 100) (λa3.((f2 a3) k6)))) (λa2.((f1 a2) id))))
-> λk1.k1 ((λf1.(λk6.(λk7.k7 (λa5.λk10.k10 ((λa1.id (add10 a1)) a5))) (λf2.(λk8.k8 100) (λa3.((f2 a3) k6)))) (λa2.((f1 a2) id))) (λa4.λk9.k9 ((λa1.id (add10 a1)) a4)))
-> λk1.k1 ((λk6.(λk7.k7 (λa5.λk10.k10 ((λa1.id (add10 a1)) a5))) (λf2.(λk8.k8 100) (λa3.((f2 a3) k6)))) (λa2.(((λa4.λk9.k9 ((λa1.id (add10 a1)) a4)) a2) id)))
-> λk1.k1 ((λk7.k7 (λa5.λk10.k10 ((λa1.id (add10 a1)) a5))) (λf2.(λk8.k8 100) (λa3.((f2 a3) (λa2.(((λa4.λk9.k9 ((λa1.id (add10 a1)) a4)) a2) id))))))
-> λk1.k1 ((λf2.(λk8.k8 100) (λa3.((f2 a3) (λa2.(((λa4.λk9.k9 ((λa1.id (add10 a1)) a4)) a2) id))))) (λa5.λk10.k10 ((λa1.id (add10 a1)) a5)))
-> λk1.k1 ((λk8.k8 100) (λa3.(((λa5.λk10.k10 ((λa1.id (add10 a1)) a5)) a3) (λa2.(((λa4.λk9.k9 ((λa1.id (add10 a1)) a4)) a2) id)))))
-> λk1.k1 ((λa3.(((λa5.λk10.k10 ((λa1.id (add10 a1)) a5)) a3) (λa2.(((λa4.λk9.k9 ((λa1.id (add10 a1)) a4)) a2) id)))) 100)
-> λk1.k1 (((λa5.λk10.k10 ((λa1.id (add10 a1)) a5)) 100) (λa2.(((λa4.λk9.k9 ((λa1.id (add10 a1)) a4)) a2) id)))
-> λk1.k1 ((λk10.k10 ((λa1.id (add10 a1)) 100)) (λa2.(((λa4.λk9.k9 ((λa1.id (add10 a1)) a4)) a2) id)))
-> λk1.k1 ((λa2.(((λa4.λk9.k9 ((λa1.id (add10 a1)) a4)) a2) id)) ((λa1.id (add10 a1)) 100))
-> λk1.k1 (((λa4.λk9.k9 ((λa1.id (add10 a1)) a4)) ((λa1.id (add10 a1)) 100)) id)
-> λk1.k1 ((λk9.k9 ((λa1.id (add10 a1)) ((λa1.id (add10 a1)) 100))) id)
-> λk1.k1 (id ((λa1.id (add10 a1)) ((λa1.id (add10 a1)) 100)))
-> λk1.k1 ((λa1.id (add10 a1)) ((λa1.id (add10 a1)) 100))
-> λk1.k1 (id (add10 ((λa1.id (add10 a1)) 100)))
-> λk1.k1 (add10 ((λa1.id (add10 a1)) 100))
-> λk1.k1 (add10 (id (add10 100)))
-> λk1.k1 (add10 (add10 100))