aboutme:114758

call/cc を知る。プログラムの例外処理に関してある記事を読み、そういえば、背理法は例外処理にあたると恩師から聴いていたのを思い出しググってみた。以前に call/cc という考え方に触れたことがあったはずだが、そのときは関心を持たなかった…。

JRF 2009年12月 5日 (土) Tweet

関心を持つようになったのは最近↓に書いた＞ その者の中の乙女が死んだとき、その者が与えた夢の欠片が彼女を抱く、すると、その乙女の夢の中で、乙女は夢を抱きしめて蘇える。＜に call/cc の考え方が似ていると感じたからかもしれない。

《JRFのひとこと:「未来の子供」…: アバウトミー : @nifty》
http://jrf.aboutme.jp/user_statuses/show/113999

JRF 2009年12月05日 6100

call/cc というのは call with current-continuation の略で、プログラム言語 Scheme などで「継続」と呼ばれるものを作るための機構である。応用として例外処理などを書ける。プログラムには関数を渡すことができるが、この関数としてなんと return を渡せるようにするのが、call/cc という機構であると考えていい。

JRF 2009年12月05日 1517

形式的には、ある解釈の環境 E[] 下で、M という項が問題になっているとき E[M] と書くとすると、E[call/cc(M)] |-> E[M λz. A(E[z])]。この A は環境を固定化し、A が解釈されそうになると、その内に留めた環境に引き戻す効果を(だいたい)もつものである。

JRF 2009年12月05日 7807

call/cc を解釈するときの環境が E_0[] だとして、処理が進んで環境 E_1[] に進んでいる。でも、call/cc から返された継続が呼ばれたとき、E_1 までなったことを捨てて E_0 の続きに戻るという処理がなされる。つまり E_1 は「死んだ夢の世界」のように捨てられる。ただし、そのとき E_1 の環境から値を返すことができる。

……。

JRF 2009年12月05日 0704

背理法との関係は↓がおもしろかった。

《d.y.d.：Curry-Howard Isomorphism》
http://www.kmonos.net/wlog/61.html

その記事に次のような call/cc を使った例がある。

callcc (
fun (k: (a, a->⊥) sum -> ⊥) ->
InRight (fun (x:a) -> k (InLeft x)))
)

この全体の型は (a,a->⊥) sum になる。つまり、「a か not a」という定理になる。

JRF 2009年12月05日 9642

上を使うプログラムとしては例えば次のように受ける。

program M {
var j = callcc(…上のもの…)

var b = switch(j){
case InRight f -> f:a->⊥ についての処理。
case InLeft x -> x:a についての処理。
}
…
}

j の中身を見ると、InRight(…) というのが来ているので、switch の中では、「f:a->⊥ についての処理」がまず続くが、あるとき、f に何か(d:a)が代入されると、そこは f(d):⊥となって、無限ループに陥ることに相当する。

JRF 2009年12月05日 6012

ただし、「継続」のおもしろいところは＞継続に値を突っ込んだらその継続先にジャンプしてしまってその場所には返ってこない＜ところで、こんどは j の奥にあったところの InLeft d となって switch 分の中に「蘇え」り、何ごともなかったかのように「x:a についての処理」を進める。

さて、大事なことは j の段階では d:a があるなんてことは「知らない」ということ。

JRF 2009年12月05日 1766

……。

これを無理に「文学的」に表現してみると…。

JRF 2009年12月05日 3464

大魔王モモ(M)は、使いとしてやんちゃなジジ(j)を地上に送ります。ジジは料理店の店主バイデン(b)さんのところで働きます。バイデンさんはジジに珍宝である秘伝のスパイス(x:a)は今あるかと聞きます。ジジはそんなことは知りません。でも、夢でモモがそっとささやきました。「ないことにしてあなたが成長すれば、あなたの敵がきっとそれを発明してきます。その世界を苦しむというなら、あなたをそれが今あった世界に導きましょう。」

JRF 2009年12月05日 5087

ジジは「ない」と答えました。ジジはバイデンさんのところで働き続けました。するとモモが言っていたとおり、「敵」がそれ(d:a)を持ってきました。でも、今さら、それが手に入ってもどうすることもできません。そして、ジジは老い、きっと死んだのでしょう。

ジジは「ある」と答えて珍宝(d:a)を取り出しました。バイデンさんは大喜びです。「ライバル」がそれを見て悔しがっています。

JRF 2009年12月05日 8999

「でも、ジジがどうやってその珍宝を手に入れたのか誰も(ジジも)知らないのでした。」そう言って、「大魔王」モモは本を閉じました…とさ。

……。

これが自然で古典的な演繹というわけだ。

JRF 2009年12月05日 9874

なお、知ったばかりでプログラムも実際の処理系で試しておらず、間違っているかもしれません。誰か指摘してくれたらうれしいけど…その望みは薄いですが、もし、指摘があれば後日「まるまるナシにして」と追記するかもしれません。

JRF 2009年12月05日 8982

(最初に書いた「ある記事」は↓。)
《シーケント計算と例外処理コード - 檜山正幸のキマイラ飼育記》
http://d.hatena.ne.jp/m-hiyama/20091130/1259541758

「文学的」表現については↓が私の関連記事かな。
《シミュレーション・アーギュメントを論駁する》
http://jrf.cocolog-nifty.com/religion/2006/10/post.html

JRF 2009年12月05日 8418

シミュレーション・アーギュンメントや三囚人問題と関連するのか一つ前のひとことにも関連して、眠り姫問題というものがあるらしい。Yet Anotehr 変形三囚人問題というのを2008年03月08日あたりのひとことで紹介してます。
《眠り姫問題とは - はてなキーワード》
http://d.hatena.ne.jp/keyword/%CC%B2%A4%EA%C9%B1%CC%E4%C2%EA

JRF 2009年12月05日 2319

他に私の以下のカテゴリや記事もよければ読んでみてください。
《JRF の私見：雑記: 論理学》
http://jrf.cocolog-nifty.com/column/cat2934351/index.html
《呪術的オブジェクト指向用語訳》
http://jrf.cocolog-nifty.com/column/2006/03/post_17.html

JRF 2009年12月05日 9585