以下のような普通の関数を考える。
let add x y = x + y;;
let mul x y = x * y;;
let f () =
let a = add 1 2 in
let b = mul 3 a in
(a, b);;add と mul は結果を戻り値として返しているが、結果を継続に渡すような定義にしてみると、次のようになる。
let add2 x y k = k (x + y);; (* 継続にx + yの結果を渡す *)
let mul2 x y k = k (x * y);; (* 継続にx * yの結果を渡す *)上の関数を使うには、 k に後続処理を関数として渡す必要がある。
let f2 k =
add2 1 2 (fun a ->
mul2 3 a (fun b ->
k (a, b));;このような、継続を引数としてとるようなスタイルをCPS(継続渡しスタイル)と呼び、 最初の普通のスタイルをダイレクトスタイルと呼ぶ。 ダイレクトスタイルからCPSに変形することをCPS変換と呼ぶ。
ちなみに、一番外側の継続の引数には結果が入ってくるため、それをそのまま返せば答えが得られる。
let f () = f2 (fun res -> res);;これをshift/resetを使って書くとこのようになる。
let f3 () =
reset (fun () ->
let a = shift (fun k -> add2 1 2 k) in
let b = shift (fun k -> mul2 3 a k) in
(a, b)
);;継続を渡しているのに、ダイレクトスタイルで書けている。
let rec len xs =
match xs with
| [] -> 0 (* 空リストの場合の長さは0 *)
| _::rest -> 1 + (len rest);; (* 要素が1つ以上ある場合のリストの長さは、1 + (先頭を取り除いたリストの長さ) *)この関数をCPS変換してみる。
- 関数呼び出し部分を
letで結果を変数で受け取るようにする - 結果を継続に渡すようにする
let rec len xs =
match xs with
| [] -> 0
| _::rest ->
let lenRest = len rest in (* len呼び出しの結果を変数で受け取るようにした *)
1 + lenRest;;この len は最初の len と同じ意味、同じ使い方になる(単にローカル変数に抽出しただけ)。
書き換え規則
match x with pat_1 -> expr_1 | pat_2 -> expr_2 ... | pat_n -> expr_nのexpr_nに書き換え規則を適用するlet y = f x in zをf x (fun y -> k z)に書き換えるvalueをk valueに書き換える
let rec len2 xs k = (* この関数の継続を受け取るようにした *)
(* 書き換え規則1 *)
match xs with
| [] -> k 0 (* 書き換え規則3 *)
| _::rest ->
(* 書き換え規則2 *)
len2 rest (fun lenRest ->
k (1 + lenRest));;
let len xs = len2 xs (fun res -> res);;let rec len3 xs =
match xs with
| [] -> shift (fun k -> k 0)
| _::rest ->
1 + (shift (fun k -> k (len3 rest)));;
let len xs =
reset (fun () -> len3 xs);;shift/resetが使えると、ダイレクトスタイルで書けて便利。
let rec map f xs =
match xs with
| [] -> []
| first::rest ->
f first :: map f rest;;let rec map f xs =
match xs with
| [] -> []
| first::rest ->
let y = f first in
let ys = map f rest in
y::ys;;書き換え規則ver2
match x with pat_1 -> expr_1 | pat_2 -> expr_2 ... | pat_n -> expr_nのexpr_nに書き換え規則を適用するlet y = f x in zをf x (fun y -> z)に書き換え、zの部分に書き換え規則を適用するvalue::valuesをk (value::values)に書き換えるvalueをk valueに書き換える
let rec map2 f xs k = (* この関数の継続を受け取れるようにした *)
(* 書き換え規則1 *)
match xs with
| [] -> k [] (* 書き換え規則4 *)
| first::rest ->
f first (fun y -> (* 書き換え規則2 *)
map2 f rest (fun ys -> (* 書き換え規則2 *)
k (y::ys)));; (* 書き換え規則3 *)
let map f xs =
map2 (fun x k -> k (f x)) xs (fun res -> res);;(ラムダ計算とかに比べて)複雑な言語はルールをいっぱい用意しなくちゃいけなくてつらい。
実は今回のルールはかなり簡略化された不完全なもの(そもそも関数に追加した k はどこからやってきた？)。
let len xs =
let result = ref 0 in
let targets = ref xs in
while !targets <> [] do
incr result;
targets := tl (!targets)
done;
!result;;while を直接CPS変換するのは難しいので、再帰に書き換えてCPS変換する。
let rec lenRec result xs =
match xs with
| [] (* whileの条件の否定 *) -> xs (* whileの後続処理 *)
| targets ->
(* ↓ resultの書き換えを引数に移動 *)
lenRec (result + 1) (tl targets)
(* ↑ targetsの書き換えを引数に移動 *)あとは普通にCPS変換するだけ。
for も while に変換できるため、同様にCPS変換できる。
let rec mul xs =
reset (fun () ->
let result = ref 1 in
let targets = ref xs in
while !targets <> [] do
let x = hd (!targets) in
if x = 0 then
shift (fun _ -> 0)
else
result := !result * x;
targets := tl (!targets)
done;
!result
);;while だろうがお構いなしに継続が取れる。便利。
多くの関数型言語の基礎となっている計算モデル。 とてもシンプル(簡単とは言っていない)。
t ::= 項とは・・・
x * 変数
λx.t * ラムダ抽象
t t * 関数適用
のいずれかである
これだけ。 実際には、優先順位を表すためにかっこを使う。
簡約規則: プログラムを実行して結果を得るためのステップをルール化したもの。これを繰り返すことがプログラムを実行するということ。
v ::= 値とは・・・
λx.t ラムダ抽象
である
v1 t2 ↝ v1 t2' (t2 ↝ t2'の場合)
t1 t2 ↝ t1' t2 (t1 ↝ t1'の場合)
(λx.t1) v2 ↝ [x ↦ v2]t1
ここで、 [x ↦ v2]t1 とは、 t1 の中に現れる変数 x を値 v2 で置き換えることを意味している。
一般的なプログラミング言語的な表現をすると、
(x => x + 1)(20)
という式を
(20 + 1)
にすることを意味している。
実は何でもできる。 数字も表せるし、分岐やループも表せる。 計算能力は一般的なプログラミング言語と等しいことが分かっている。
ただし、書きやすいとは言っていない(下は1+2の例)。
v1 t2 ↝ v1 t2' (t2 ↝ t2'の場合)
t1 t2 ↝ t1' t2 (t1 ↝ t1'の場合)
(λx.t1) v2 ↝ [x ↦ v2]t1
plus = λm.λn.λs.λz. m s (n s z)
one = λs.λz.s z
two = λs.λz.s (s z)
plus one two = (λm.λn.λs.λz. m s (n s z)) (λs.λz.s z) (λs.λz.s (s z))
(λm.λn.λs.λz. m s (n s z)) (λs.λz.s z) (λs.λz.s (s z))
(λn.λs.λz. (λs.λz.s z) s (n s z)) (λs.λz.s (s z))
λs.λz. (λs.λz.s z) s ((λs.λz.s (s z)) s z)
λs.λz. (λz.s z) ((λs.λz.s (s z)) s z)
λs.λz. s ((λs.λz.s (s z)) s z)
λs.λz. s ((λz.s (s z)) z)
λs.λz. s (s (s z))
ラムダ計算を拡張してshiftとresetを導入する。
t ::= 項とは・・・
x * 変数
λx.t * ラムダ抽象
t t * 関数適用
Sx.t * shift
<t> * reset
のいずれかである
ラムダ計算に shift と reset を加えただけ・・・ではさすがにつらいので、数値も足してみると、
t ::= 項とは・・・
0,1,2,...* 数値
x * 変数
λx.t * ラムダ抽象
t t * 関数適用
Sx.t * shift
<t> * reset
のいずれかである
v ::= 値とは・・・
0,1,2,...* 数値
λx.t * ラムダ抽象
のいずれかである
[| x |]cps = λk.k x ・・・val (xが数値の場合も同様)
[| λx.t |]cps = λk.k (λx.[|t|]cps) ・・・lam
[| π t |]cps = λk.[|t|] (λa.k (π a)) ・・・app1
[| t1 t2 |]cps = λk.[|t1|]cps (λf.[|t2|]cps (λx.f x k)) ・・・app2
[| Sx.t |]cps = λk.[x ↦ λa.λk'.k' (k a)]([|t|]cps (λv.v))・・・shift
[| <t> |]cps = λk.k ([|t|]cps (λv.v)) ・・・reset
ここで、 [|...|]cps はかっこの中をCPS変換することを意味している。
また、 π はプリミティブな(CPSでない)関数。
例えば、 add10 が10を足すという関数だとして、 add10 20 をCPS変換することを考えると、
[|add10 20|]cps
と表し、 [|...|]cps がなくなるまで変換規則を適用していく。
変換を 変換前 適用規則名 -> 変換後 で表すとすると、
[|add10 20|]cps
app1 -> λk1.[|20|] (λa1.k1 (add10 a1))
val -> λk1.(λk2.k2 20) (λa1.k1 (add10 a1))
となる。
面倒なので、以降 [|...|]cps は単に [|...|] とする。
1 + reset (fun () -> 10 + (shift k -> k (k 100)));;このコードでは k は 10 + [・] なので、 1 + (10 + (10 + 100)) となり、 121 が得られる。
これをラムダ計算 + shift/resetで書き直すと、
add1 <add10 (Sx.x (x 100))>
となる。
これをCPS変換するが、より小さな例から始めるため、まずは <add10 (Sx.x (x 100))> をCPS変換する。
[|<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)))・・・(3)
(3)を(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)・・・(4)
となる。
この状態で x の置き換えを行うと x が2か所にあるため、コード量が増えるのでここでは置き換えずにおいておくことにする。
(4)はCPS変換後の式のため、結果を得るためには継続として id を渡したものを簡約すればよい(継続の引数に結果が入ってくるため、それを全体の結果として返すようにする)。
簡約規則は下記の通り。
v1 t2 ↝ v1 t2' (t2 ↝ t2'の場合)
t1 t2 ↝ t1' t2 (t1 ↝ t1'の場合)
(λx.t1) v2 ↝ [x ↦ v2]t1
また、 λv.v を id と表記し、簡約結果をシンプルにするために id t1 は即座に t1 に簡約することとする。
(λ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・・・(5)
↝ (λ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
本当にCPS変換したかったのは、 add1 <add10 (Sx.x (x 100))> だった。
これをCPS変換してみる。
[|add1 <add10 (Sx.x (x 100))>|]
app1 -> λk0.[|<add10 (Sx.x (x 100))>|] (λa0.k0 (add1 a0))
~~~~~~~~~~~~~~~~~~~~~~~~~~(6)
(6)をCPS変換すると(4)になるため、全体としては下記のようになる。
λ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))・・・(7)
(7)を 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))
↝ (λa0.id (add1 a0))
((λ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 (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)
add1 の後ろ側は(5)と同じ形になっているので、(5)を簡約した結果である 120 に置き換える。
add1 120
↝ 121
これは、 1 + reset (fun () -> 10 + (shift k -> k (k 100)));; の結果と一致する。
CPS変換された結果をOchaCamlコードで表現してみて、部分的に簡約して簡略化してみる。
まずは、単に構文を書き換える。
(λa.t) = (fun a -> t)
(λa.λb.t) = (fun a b -> t)
また、 let id x = x;; を前提とする。
(fun k0 ->
(fun k1 ->
k1 (
(fun k2 ->
(fun k3 ->
(fun k4 ->
(fun k5 -> k5 (fun a k' -> k' (k3 a)))
(fun f1 ->
(fun k6 ->
(fun k7 -> k7 (fun a k' -> k' (k3 a)))
(fun f2 -> (fun k8 -> k8 100) (fun a3 -> f2 a3 k6))
)
(fun a2 -> f1 a2 k4)
)
)
id
)
(fun a1 -> k2 (10 + a1))
) id
)
) (fun a0 -> k0 (1 + a0))
) id;;この状態で実行しても、121と計算できる(し、当然以降の各ステップのどのコードも実行結果は121になる)。
まずは (fun x -> y) id を展開し、 id x を x にする。
(fun k1 ->
k1 (
(fun k3 ->
(fun k5 -> k5 (fun a k' -> k' (k3 a)))
(fun f1 ->
(fun k6 ->
(fun k7 -> k7 (fun a k' -> k' (k3 a)))
(fun f2 -> (fun k8 -> k8 100) (fun a3 -> f2 a3 k6))
)
(fun a2 -> f1 a2 id)
)
)
(fun a1 -> 10 + a1)
)
) (fun a0 -> 1 + a0);;これだけでも大分すっきりとはしたが、まだ冗長な部分がある。
(fun k -> k x) y を展開し、 y x にする。
(fun a0 -> 1 + a0) (
(fun k3 ->
(fun f1 ->
(fun k6 ->
(fun f2 -> (fun a3 -> f2 a3 k6) 100)
(fun a k' -> k' (k3 a))
)
(fun a2 -> f1 a2 id)
) (fun a k' -> k' (k3 a))
)
(fun a1 -> 10 + a1)
);;次に、 f1 を引数に持つラムダ式と f2 を引数に持つラムダ式を展開する。
(fun a0 -> 1 + a0) (
(fun k3 ->
(fun k6 ->
(fun a3 -> (fun a k' -> k' (k3 a)) a3 k6) 100
)
(fun a2 -> (fun a k' -> k' (k3 a)) a2 id)
)
(fun a1 -> 10 + a1)
);;ここまでで、 a を引数に持つラムダ式と a0 を引数に持つラムダ式と a3 を引数に持つラムダ計算が簡約しやすい形になったので展開する。
1 + (
(fun k3 ->
(fun k6 ->
(fun k' -> k' (k3 100)) k6
)
(fun a2 -> (fun k' -> k' (k3 a2)) id)
)
(fun a1 -> 10 + a1)
);;k6 を引数に持つラムダ式を展開する。
1 + (
(fun k3 ->
(fun k' -> k' (k3 100))
(fun a2 -> (fun k' -> k' (k3 a2)) id)
)
(fun a1 -> 10 + a1)
);;ここまでで、かなり見通しの良いコードになった。
1 + ...はresetの外(resetの結果を待ち受ける継続)に対応。k3と2つのk'はshiftをCPS変換した結果導入されたもの。k' (k3 100)はshiftの中のラムダ式に対応。k' (k3 a2)もだが、少しわかりにくいか・・・？fun a1 -> 10 + a1はshiftで切り取られる継続に対応。
さらに、残っている id を消す。
1 + (
(fun k3 ->
(fun k' -> k' (k3 100))
(fun a2 -> k3 a2)
)
(fun a1 -> 10 + a1)
);;k' を引数に持つラムダ式を展開する。
1 + (
(fun k3 ->
(fun a2 -> k3 a2) (k3 100)
)
(fun a1 -> 10 + a1)
);;a2 を引数に持つラムダ式を展開する。
1 + (
(fun k3 -> k3 (k3 100))
(fun a1 -> 10 + a1)
);;ここまでくると、元のプログラムと比較しやすくなっている。
(* 元のプログラム *)
1 + reset (fun () -> 10 + (shift k -> k (k 100)));;fun a1 -> 10 + a1 は shift によって切り取られる継続そのものだし、
fun k3 -> k3 (k3 100) は shift の中身そのものとなっている。
またこのプログラムは、元のプログラムを評価文脈付きの簡約規則を使って部分的に簡約したものと同じ形になる。
reset (fun () -> E[shift (fun k -> expr)]) =
reset (fun () ->
(fun k -> expr)
(fun v -> reset (fun () -> E[v])))・・・shift
reset (fun () -> v) = v ・・・reset
1 + reset (fun () -> 10 + shift (fun k -> k (k 100)))
shift -> 1 + reset (fun () -> (fun k -> k (k 100)) (fun v -> reset (fun () -> 10 + v)))ここで、外側の reset の中の式にも内側の reset の式の中にも shift が現れないため、強引だが値とみなして簡約すると、
1 + reset (fun () -> (fun k -> k (k 100)) (fun v -> reset (fun () -> 10 + v)))
reset -> 1 + ((fun k -> k (k 100)) (fun v -> reset (fun () -> 10 + v)))
reset -> 1 + ((fun k -> k (k 100)) (fun v -> 10 + v))となる。 CPS変換したものを恣意的に簡約したものと比べてみる。
(* CPS変換したものを簡約 *)
1 + (
(fun k3 -> k3 (k3 100))
(fun a1 -> 10 + a1)
);;
(* 評価文脈付きの簡約規則で簡約 *)
1 + (
(fun k -> k (k 100))
(fun v -> 10 + v)
);;このように、どちらを使っても同じようなプログラムに変換された。