Derive Your Dreams
Twitter: @kinaba
13:33 08/06/29
RSS of kmonos/wlog moved!
http://www.kmonos.net/wlog/index.rdf
いや、移動したのは15ヶ月前なので、すでにご存じの方は華麗にスルーしてください。
「ここのRSSが文字化けしてるよー」という方だけ、↑に登録変更していただけると、
直るかと思います。お手数おかけしてスミマセン。定期的に「文字化けってる」という
指摘を見かけるので再度ブロードキャストです。こう、辛辣な評議会とかで怒られそうですけど、
諸般の事情により古い方からリダイレクトかけるの難しいらしいのだよね…
それはそうと、昨日の記事に追記しました。
10:26 08/06/28
Logic ∩ CS
検索してたらたまたまヒットした
"On the Unusual Effectiveness of Logic in Computer Science"
を読んでました。超訳すると、なんだろ、「コンピュータ科学での論理学の便利さは異常」。
序文によると「自然科学での数学の便利さは変態的（褒め言葉）」みたいな伝統
がガリレオの昔からあるらしく、それの Computer Science & Logic 版行ってみよう！という企画のようです。
コンピュータ科学の中から論理論理してる 5 つのトピックを取り上げて語っています。
1 つめは、記述的計算量（…でいいのかな標準的な訳は。Descriptive Complexity）。
計算量ってのはいわゆる O(N logN) とか P とか NP とか PSPACE とか、そういうのです。
問題を解くプログラムがどのくらいの時間やメモリ消費で走るかの分類ですね。
これが実は、これとは別の「どんな論理記号があれば記述できる問題か？」という分類と
わりとうまく一致するよ、というのが Descriptive Complexity のお話。
例えば、FO+LFP（一回述語論理＋最小不動点演算子）の範囲の論理記号で書かれた問題は絶対に時間計算量 P で解けるし、
逆に P で解ける問題は必ず FO+LFP で仕様を書き下すことができることがわかっています。
SO∃（二階述語論理、ただし二階の量化子は∃を一番外で使うに限る）で書ける問題は NP で解けるし、
NP で解ける問題は SO∃ で書ける。
ある意味、「Pっぽい問題ってどういう問題？」や「NPっぽい問題って（以下略」などの疑問に迫る分野です。
2 つめは Database Query。
要するに要しすぎると SQL の話。
この辺の話は Logic 的には
有限モデル論 (Finite Model Theory)
とかそういう方面だと思います。
3 つめは型理論（Type Theory）。
昔いきおいで書いた Curry-Howard Isomorphism について語る日記
がありますが、要するにそういう方向の話です。"型"と"その型のプログラム"の関係は
"命題"と"証明" の関係と鏡に映したように一致していて、型システムに関する基礎理論とはすなわち
証明システムに関する基礎理論であり、逆向きでもあり。
Logic 的には
Proof Theory
になるのかな。
4 つめの Reasoning about Knowledge
…は私がまったく勉強したことがないので解説があやふやになりますが、
「「「Aさんはある情報を知っている」ということをBさんは知っている」という情報は全員が知っている」
みたいな、"知っている" に関する論理・推論らしい。分散処理プロトコルで、
「「全体に情報が行き渡った」ことを全ノードが把握した」ことを知った時点で各ノードが処理を進める的な
同期・協調をする話があるらしいですよ。
5 つめはプログラムの検証（Automated Verification）。
要するにモデル検査。モデル検査では仕様を、時相論理（Temporal Logic）で記述することが多いです。
これは例えば「"次の"瞬間も○○は必ず成り立っている」や「△△になる"までは"□□である」、あるいは
「"いつかは"必ず☆☆状態になる」「"永遠に"変な状態にならない」のように時間的な関係を考えられるのが
特徴の論理です。プログラムが指定された仕様に関して正しいかどうかを、
この時相論理の性質をもとに、いかに効率的に判定するかが一つのポイント。
この辺りは
Modal Logic
と総称される分野でしょうか。
命題○○に対して、and,or,not のような単なる真偽値の組み合わせではない、
○○"を知っている"、○○"な可能性がある"、"次の瞬間は"○○、
などの修飾を考える種類の論理学です。
追記
omoさんによる、元ネタの 数学＠自然科学バージョンの紹介と序説の和訳。
それです！ Logic in CS の最初の "here"
にある論文でも参照されてました。
もいっちょ追記。忘れてた。
Cryoliteさんの指摘
で思い出したのですが、4つめの「知っている」に関する論理ってのは要するに
"Alloyで知識論理を使って論理パズルを解く" にあるようなパズルの基礎になってる論理ですね。
17:09 08/06/23
ICFP Contest
shinh さんが mame さんと言えば
hogelog さんと対消滅とかするんじゃないか とか書いておられたけど、そういえばなんか本当に
twitterのhogelogさんの写真が僕にはいまだにmameに見える
のであった。さらに最近のhogelogさんといえばGCでありGCといえばガベコレページの遠藤さんであり
遠藤といえばmameなのでもう頭の中が大変なことに。
本題
そして Endo さんといえば（去年の）ICFP コンテストということで、改めて紹介を書いてみます。
最近それ系の検索でうちに辿り着かれる方がかなり増えているので、
レスポンスという意味も込めて。
ICFP (International Conference on Functional Programming) という関数型プログラミングの国際学会が
主催しているコンテストで、毎年１回、72時間勝負で開催されています。今年は日本時間で言うと
7/12 (土) AM 4:00 スタートで 7/15 (火) AM 4:00 に終了。
土日だけ参加するもよし、月曜の授業さぼったり有給取ったりで全力を注ぎ込むも良し！
事前登録みたいなのは不要なので、実際始まってみて面白そうだったら手を出してみる、というのもあり。
それと今年は注意書きがないので、おそらく、１人でやるのも何十人でチーム組むのもお構いなしでしょう。
7/4追記 ルール出ました５人までだそうです！
使うプログラミング言語もなんでもＯＫです。というか、「キミの好きな言語を存分に使って愛を示せっ！」
という趣旨のコンテストです、たぶん。もちろん ICFP なので関数型言語好きーな参加者が結構多いですし、
一方で逆に私みたいに関数型言語野郎どもをヘコませてやりたい的な人もいますし、そういうのどうでもいいぜ
祭りだわっしょいって人も多数。
どういうことをやるコンテストかというと、これは 年によって全然違う
ので始まってみないとわかりません。これまでの概略が
cpoucet さんによる紹介記事
に素晴らしくまとまってます。2005 年までは、
「荷物運びロボット」や「泥警の泥棒＆警官ズ」のようなゲームのAIを書け、という問題だったり、
専用言語で3Dシーンの仕様が与えられるのでそれを解釈してレイトレースしろ、というような言語処理的要素の入った
問題だったり、あるいはアリの群れにエサを取らせるゲーム（アリの思考ルーチンはもの凄い低級言語なので、
サクッとDSLやコンパイラを書いて自分の戦略をアリ言語に落とす環境を整えて戦う）という合わせ技だったり。
ゲームの思考ルーチンを書いたり言語処理系を書いたりするワンテーマ、というのが主流でした。
2006年、2007年は毛色が変わって、主催者側が異様な気合いの入ったシステムを用意してきて、
「システム内にある関数型言語や言語処理をネタにしたパズルを（プログラミングによって）たくさん解いたチームが勝ち」
みたいな感じになりました。そのシステム自体怪しげな独自マシン語で書かれているのでまず自分でVMを作る
とこから始めなくてはいけなかったり。
終了後、2007年のVMを高速に実現できるデータ構造を実装してライブラリ化するブーム
（e.g., Ruby,
Java）
が起きるなどしてました。当時の雰囲気は
ICFP contest 2007 感想リンク集
とかでわかります。
ただ、上記の cpoucet さんも書いておられるように、今年は 2005 年以前の雰囲気に戻りそうな感じですね。
まとめ
みんな 7/12, 13 の週末は予定空けとくように！！
17:20 08/06/19
OMeta
水島さん 曰く
"k.inaba さんの考えているのって、先日聞いた OMeta に近い気がするけど、どうなんだろ。"
ということで、OMeta をチェック中。
前のPEPMの PEGで左再帰の話
経由で論文は読んでたはずなんですが、「言語を作るための言語」という視点で Introduction
が書かれてたのでその時は全然ピンと来てませんでした。
そうか、
PEGs operate on ... only ... characters.
... OMeta operates on arbitrary kinds of data ...
とか書いてある。
OMeta/JS なら単に「オブジェクト列に対するPEG的パターンマッチで拡張されたJavaScript」と思えばいいし
PyMeta なら「同じく Python」と思えばいいのか！そうかその通りだ！頭の中で色々つながりました！
うああなんでそういう視点で見てなかったんだろう俺。
DSLとかメタ言語とかそんなめっちゃどうでもいいこと（言い過ぎ）に使われてる場合じゃないですよ OMeta さん。
まだ論文見てるだけなんですが、「ネストしたリストに対するネストしたパターン」が書けるのは素晴らしいとして、
「任意のオブジェクトを Scala の unapplySeq みたいなのによってリストとして"見せた"物体でネストした
構造」に対するパターンとか書けるのかな、これ。無くても JS 版なら手を加えるのも楽そうだな。
水島さんの OMeta ブームは
こちらの発表
発なのか。すごい！ナイス！
22:22 08/06/17
深遠の道
クリアった → nana25.rpl。
一番の見せ場は７９Ｆですかね。[魂] 印は他の合成が完璧に整ってないとスリル満点すぎなことがわかりました。
面白かった。序盤の敵の強くなり方が緩やかなのと、モンハウが物凄く多いのとで、確実に十分な武器防具が整う
バランス。かなり運要素少なめでいい感じなのではないかと思う。
これ、オオイカリパッチとかじゃなくてモンハウゼロパッチとかにして難易度あげるのも面白そう。
13:51 08/06/17
ぱたーん☆まっち
パターンマッチ的な物の未来を考える、というか主に願望を垂れ流します
（see also: NyaRuRuさん、
きむら(K)さん）。
リンク先でも話題にあがっているように、パターンマッチの使い勝手を考える上で
正規表現というのは近い位置にいるような気がするので、意図的にその辺りごちゃまぜに考えます。
-
とりあえず、文字列以外のリストも正規表現で処理したいということは自分の場合本気で結構あるので
（日記に書いたのだと PQ Tree や
構文解析の話 ‐ "毎回スタックを覗く感じの実装"
は非終端記号+構文木列スタックを正規表現で覗き込みたい ‐ など）、
その辺り巧く統合されて正規表現でできることはパターンマッチでできて逆もまた可、ってなると楽しい。
-
あるいは。
各種 LL の多重/アンパック/リスト代入は、私の感覚では、物凄く限定された形のパターンマッチなんですが、
Haskell や ML のようなフルのパターンマッチまで行かなくても、なにかもう一声欲しいよなーと思うことがあって、
そんなに大革命でなくても、今の言語に対するこのくらいの拡張でも便利なのでは…という消極的拡張。
if a.size >= 2 then
x = a[0]
y = a[1]
...
end
よりも
if a.size >= 2 then
x,y,* = a
...
end
の方が感覚的には500倍くらいわかりやすくて、
if x,y,* = a then
...
end # 的な何かそういったもの
さらにこう書けたらもう500倍くらいわかりやすいなーと。
正規表現って文字列のパターンを視覚的にわかりやすく表現する記法で、
それを使って、「そのパターンにマッチするかどうか調べられる」と同時に
「マッチする部分を取り出せる」という二つの機能を実現しているわけで、
多重代入は今のところ「取り出す」専用だけど「取り出せるかどうか調べる」も兼ねたい。
（※今のところ1番目より2番目は圧倒的に遅いので、そもそもこういう風に使うように
できていないわけですけど、そこを「こういう風に使いたい」という辺りも含めて）
（※そういえば、"パターン"がここで書いた二つの役目を兼ねてるのって別に必然じゃないよね
分離して考えることもできるんじゃない？みたいな論文を見たことがある気がする）
-
また積極的主張に戻る。
いやこれは私が色々使い方間違ってるだけな気がするんですが、たまにこういう正規表現書くはめになって
mystr.scan( /(aaa)|(aab)|(abc)/ ) do
case
when $1 ...
when $2 ...
when $3 ...
end
end
正規表現に括弧が増えるのが面倒くさい！あと、aaa の代わりに中で () 使うようなちょっと複雑な正規表現
が入ると、もう $1 の次が $3 なのか $4 なのか中身によって変わってしまって大変なことに！ …
などなどの理由で
mystr.scan do-case
when /aaa/ ...
when /aab/ ...
when /abc/ ...
end # 的な何かそういったもの
こういう風に書きたいなあと妄想してしまうことがよくあります。たぶん、「ブロック」を first-class
のオブジェクトとして扱える言語がループ等の制御構造を自由自在に作り出せるのと同じように、
「パターン」を first-class のオブジェクトとして扱える言語なら、こういう、ユーザー定義のパターンマッチ
制御構造みたいなのを書けるであろうなあ、というアレコレ。
これに類することができる文字列解析器（Semantic Action がつけられるヤツなら基本OKそう）や、
正規表現用のツールの存在は知っていますが、これもやっぱり、文字列に限らず「データ構造」に対する「パターン」
のユーザー定義の自由な「制御」、っていう枠組みにまで広げた方が便利だと思うんですよ。
なんか正規表現の話しかしてないな。なんでだろ。
「列」に対するパターンマッチの機能以外は、
Extractor (Scala) とか
[PPT] Active Pattern (F#) とか
View Pattern (Haskell) とか
で任意の抽象データ型に好きなだけパターンマッチできるようになった時点で、私的にはかなり満足
できちゃってるんですよね、たぶん。あんんまり話を混ぜない方がよかった気がしてきた。まあいいや。
みんなで混乱しましょう。
「列」に対するパターンという話で行くと、C++ の STL でいう「IteratorやRange」と「Algorithm」
の間にある、今だと「PredicateやFunction」のレイヤが何か「パターン」によっててもう少し構造化されうるんじゃ
ないかという適当な感覚があって、その辺適当にこうなんとか。
08:54 08/06/12
SIGMOD/PODS
リプレイ nana7.rpl 再生できるのは素晴らしいとしか言いようがないな。
20F, 48F 辺りどうするのが正解なのか検討会とか開きたい。
しかしこれ、一手でモンハウ解決できるようなアイテム（身代／目潰／やりすごし etc）は
入門ダンジョン限定なのかな…
…というまったく関係のない前振りはさておき、
今ちょうどやってるらしいので、SIGMOD/PODS
の論文をパラパラ眺めてみてます。データベース系の偉い学会です。
ACM 見れる人はこの辺 → SIGMOD,
PODS ← に PDF あります。
まだ Introduction しか読んでないけど適当メモ。
"XPath Evaluation in Linear Time":
一番自分の研究に近そうな方面。
XPath は定義通りに素直に木をたどる実装をすることもできるけど、
簡単な部分（数値や文字列演算なしで木の構造とタグ名だけに関するクエリ）
なら、XPath式がどんなに複雑でもXMLツリーサイズに比例する時間で確実に答えを返すような
巧い実装ができることも知られてて、ここではもうちょい範囲を広げてその簡単な部分＋属性の同値判定、
くらいまで線形時間でできる XPath の評価アルゴリズム。
"Scalable Regular Expression Matching on Data Streams":
DFAのステートはいきなりフルに作らずに適度に
キャッシュしながら on-the-fly でやるぜ！って辺りは何が新しいのかさっぱりなのですが、
複数の正規表現を同時に走らせてマッチをとるときに全部合わせた状態数が爆発しないようにグループ化を
うまく考えるとかいう辺り面白そげ。最近 Yahoo Research のひとよく見る気がする。
"Adding Magic to an Optimising Datalog Compiler":
well-known らしい "magic-sets transformation" というテクニックが面白そうだったので調べてみる。
08:04 08/06/11
だんじょん
うらやましがる作戦、
ということで猛烈に何かそっち系のゲームを新しく始めたくなってしまったので
七不思議
がスタート。
（図は、持ち込み無しで最初の４ダンジョン一発クリアして５つ目もかなりの安定状態に
なっちゃったので「これヌルゲーじゃね？」と思いっきり余裕をぶっこいてモンハウのど真ん中で
逃げずに殴り合ってたらいつの間にかやられてた様子を示す）
あと、AI って思いっきり賢くする気で作れば簡単な Roguelike なら自分より上手いくらいのいくらでも
作れそうだから適度にお馬鹿にするのもバランス調整のうちなんだろうなーと思いつつ、そういえば
Rogue やら NetHack やらの自動ソルバーってありそうだな探してみようなかなか見つからん、とか言ってたら
shinhさんに情報もらた。わーい。
Rog-O-Matic (Rogue) これか。
APW-Borg (Angband) というのもリンクされてた。
NetHackボット集 みたいなのも見つけた。
17:17 08/06/07
Sort of sort
順位決め @ ょゎさん
に反応。
1 國府田マリ子 2 中原麻衣 3 豊口めぐみ 4 浅野真澄 5 氷上恭子 …になったのですが
浅田葉子も山崎和佳奈もいないランキングなんて！
……じゃなかった。そんなことはどうでもよくて。
「推移律を満たさない度合」をパラメータ化して何かできないか
が面白そうだなーと思って考えてたんですけど、その前に、マージソートやその他著名な
ソートアルゴリズムに対して、推移律を満たさない答えを返すこと自体そもそも可能なのだろうか、
という疑問が。要は "A<B" と "B<C" がわかってる時に "A<C?" を問い合わせてくるアルゴリズムって
無駄なことをやってるわけで、最適なアルゴリズムならそもそもそんなことは訊いてこないので、
そこでfalseと答えて推移律を破ることもできない、はず。
「計算量のオーダー的に最適」なのとは独立な性質だと思う（普通のマージソートの最後に１回余分な比較を
付け加えて推移律を満たさない答えを返す機会を与えてもO(n log(n))は変わらない。逆に、最悪O(n^2)であっても
クイックソートが推移律を破らせないのは(重複要素がない場合)わりと自明な気がする）。
マージソートは、ヒープソートは、バブルソートは、挿入ソートは、シェルソートは、それぞれどうだろう。
あとで考える。
あるいは
昔ICPCの合宿かなんかで、「全順序になってない順序に標準ライブラリのsort関数を適用する
荒技トポロジカルソート」という話を聞いたことがあるような気がするんだけど、で、これも
クイックソートなら大丈夫そうかなーと朧気に思った覚えがあるんだけど、
一方でこれが上手く行かないように挿入ソートを組むのは簡単な気がする。
これが可能なsortの実装というのはどういうものに限られるのだろうか。
千日手
王手を回避しなきゃいけないので、自分の駒の移動先と打ち込み先は常に自玉のライン上（＋桂馬の位置）
に限る。可逆性から、移動元も同じく自玉のライン上（＋桂馬の位置）に限る。相手玉に関しても、
王手をかけなきゃいけないので移動先"または"移動元はライン上でなければならない云々。うーん。
「無限ではないことを示す」証明の定番というと、なんか下限のある盤面に関する特徴量を見つけて、
それが連続王手という制約のもとでは単調減少なことを言う、とかなんでしょうけど
全然うまい量が思いつかんのですよね。
というわけで（？）、期待！！！
10:16 08/06/05
双方連続王手の千日手
やねうらおさんとこの話題
が面白かったので考えてるんですけど難しいですね。違う方向から考えようと思って
[定理1] より王は動かない。ゆえに手順中に両王手は存在しない。すなわち、
全ての手は「"大駒"による遠距離からの王手」と、「大駒を相手玉に隣接させるもしくは小駒による、
近距離王手」のどちらか一方。千日手が一周する間の、先手による前者の王手の回数を Af (far)、
後者の回数を An (near) とする。同様に後手のそれを Bf, Bn とする。
これとは別に、相手にかけられた王手の回避の仕方で分類してみる。
王手をかけてきてる駒を取る Ag (get)、合駒を打つ Ap (put)、駒を動かして合駒 Ab (block)
の３種類。これも排反。
- An+Af = Ap+Ag+Ab = Bn+Bf = Bp+Bg+Bb
- Ap = Ag & Bp = Bg (打った回数分取らないと持ち駒の収支が合わない)
- Ap = Bg & Bp = Ag (打った回数分取られないと盤上の駒数の収支が合わない)
- An ≦ Bg & Bn ≦ Ag (近接王手は取るしかない)
- Bp+Bb ≦ Af & Ap+Ab ≦ Bf (合駒は遠距離王手に対してしか打てない)
ゆえに An ≦ Ag ＝ Ap ≦ Ap+Ab ≦ Af。だからなんだというのだー！ という辺りで諦めた。
[定理3] と [定理2] （Ap=0 とすると Ab=Af=Bb=Bf, 他=0 になるが相手玉のライン上から別のライン上へ１手で移るのは
不可能なことからこれはないqed）を言い直しただけに近い。うーむ。
11:21 08/06/04
計算機は人間のように考えない
再帰ではない方法
は、実際のところ、再帰のままでいいと思います。ひとつだけ細工が要りますが。
$cache = {}
def count_r(start, range, depth, a)
if $cache.has_key? [start,range,depth]
return $cache[[start,range,depth]]
end
if depth == 0
p a if $DEBUG
return 1
end
r = 0
start.upto(range) do |is|
a.push is
r += count_r(is, range, depth - 1, a)
a.pop
end
$cache[[start,range,depth]] = r
r
end
別の話題。
ラミーの役判定超簡易版 を作るときに、
まず同じ色ごとにカードを選り分けて、同じ数字が3枚未満なら連番で組むしかないからその場合のみを考えて…
と場合分けをする必要はない。そう、サイズが9とかだったらとりあえずnext_permutationするtopcoder脳。9枚のカードの並べ替えは 9! = 362880
通り。並び替えて機械的に左から3枚3枚3枚で区切って調べる、これを362880回繰り返す。
How to ...
人間が手で問題を解くなら、解の規則性や公式を見つけ出して、それに基づいた賢い計算式を発見する……
そういう風に考えるアプローチは必須だろうと思います。ただ、そこに計算機があるときはどうか。
「とりあえず馬鹿みたいに全部試す」のが計算機の最も得意とするところ。計算機達はそういう風に
アルゴリズムの夢を見る。
動的計画法
が感覚的に理解できないという人のひっかかる点の一つとして、
「問題 P の入力 n に対する答え P(n) が欲しいだけなのに、
P(n-1), P(n-2), P(n-3), ... , P(1), P(0) の答えを全部片っ端から計算する」
という知性のかけらも感じられない物凄い無駄なことを平気でやってる感、があるのではないかと思う。
自分が手で動的計画法を実行してるシーンを考えると実際なんか馬鹿っぽいのだ。
けど、たぶん、計算機にとってはそうじゃない。
とかいう。
何が言いたいのかさっぱりわからなくなってきたけど、こう、アルゴリズムを考えるときには、
それを実行するのは自分じゃなくてコンピュータだよ！っていうのは意外と頭から抜け落ちがちだよ
という話をしたかったんだと思う、たぶん。冒頭のリンクはあんまり関係なかった気がしてきた。
17:55 08/06/03
おもしろいみろん
「プログラミング言語の」「フォーマルな」意味論（Semantics）
には大きくわけて３種類あって、一番メジャーなのは操作的意味論…
（参考 → [1]
[2]
[3]）
というのは、まあそうかなとも思うのですが、
それはそれとして一番面白いのは表示的意味論だ、と適当なことを書き散らしてみるよ。
役に立つかなんて関係ない、面白さが全てだ。
勿論、どれもきちんと深く学んで、どういう風に応用されてるかを知れば面白いんですよ。
でも操作的意味論と公理的意味論って、パッと見すごく当たり前じゃないですか。
操作的意味論って要するに eval の実装が書いてあるだけだし（暴言）、
公理的意味論では "プログラムを動かす前と後でどういう論理式が成り立つか" がプログラムの意味で、
「プログラム "x := 42" を実行した直後は、42を当てはめると真になる論理式はxを
当てはめても真になりますよ x+1==43 とか。それが x:=42 の意味」みたいな。知ってるよそんなこと。
いや、繰り返しますが、もちろん世の中そんな単純ではなくて、それぞれ真剣に深く考えると
そんな「当たり前」なことばかりではなくて面白いですし、それ以前に、当たり前っていいことだよね。
プログラマの直感に合うってこと、わかりやすいってことだし。
ただ、勉強してて「"プログラム" っていうものをそういう風に捉える見方があったのか！その発想はなかった！」
と感じる瞬間が一番多かったのは、自分にとっては表示的意味論でした。そういう意味で「面白い」と思う。
全速力で表示的意味論
表示的意味論というのは、プログラムの意味を数学のオブジェクトで表現しようとする意味論です。
「123 っていう式の意味は？」
「整数 123 だよ」
「function f(x) { return x+2 } っていう関数の意味は？」
「整数を受け取ってそれに2を足して返す(数学的な意味での)関数だよ」。
「function g(x) { return x+1+1*1 } っていう関数の意味は？」
「字面は違うけど、それも意味的には整数を受け取ってそれに2を足して返す(数学的な意味での)関数だよ」
「f(123) っていう式の意味は？」
「fの表す(数学的な)関数を123の表す整数に適用した結果 ― つまり整数125だよ」
「function h(x) { if( x==1 ) { return 2 } else { for(;;){} } } っていう関数の意味は？」
「引数が1なら2を返して、それ以外なら無限ループする関数だよ」 !!!!
ええと、無限ループって全然数学用語じゃないですよね。困った。なんとか数学っぽく定義したいんですが。
ここは、こんなアプローチがあります。意地でも関数には関数で居てもらうために、
無限ループするときは「無限ループしてることを示す値」というのを返すことにしてしまう。その名も ⊥ （ボトム）。
「では改めて、function h(x) { if( x==1 ) { return 2 } else { for(;;){} } } っていう関数の意味は？」
「引数が1なら2を返して、それ以外なら⊥を返す関数だよ」
「function i(x) { return 3 } っていう関数の意味は？」
「引数１個受け取るけどその値に関係なく 3 を返す関数だよ」
「function k(x) { return i(h(x)) } っていう関数の意味は？」
「引数１個受け取とって、それにhの表す関数を適用した結果にiの表す関数を適用した結果を返す関数だよ」
「k(5) っていう式の意味は？」
「kの表す関数に5の表す整数を適用した結果だから ―
整数5をhに適用した結果にiを適用した結果
―
つまり⊥にiを適用した結果
―
iは引数関係なく 3 を返すはずだから
―
この式の意味は整数 3 だ」!!!!
Haskell みたく遅延評価する言語だったなら、この会話は正しい。確かに k(5) は 3 になるはずだから。
でも、正格評価の言語だと、これはおかしい。k(5) は無限ループするはず、つまり意味としては ⊥ でないといけない。
「function i(x) { return 3 } っていう関数の意味は？」
「引数が⊥なら⊥を返して、それ以外なら値に関係なく 3 を返す関数だよ」
正格評価の場合、正しくはこうでないといけなかったのだ。i だけじゃなくて f も g も h も k も、そう。
こんな風に、「int -> int 型の式の意味」は、
直感的に思い浮かぶ「整数から整数への(数学的な)関数」では上手く行かないのです。
ここで上げた方法では、「(整数または⊥ から 整数または⊥ への数学的な関数) または⊥」みたいなものと
して考えよう…という方向をとりました。別の方法もあるんじゃないかなたぶん。
あと、普通の値と違って⊥は if x == ⊥ then ... みたいな形で使うことはできないという制限から
考えると、「(整数または⊥ から 整数または⊥ への数学的な関数) または⊥」の中でも、プログラムとして
表現できる集合はごく一部だろうと推測できて、実際、「連続関数」と呼ばれる種類の関数（微分とかで出てくる
連続関数とは別物です注意）だけがプログラムで書けることがわかったりして
（参考: [PDF]武市先生の
講義資料）、
この「または⊥または⊥または⊥」で⊥を埋め込みまくった謎の集合上の連続関数に、
「⊥が少なめの方が"大きい"関数」的に大小関係を定義してやると CPO (Complete Partial Order)
と呼ばれる種類の集合になって、
再帰関数の意味とは不動点である！
と議論できるようになったりとか、まあ色々なお話があるわけです。
いわゆる「領域理論」というのが、こっちの方向の表示的意味論です。
こう、「無限ループ自体を⊥という１つのオブジェクトとして扱っちゃう」
「遅延評価/正格評価を、評価順序というよりも、値⊥の扱い方の違いとして捉える」、
あと全然説明してないですけど「"⊥が少なめの方が大きい関数"的に関数と関数の間の順序関係を考える」
「再帰関数は不動点というか⊥からはじまる関数列の極限」あたりの発想が、自分的には結構驚きだったの
でありました。
ところで
表示的意味論界（？）の大問題として、「Full Abstraction」というのがあります。
同じ動きをするプログラムの意味は、多少字面が違ってても同じ数学的オブジェクト
であって欲しい。そういう表示的意味論は「Fully Abstract である」と言う。これが成り立つと嬉しい。
だって、成り立たないと、同じ動きをするプログラムなのに「意味」が違うということに
なってしまうじゃないですか。
これが簡単そうに見えて面倒な問題で、PCF
（[PDF] 勝股先生の資料）
というスタンダードな高階関数型言語の Fully Abstract な表示的意味論が、領域理論だとなかなか作れない。
長年の未解決問題となっていました。
住井さんの記事 に詳しいですが、
プログラムでは書けないのに意味論上のオブジェクトとしては存在するような余り物（この場合は por）が
どうしても紛れ込んでしまうのが問題らしい。
これを颯爽と解決してのけたのが、「ゲーム意味論」という別の表示的意味論で、
プログラムの意味とは「実行環境とプログラムの間で戦われるゲーム」であるとする、これまた楽しい発想。
この「ゲーム」っていうのは人間がやってもたぶん全然楽しくないとは思うんですが、まあ、
数学的にちゃんと定式化された概念ではあるので「意味」としては使えます。
正確には、プログラムの「型」がゲームの「ルール」で、プログラムそのものはゲームにおける「戦略」
とする。function(x) { return x+2 } は実行環境側が打った手に2を足して打ち返すという戦略（…というのは
ちょっとかなり不正確ですがそんな感じ）。ググったら
[PDF] "Notes on Game Semantics"
の最初の方に、ゲーム意味論だと
por は出てこないよという話が載ってるみたいので気になる方はどうぞ。（自分はちゃんと読んでない
まとめ
例によって専門家の強烈な突っ込み待ちです！
