限定継続について勉強してみた

話題の限定継続についてこれで自習。意味論とか書いてあって難しそうだけど、とりあえず自分の分かる範囲で読み進める。ツッコミ歓迎です。

まずは、call/ccのsemantics。

$\llbracket\mbox{call/cc}\,E\rrbracket\rho = \lambda k.\llbracket E\rrbracket\rho(\lambda f.f(\lambda v.\lambda k'.k v) k)$

Eを評価すると1引数関数fになる。fは $\lambda v.\lambda k'.k v$ という関数に適用される。 $\lambda v.\lambda k'.k v$ は「引数を1つとり、それを(自分自身の継続k'を無視して)call/ccの継続kに引き渡す」関数。

たとえば、

(+ 1 (call/cc (lambda (cc) (+ 2 (cc 3)))))  ;=> 4

というコードでは、(lambda (x) (+ 1 x))がk、(lambda (x) (+ 2 x))がk'、ccが $\lambda v.\lambda k'.k v$ になる。semanticsの方がCPSで書かれているので引数の個数とかで多少違いはあるけど、だいたいこんなような感じ。注意する点はk'を無視してkを呼び出しているところで、上のコードでは(cc 3)の後に「2を足す」継続は捨てられて、「1を足す」継続に制御が渡る。

次にresetのsemantics。

$\llbracket\mbox{reset}\,E\rrbracket\rho = \lambda k.k(\llbracket E\rrbracket\rho(\lambda v.v))$

resetは特に何もしない。Eを評価して返ってきた値を継続kに渡しているだけ。

そしてshift。

$\llbracket\mbox{shift}\,c\,M\rrbracket\rho = \lambda k.\llbracket M\rrbracket(\rho[c\mapsto\lambda v.\lambda k'.k'(k v)])(\lambda v.v)$

shiftは、環境 $\rho$ に束縛 $c\mapsto\lambda v.\lambda k'.k'(k v)$ を導入してMを評価する。cに束縛される関数 $\lambda v.\lambda k'.k'(k v)$ は、call/ccでfに渡される関数と似た形をしている。違うのは(k v)の後にk'が呼ばれる点。k'はcの呼び出し時点での継続だ。これにより、

(reset (cons 2 (shift c (cons 3 (c '())))))

は、(3 2)に評価される。つまり、(c '())が評価されると次に、resetからshiftの間に挟まれた継続(lambda (x) (cons 2 x))が実行され、その次に(c '())の継続(lambda (x) (cons 3 x))が実行される。さらに、resetも継続を持てば、最後にそれが実行される。

(cons 1 (reset (cons 2 (shift c (cons 3 (c '()))))))  ;=> (1 3 2)

また、cが呼び出されなければ継続は $\lambda v.v$ になるから、元々のshiftの継続kは捨てられることになる。

(cons 1 (reset (cons 2 (shift c '()))))  ;=> (1)

さて、ここまで見てきて限定継続の「限定」たる所以はだいたい分かったのだけれど、1つ疑問なのは、「なぜcに束縛される関数は $\lambda v.\lambda k'.(k v)$ ではなく、 $\lambda v.\lambda k'.k'(k v)$ なのか」という点。k'がなければ挙動が本当に「範囲を制限されたcall/cc」になるし、上で見たようなズタズタな制御にならずに済むように思えるのだけど。k'(k v)であることで何か利点があるんだろか？それとも理論的な理由によるんだろうか？謎です。

このあと、meta-continuationというのが出てきてshift/resetの実装の話に移ってくようだけど、まだよく分からないので続きはそのへんを理解してから。続かないかも。