gistfile1.md

[| 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) ・・・(1)
                                                ~~~~~~~~~~~~~(2)
(2)を変換
[|x (x 100)|]
app2  -> (λk4.[|x|] (λf1.[|x 100|] (λa2.f1 a2 k4)))
val   -> (λk4.(λk5.k5 x) (λf1.[|x 100|] (λa2.f1 a2 k4)))
app2  -> (λk4.(λk5.k5 x) (λf1.(λk6.[|x|] (λf2.[|100|] (λa3.f2 a3 k6))) (λa2.f1 a2 k4)))
val   -> (λk4.(λk5.k5 x) (λf1.(λk6.(λk7.k7 x) (λf2.[|100|] (λa3.f2 a3 k6))) (λa2.f1 a2 k4)))
val   -> (λk4.(λk5.k5 x) (λf1.(λk6.(λk7.k7 x) (λf2.(λk8.k8 100) (λa3.f2 a3 k6))) (λa2.f1 a2 k4)))

(2)を(1)に戻す
λk1.k1 ((λk2.(λk3.[x↦λa.λk'.k' (k3 a)]([|x (x 100)|] id)) (λa1.k2 (add10 a1))) id) ・・・(1)
                                       ~~~~~~~~~~~~~(2)
= λ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)・・・(3)

(3)をidに適用したものを簡約
(λ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)) id
↝ id ((λ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)
↝ (λ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・・・(4)
↝ (λ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.id (add10 a1))
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λk4.(λk5.k5 x) (λf1.(λk6.(λk7.k7 x) (λf2.(λk8.k8 100) (λa3.f2 a3 k6))) (λa2.f1 a2 k4))) id)
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λk5.k5 x) (λf1.(λk6.(λk7.k7 x) (λf2.(λk8.k8 100) (λa3.f2 a3 k6))) (λa2.f1 a2 id)))
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λf1.(λk6.(λk7.k7 x) (λf2.(λk8.k8 100) (λa3.f2 a3 k6))) (λa2.f1 a2 id)) x)
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λk6.(λk7.k7 x) (λf2.(λk8.k8 100) (λa3.f2 a3 k6))) (λa2.x a2 id))
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λk7.k7 x) (λf2.(λk8.k8 100) (λa3.f2 a3 (λa2.x a2 id))))
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λf2.(λk8.k8 100) (λa3.f2 a3 (λa2.x a2 id))) x)
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λk8.k8 100) (λa3.x a3 (λa2.x a2 id)))
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λa3.x a3 (λa2.x a2 id)) 100)
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)](x 100 (λa2.x a2 id))
= [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λa.λk'.k' ((λa1.id (add10 a1)) a)) 100 (λa2.x a2 id))
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λk'.k' ((λa1.id (add10 a1)) 100)) (λa2.x a2 id))
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)]((λa2.x a2 id) ((λa1.id (add10 a1)) 100))
↝ [x↦λa.λk'.k' ((λa1.id (add10 a1)) a)](x ((λa1.id (add10 a1)) 100) id)
= (λa.λk'.k' ((λa1.id (add10 a1)) a)) ((λa1.id (add10 a1)) 100) id
↝ (λk'.k' ((λa1.id (add10 a1)) ((λa1.id (add10 a1)) 100))) id
↝ id ((λa1.id (add10 a1)) ((λa1.id (add10 a1)) 100))
↝ (λa1.id (add10 a1)) ((λa1.id (add10 a1)) 100)
↝ id (add10 ((λa1.id (add10 a1)) 100))
↝ add10 ((λa1.id (add10 a1)) 100)
↝ add10 (id (add10 100))
↝ add10 (add10 100)
↝ add10 110
↝ 120

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

         [|add1 <add10 (Sx.x (x 100))>|]
app1  -> λk0.[|<add10 (Sx.x (x 100))>|] (λa0.k0 (add1 a0))
             ~~~~~~~~~~~~~~~~~~~~~~~~~~(5)
(5)は(3)になるため、
λk0.(λ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)) (λa0.k0 (add1 a0))・・・(6)
となる。

(6)をidに適用したものを簡約
(λk0.(λ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)) (λa0.k0 (add1 a0))) id
↝ (λ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)) (λa0.id (add1 a0))
↝ id (add1 ((λ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))
↝ add1 ((λ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)
       ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~(4)
       
(4)より
↝ add1 120
↝ 121