日々の流転

λ. 夢

キングオブファイターズとハンター×ハンターと列火の炎と水戸黄門が混ざったような夢を見た。まったく意味不明だった。

λ. XMLで表現して管理したいもの

誰かつくってくんねえかなぁ。

証明図

MathMLと似たようなものか。 もちろん、NKでもLKでもLHqでも何でもありで。 さらに証明の妥当性の検証とか出来ると吉。

将棋の盤面と棋譜

そういえば、白将棋駒(WHITE SHOGI PIECE)と黒将棋駒(BLACK SHOGI PIECE)って、JIS X 0213 と Unicodeに入ったんでしたっけ?

ボーリングのスコア

以前にも同じことを考えたけど。

λ. GTK+ Object Builder

GOB is a preprocessor for making GTK+ objects with inline C code so that generated files are not editted. Syntax is inspired by java and yacc or lex. The implementation is intentionaly kept simple, and no C actual code parsing is done.

λ. 読書

『吸血姫美夕 (ヴァンパイア ミユ)　二』

『吸血姫美夕 (ヴァンパイア ミユ)　三』

『吸血姫美夕 (ヴァンパイア ミユ)　四』

『吸血姫美夕 (ヴァンパイア ミユ)　五』

垣野内成美[画] 平野俊貴[原作]

λ. アジアでのRuby

偶然このメールを見掛けて気になったのだけど、日本を除くアジアでのRubyって現在どんな感じなのかなぁ。

λ. Gimp-Python shell

ふむふむ。Gimp-Rubyでもちゃんと補完できるようにしたいところだなぁ。

λ. DAG

Development Assistance Group よりも Directed Acyclic Graph の方が先に頭に浮かぶ今日この頃。

λ. Amaya

libthotのDisplayJustifiedTextが仕事を抱え込み過ぎてとんでもない状態になっている。ここさえ切り崩せればlibthotは一段落なんだけどなぁ。ディスプレイ上で何度か眺めててもサッパリなので印刷したら7ページなり。長過ぎじゃ!!

λ. 「VIP女性独占」

「VIP女性独占」というサブジェクトのspamがきた。

ちょｗｗｗｗｗｗｗおまｗｗｗｗｗｗｗｗっうぇうぇｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗｗ

λ. 秋学期修士最終試験

中高の入試と被っていたので朝バスは凄い状態になっているのではないかと思ったが、8:40〜9:00ごろには空いていた。受験生はもっと早い時間だったのかな。

発表ではPowerpointの発表者ツールが使えずに焦ったが、発表時間の調整は発表練習の時よりもうまく行っていた。不思議だ。そして、質疑応答もそれなりにうまくこなせた。人事は尽くしたし、あとは天命を待つだけ。

発表スライド:

発表を終え、会場を後にする修士たちの姿(まだ未発表の人もM2じゃない人もいるけど)。赤松さんによる写真。

λ. Haskellと高階論理の土台は異なるか?

宮本の日記（仮）のGHCは気色悪いという話に関して。コメントとして書こうと思ったのだけど、色々と書き足しそうなので、こっちに書く。

∀x. (a → b → x) → x が a ∧ b と同型になることは通常パラメトリシティを用いて示されるが、Haskellのような言語ではパラメトリシティは完全には成り立たない。また、高階論理であってもパラメトリックでないモデルを考えれば両者は同型にはならないのではないかと思う。

次に ∀a,b. a → b という型を持つ閉項が存在するという話について。全ての型に対して不動点演算子 fix が存在する言語では、全ての型が閉項 fix(λx. x) を持ち、論理体系としては矛盾した体系になる。それゆえ、不動点演算子はパラドキシカル演算子と呼ばれることもある。 Haskellのように再帰的定義が自由に行える言語では fix f = f (fix f) によって不動点演算子を定義でき、論理体系として解釈すると矛盾した体系になっている。通常の論理では無矛盾であることが基本なのに対して、通常のプログラミング言語は論理体系としては矛盾していることが前提なため、ある意味「土台」が異なっていると言えると思う。

その点に関して、A note on inconsistencies caused by fixpoints in a cartesian closed category (20061110#p01参照) では「The results indicate the different nature of domain theory and set=topos theory or, in other words, that programming requires other foundations than even a constructive set theory.」と述べられていたりする。

また、この話については「自己言及の論理と計算」 (20030629#p03参照) は非常に面白く書けていると思う。

この辺りの話は結構面白く、幾らでも書けそうな気がするけど、とりあえずこの辺りで。

(2/5 追記) seqとパラメトリシティ

seqとパラメトリシティの話は知ってはいました(20050315#p03)が、面倒だったので触れていませんでした(それにseqが存在しなくともパラメトリックでないモデルを作ることは出来るはずだし)。そしたら早速指摘が。

• sumiiさんのseqとパラメトリシティ
• KeisukeNakanoさんのパラメトリシティとseq

今回の話の個人的な収穫は以下の点。Pittsのアプローチには詳しくないため、TT-closedness は admissibility と同じようなものだと思っていたが、KeisukeNakanoさんによれば「TT-closed は admissibility より強すぎる」とのこと。うーむ……

λ. 『Big Bang』 by Simon Singh

ようやく読み終わった。読み始めたのが11月でなので約3ヶ月かかったわけか。ほとんど通勤中に気が向いたときにしか読んでいなかったというのもあるが、さすがにこんだけかかるとなぁ……。次はもっと薄い本にしよう。

λ. pure crisis :)

haskell-cafe の pure crisis :) というスレッドがちょっと面白い。「pure functional denotation for crisis:　(_|_)」に対する、「Thus, when people try to evaluate the amount of savings they have left, their behavior frequently becomes _undefined_ :)」とか。