aboutme:114758
call/cc を知る。プログラムの例外処理に関してある記事を読み、そういえば、背理法は例外処理にあたると恩師から聴いていたのを思い出しググってみた。以前に call/cc という考え方に触れたことがあったはずだが、そのときは関心を持たなかった…。
JRF 2009年12月 5日 (土)
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
トラックバック
他サイトなどからこの記事に自薦された関連記事(トラックバック)の一覧です。
感情はコントロールできるけれど、理性はコントロールできないからね…って、いや、しかし、ビョーキを経験した私には、理性と感情を共調させることができれば、その後、感情に理性が従うような設定を理性に律させることはできるという実感がある。... 続きを読む
受信: 2012-01-05 21:38:42 (JST)
関心を持つようになったのは最近↓に書いた> その者の中の乙女が死んだとき、その者が与えた夢の欠片が彼女を抱く、すると、その乙女の夢の中で、乙女は夢を抱きしめて蘇える。<に call/cc の考え方が似ていると感じたからかもしれない。
《JRFのひとこと:「未来の子供」…: アバウトミー : @nifty》
http://jrf.aboutme.jp/user_statuses/show/113999
JRF 2009年12月05日 6100