call/ccは副作用らしい

CS

ちょっと前に参考[1]で知ったのだが、Schemeのcall/ccには副作用が生じるらしい。ここ1年間で最も使った言語はたぶんSchemeだけれど(というかまともにプログラミングしてないのだが)、未だにcall/ccは使ったことがない。そもそも使い時が分からないし、継続というものが分からない。ちなみにマクロもまともに使えない。なので、Schemeを使っているとはおこがましくて大きな声では言えないのだ。
そんなわけで、call/ccが副作用だろうがそうじゃなかろうが別に関係ないのだが、ちょっと考えてみた。
参考[1]にある例。

> (define x (call-with-current-continuation call-with-current-continuation))
> x
#<system continuation>
> (x 123)
> x
123

うーむ、これは面白い。しかしまったく分からん。というか"call-with-current-continuation"は名前は知っているが実際にどんなものか知らなかったことに気付く。R5RSで調べると"call/cc"("call-with-current-continuation"は長い！)は1引数の手続きを引数とする手続きらしい。で、現在の継続をその引数の手続きに渡す。ということは、xは最初のcall/ccの継続kに二番目のcall/ccの継続k'を適用したものになるわけだ。ここで、継続kと継続k'がどんなものか分かれば良いのだが、ちょっと分からないので、結果から妄想すると、どうやらどちらの継続も変数xに代入を行うもののようだ。たぶん、環境とかストアを変更するような継続なのだろう。この辺の知識は武市先生の「プログラミング言語」*1で勉強したのでなんとなく想像できる。あっているかは知らんが。昨日の「計算モデルの基礎理論」もそうだが、この本も絶版。岩波さん、どうにかしてください。ちなみに、この本も運よく手に入れることができた。某先生に多謝。
話がそれた。閑話休題というやつだ。「閑話休題」というと、私はマンガ版パトレイバーでこの用語を知ったので、正しい使い方には違和感があるのだ。汚名は挽回するものだと思っているΖガンダムファン、サイボーグ009ファンと同じ感じである。
話がそれた。継続が想像通りだとすると、

(define x (call/cc (lambda (x) x)))

も同じようになると考えられる。
で、実際に試した結果。

gosh> (define x (call/cc (lambda (x) x)))
x
gosh> x
#<subr continuation>
gosh> (x 123)
x
gosh> x
123

確かに、同じだ。
ところで、継続ってどうやって決まるのだろう。普通に考えれば実装依存になりそうなのだが。と、ここでピンと来ましたですよ。R5RSに書いてあるんじゃねと。で、見てみたら、やはりあった。「7.2 形式的意味論」に書いてあります。まあ、普通に考えればR5RSに書いてあるって分かるよなあ。そうじゃなくちゃ"call/cc"なんて使えない。
しばらくその部分を読んでみたのだが、全然わからん。どうやらSchemeでは手続き呼出し時の評価順は決まっていないらしい。これは注意書きといった感じで書いてあったので分かったのであって、意味関数から読み取ったわけではない。
ああ、ちょっと勘違いしてた。手続き呼出しの継続は、その手続き式(？)の手続きの評価したときの継続ではなくて、手続きが適用されるときの継続か。つまり、"(proc arg)"の継続は"proc"を評価したときの継続ではなくて、"arg"を"proc"に適用したときの継続というわけか。R5RSの意味関数で言えばε[(E0 E*)]に渡される継続が"(proc arg)"の継続になる。なぜなら、補助関数applicateにそのまま渡されているから。あたりまえといえばあたりまえだなあ。ちょっとどころではなく結構な勘違いだったようだ。
なるほど。これで、

(define x (call/cc call/cc))

の最初のcall/ccと二番目のcall/ccの継続が等しいことが分かった、ような気がする。さすがに意味関数、補助関数もだが、は分からないところが多いので言い切ることできないなあ。
分からないところを想像し、あまり重要でなさそうなところを省略すると"(call/cc call/cc)"は次のようになりそうな気がするのですよ。

applicate cwcc cwcc k
-> cwcc cwcc k = applicate cwcc λe*k'.ke* k
-> cwcc λe*k'.ke* k = applicate λe*k'.ke* λe*k'.ke* k
-> k(λek'.ke)

自身はないが上の例ではこれで上手く行きそう。"define"の働きが分からないのでなんとも言えないが。ところで、R5RSの形式的意味論のところには"define"について書かれていない気がするのだが、なぜなのだろう。とりあえず、参考[1]によると『Schemeではトップレベルのdefine ≒ set!という定義』らしい。それなら問題なさげだが、正確な定義とかはないのだろうか。R5RSをちゃんと読んでみるかな。
let式、というかlambda式だが、は意味関数により意味が与えられているので、こっちで考えてみよう。うむ、また分からなくなってきたぞ。一度分からなくなると、今までのも合っているのかどうか不安になってくるな。明日以降、時間がある時にもう少し考えてみよう。

*1:

岩波講座 ソフトウェア科学〈〔基礎〕4〉プログラミング言語

岩波講座 ソフトウェア科学〈〔基礎〕4〉プログラミング言語