2001-12-05
λ. 利害が絡まないと真剣になれないけど、利害が絡むと今度は目が曇る。悩ましい。
λ. PM 6:30 頃まで惰眠を貪った。
λ. やっぱ、明日は研究会あるのね。発表が僕の番なんだけどどうしよっかな。僕が発表資料を作っても、既存の資料の質の悪いツギハギにしかならないだろうから、自分で資料を作る代わりに、他の人の発表資料をそのまま使わせてもらって、それに解説を加える形で発表する事にする。それから、僕はプレゼンの類をほとんどした事の無い人間なので、内容については期待しないこと。 > 研究会の人
2002-12-05
λ. 喉が痛い。頭がボーッとする。風邪ひいたかな。
λ. 読書
- 『ちゃぶだいケンタ』
- うめ[著]
λ. C++言語カルトクイズ
Zinnia hack tomorrow. (2002-12-05) より。
がびーん。typenameも例外仕様も知りませんでした。exportも名前だけしか知らなかったので答えられなかったし、仮想継承も説明できませんでした。仮想継承の実装方法は11/10の「C++: 水面下の仕組み」で理解していたのだけど、概念を説明するのは難しい。
λ. open-uri
[ruby-dev:19011]より。おぉ、便利だ。
λ. Computational lambda-calculus and monads.
Wadlerの論文は幾つか読んだけど、Moggiのオリジナルはこれまで読んでなかったので、読んだ。すごく面白かった。
2004-12-05
λ. 『さよならみどりちゃん』, 南 Q太
を読んだ。
λ. Cで作ったProcをブロック付きで呼び出すと……
[ruby-dev:25051]。この振る舞いはおかしくて以前の振る舞いが正しい気がする。まぁ、Proc#callに渡されたブロックを参照する方法はまた別に欲しいとは思うけど。
[追記] eval.c (rev 1.744) で修正された。
λ. 停電
年に一度の定期保安点検による構内停電。
![[GROW CUBE のスクリーンショット]](./images/20061205_0.png)
2007-12-05
λ. 整礎性は一階述語論理では表現できないのね
先日、ヘンキン文 - ヒビルテ (2007-09-16) で、「Xが証明可能であることを□Xと書くと、証明可能性を様相論理で扱える」ということに触れた。これが Löb Logic と呼ばれる論理で、□(□φ→φ)→□φ という公理図式(axiom schema)を持っていて、PAでの証明可能性をある意味で忠実に反映した体系になっている。 それで、この論理をSPASSで扱って遊べないかと思ったのだけど、ちょっといじっているうちに、出来ないということに気付いた。しょぼーん。以下にその理由を簡単に書く。
SPASSはあくまで一階述語論理の定理証明機なので、□(□φ→φ)→□φ のような様相論理の公理図式は、クリプキ構造に関する一階述語論理の公理で表現してやる必要がある。 そして、□(□φ→φ)→□φ はクリプキ構造の到達可能性関係が推移的かつ整礎(well-founded)であることに対応することが知られている。 で、推移性は何の問題もないのだけど、問題は整礎性。
関係Rの整礎性は「空でない部分集合にはRに関する極小元が存在する」こと、もしくは「x0 R x1 R x2 R … という無限列が存在しない」ことによって定義される*1。 前者の定義では集合を量化する必要があるけど、一階述語論理では個体しか量化できず、集合を量化出来ないのだった。二階論理なら ∀P. (∃x. P(x)) → (∃x. P(x) ∧ ∀y. P(y)→¬R(x,y)) と書けるんだけどね。後者の定義も同様に一階述語論理では書けない。
*1 厳密には、選択公理を仮定しない場合には両者は同値ではないけど
2008-12-05
λ. 風邪でダウン中 (2)
熱は37℃台のままで、下痢が止まらない。すべきことが色々と溜まっているのに困った……
ところで、「お腹を冷やすな」というのは比喩表現だと思ってたら、お腹って本当に冷えるんだね。手を当ててヒンヤリしたので驚いた。胴体の中心に近くて血管も沢山通ってるだろうから、凍死寸前でもなければ冷えたりなんかしないと思ってたよ……
λ. 参議院法務委員会での国籍法改正案の採択
改正国籍法の是非についてはともかく、意見に対して音声と速記を止めるってのはどうなの? 国会での慣行を知らんので何とも言えないのだけど、こういうことが行われているってのは結構ショックなんだけど……
