CPS変換まとめ
CPS変換の手法にもいろいろある．
前提として，λ式は以下のような構文で定義されているとする．
M, N ::= x | λx.M | M N
CPS(継続渡し形式)とは，計算が行われる順序を明示するために，ある式の計算結果を，残りの計算を表す継続（途中結果を受け取り，残りの計算を行う関数として表現できる）に次々と渡していくようなスタイルのλ式である．
上で定義したλ式では，計算はλ適用(M N)しかないので，CPSは適用の順序を明示的に示すようなλ式のスタイルということになる．
たとえば，(h ((g x) y))というλ式は，左から右へのcall-by-valueの評価戦略では，計算順序は以下のようになる．
(g x)を計算し，その結果t1とする．
(t1 y)を計算し，その結果をt2とする．
(h t2)を計算し，その結果を最終的な計算結果rとする．
以上の計算の流れをCPSで表すと，
((g x) λt1.((t1 y) λt2.((h t2) λr.r)
という感じになる．
PlotkinのCPS変換
まずは，PlotkinのCPS変換を以下に示す．
C[[x]] = λk.k x - (a) C[[λx.M]] = λk.k(λx.C[[M]]) - (b) C[[M N]] = λk.C[[M]](λm.C[[N]](λn.(m n) k)) - (c)
上の変換で何をやっているかというと，あらゆるλ式を，「継続kをもらって，その式自身の評価結果をkに渡す」という形式に変換している．たとえば，xやλx.Mは値なのでこれ以上評価できないので，変換結果は単に受け取った継続kにそれ自身をそのまま渡す，という形式に変換される．((a)と(b))
問題は(c)のλ適用(M N)の変換である．
そもそも，(M N)の計算の順序は次のようになる．
(1) 部分式Mを評価し，その結果をmとする．
(2) 部分式Nを評価し，その結果をnとする．
(3) (m n)の評価結果を残りの継続に渡す．
(1)について考えると，部分式MのCPS変換結果C［［M］］は，継続を受け取ってMを評価し，その結果を継続に渡すような関数に変換されているので，次のような形で表せるだろう．
C［［M］］ (λm.(2)から先の計算)
同様に(2)について考えると，
C［［N］］(λn.(3)から先の計算)
となる．(3)は，それ以降の継続をkとすると
(m n) (λr.k r)
となる．以上をまとめると，
C［［M N］］ = λk.C［［M］］(λm.C［［N］］(λn.(m n) (λr.k r)))
となる．上記のλr.k rの部分はη簡約によりkとなるので，結局(c)のようになる．
問題点
残念なことに，Plotkin方式の変換では，出力されるλ式がえらく冗長になってしまう．たとえば，
λf.λx.λy.((f y) x)
は，
λk.(k λf.λk.(k λx.λk.(k λy.λk.(λk.(λk.(k f) λm.(λk.(k y) λn.((m n) k))) λm.(λk.(k x) λn.((m n) k))))))
のような長いλ式に変換されてしまう．この式をよくみると，部分的に簡約可能な式があることに気がつく．
たとえば，以下のように簡約していける．
λk.(k λf.λk.(k λx.λk.(k λy.λk.(λk.(λk.(k f) λm.(λk.(k y) λn.((m n) k))) λm.(λk.(k x) λn.((m n) k))))))
=>
λk.(k λf.λk.(k λx.λk.(k λy.λk.(λk.(λk.(k f) λm.(λk.(k y) λn.((m n) k))) λm.(λn.((m n) k) x)))))
=>...
λk.(k λf.λk.(k λx.λk.(k λy.λk.((f y) λm.((m x) k)))))
このように，変換後に改めてリダクションしてもいいけど，どうせなら一発でコンパクトな式へ変換したい．要するにone-passで簡約化されたCPS式を出力してくれるような変換があると，いろいろな意味でありがたい．次に説明するDanvyのCPS変換はそういった変換の一つである．
DanvyのCPS変換
C[[x]] = Λк.кx C[[λx.M]] = Λк.к(λx.λk.C[[M]](Λm.k m)) C[[M N]] = Λк.C[[M]](Λm.C[[N]](Λn.(m n) (λa.кa))))
ここでは，CPS変換時に簡約化されるラムダ抽象を，通常のラムダ式と区別するために，大文字のΛで表記してある．
上で示したDanvyのCPS変換は，CPSのλ式を出力するのではなく，кを受け取るとCPSに変換されたλ式を出力する変換関数を出力する．кは何かというと，実はλ式を受け取ると，それを穴の空いたλ式に埋めたものを返すバックパッチ関数である．PlotkinとDanvyのCPS変換をともに関数とみたてて，その型を考えると，両者の違いがはっきりする．
C［［］］_plotkin : lambda -> lambda
C［［］］_danvy : lambda -> (lambda -> lambda) -> lambda
DanvyのCPS変換の導出
ここでは，PlotkinのCPS変換から出発して，Danvyの変換を導出していく．
戦略としては，CPS変換時に導入されるλ抽象（λkやλm,λn）のうち，常に簡約可能なものは変換時に簡約し，除去してしまえばよい．たとえば，...(λk.(k M) K)...のような部分は常に...(K M)...に簡約化できる．問題は，どうやったらそのような部分を特定するかである．
Plotkinの変換等式をよく見ると，変換結果は常にλk.Mの形をしていることがわかる．したがって，変換等式の右辺に現れるC［［...］］が，λ適用の左側に位置していれば（すなわち(C［［...］］X)のようになっていれば），変換時に簡約可能である．このことを念頭において，再びPlotkinの変換等式を見てみると，残念ながら以下の等式はそうなっていない．
C［［λx.M］］ = λk.k(λx.C［［M］］) - (b)
そこで，この等式を，意味を保ったまま，C［［M］］の位置がλ適用の側にくるように変形する．以下のようにη変換すればよい．
C［［λx.M］］ = λk.k(λx.λk.C［［M］］k) - (b')
この時点で，変換等式の右辺で導入されたλk，λm，λnをそれぞれΛк，Λm，Λnに置きかえてみると，以下のようになる．(λxはもともとのλ式に存在するので，Λxに置き換えずにそのままにしておく)
C[[x]] = Λк.к x - (a') C[[λx.M]] = Λк.к(λx.λk.C[[M]] k) - (b'') C[[M N]] = Λк.C[[M]](Λm.C[[N]](Λn.(m n) к)) - (c')
改めて，上の変換等式をみてみると，すべてのC［［M］］の位置はめでたくΛ適用の左側に来るようになった．これで変換時にΛ簡約ができるようになったかというと，まだいくつか問題が残っていることに気がつく．
まず，C［［M］］の引数に注意すると，(c')ではΛ式が引数になっているが，(b'')では引数がkになっている．kはλ式における単なる変数なので，このままでは，変換時，кに適用する時に失敗してしまう．そこで，再びη変換を使って，(b'')を以下のように変形してやる．
C「「λx.M］］ = Λк.к(λx.λk.C［［M］］(Λm.k m)) - (b''')
残る問題はкの出現位置だ．(a')と(b''')では，кは（変換時の）Λ適用の左に位置しているが，(c')は（変換後のλ式における）λ適用の右の位置に来ている．そこで，(c')を変形してΛ適用の左側にくるようにしよう．例によってη変換すればよい．
C［［M N］］ = Λк.C［［M］］(Λm.C［［N］］(Λn.(m n) (λa.кa))) - (c'')
以上，DanvyのCPS変換を導出することができた．
Sabry&WadlerのCPS変換
DanvyのCPS変換関数は，one-passではあったが，その型（lambda->(lambda->lambda)->lambda）を見ればわかるように高階（higher-order）関数であった．1階(first-order)の関数として，すなわち関数自身を引数に取ったり，関数を値として返したりせずに，同様の変換を実現できないだろうか？
以下に示すSabry&Wadlerの変換はそのような要求を満たす変換方式である．
// V, Wはxかλx.Mの形をしたλ式 C[[V]]K = K T[[V]] C[[V W]]K = (T[[V]] T[[W]]) K C[[V N]]K = C[[N]](λn.C[[V n]]K) C[[M N]]K = C[[M]](λm.C[[m N]]K) // 補助関数T[[]]を定義 T[[x]] = x T[[λx.M]] = λx.λk.C[[M]]k
C［［］］_sabry : lambda * lambda -> lambdaであり，確かに1階の関数になっている．
SabryのCPS変換の導出
ここでも，PlotkinのCPS変換から出発して，Sabryの変換を導出していくことにする．基本的な方針は，Danvyでやったのと同じで，β-redexが導入されないような変換を検討していく．このとき，高階関数が入り込まないように注意する．
まずは，以下の変換規則を出発点にする．
C[[x]] = λk.k x - (a) C[[λx.M]] = λk.k(λx.λk.C[[M]] k) - (b') C[[M N]] = λk.C[[M]](λm.C[[N]](λn.(m n) k)) - (c)
C［［...］］は常にλk.Mの形に変換され，かつ，変換規則の右辺に現れるC［［］］は常にλ適用の左に位置するので，このλkは変換時にβ簡約できる．ΛKを用いて以下のように変形できる．
C[[x]] = ΛK.K x C[[λx.M]] = ΛK.K (λx.λk.C[[M]] k) C[[M N]] = ΛK.C[[M]](λm.C[[N]](λn.(m n) K))
このまま進めていってもよいのだが，C［［］］］をアンカリー化してやると，以下のように書きなおせる．
C[[x]]K = K x C[[λx.M]]K = K (λx.λk.C[[M]] k) C[[M N]]K = C[[M]](λm.C[[N]](λn.(m n) K))
上記の変換規則には，まだ余計なβ-redexが導入される可能性が残っている．λmとλnの部分である．たとえば，C［［x N］］k = (λm.C［［N］］(λn.(m n) k)) xとなるが，これは，C［［N］］(λn.(x n) k)にβ簡約できる．要するに，(M N)の形によって変換規則を場合分けしてやれば，このようなβ-redexを取り除くことができる．
まず，場合分けがややこしくならないように，以下のように補助変換規則T［［］］を導入して，変換規則を書きかえる．
C[[V]]K = K T[[V]] // Vはxからλx.Mの形 C[[M N]]K = C[[M]](λm.C[[N]](λn.(m n) K)) T[[x]] = x T[[λx.M]] = λx.λk.C[[M]] k
まず，C［［V W］］の場合を考える．変換規則にしたがって変形していくと，
C［［V W］］K
= C［［V］］
= (λm.C［［W］］(λn.(m n) K)) T［［V］］
= (λm.(λn.(m n) K) T［［W］］) T［［V］］
となる．これは，β簡約できるので，結局，
C[[V W]]K = (T[[V]] T[[W]]) K -- (*)
という規則になる．次に，C［［V N］］の場合である．
C［［V N］］K
= C［［V］］
= (λm.C［［N］］(λn.(m n) K)) T［［V］］
→C［［N］］(λn.(T［［V］］n) K)
となるので，結局，
C[[V N]]K = C[[N]](λn.(T[[V]] n) K) -- (**)
という規則が得られる．さらに，上記の規則において，nは単なる変数（値）なので，さきほどの変換規則(*)を左向きに適用することで，以下が得られる．
C[[V N]]K = C[[N]](λn.C[[V n]] K)
最後に，C［［M N］］K=C［［M］］(λm.C［［N］］(λn.(m n) K))という最も一般的なケースであるが，これも，変換規則(**)を左向きに適用することで以下が得られることに気がつく．
C［［M］］(λm.C［［m N］］K)
したがって，最終的には以下の変換規則が得られる．
C[[M N]]K = C[[M]](λm.C[[m N]] K)
以上，SabryのCPS変換も導出することができた．
参考文献
- "Representing Control: A Study of the CPS Transformation (1992)", Oliver Danvy, Andrzej Filinski
- "A Reflection on Call-by-Value (1996)", Amr Sabry, Philip Wadler
- "A first-order one-pass CPS transformation (2003)", Olivier Danvy, Lasse R. Nielsen
- "Essentials of Programming Languages -- 2nd ed. (2001)", Daniel P. Friedman, Mitchell Wand, Christopher T. Haynes
