日々の流転

λ. gimp-jp-plugin

すっかりPlug-in Registryに登録するのを忘れていたので、登録。

λ. gimp-spi

がコンパイル出来なくなってて焦る。結局、WineLibを安全に初期化するにはどうするのが良いの?

λ. 自慰史観

という言葉があるらしい。面白い言葉だ。

λ. lazarus

ほほぅ。以前に試したときは全然使えなかったけど、最近はいちおう使えるようになったんだ。久しぶりに試してみようかな。

λ. うー

かったりー

λ. 昼食

Dean & Deluca

λ. キミならどう書く

規定競技のコードを用意した。資料も作らねば……

http://www.tom.sfc.keio.ac.jp/~sakai/talks/LLDN/

λ. RHG読書会::東京 Revolution::ふつうのLinuxプログラミング

相変わらず濃い集まりだった。

λ. 人狼審問 : (747)薄明の村

723村で負けたのが悔しくて速攻でエントリー。今度はちゃんと狂人をゲットしたんだけど、結果はかなりへろへろに……人狼様申し訳ない。

関連リンク

• B1/747村 - 人狼ファンWiki

λ. 『現代数理論理学入門』

を読んだ。「現代」と言いつつ、もはや30年前の本になってしまってるが、非常に良い本。述語論理の完全性, モデル理論, 帰納関数とチューリング機械, 算術体系の不完全性, 選択公理の独立性, 連続体仮説の独立性と強制法といったトピックについて、よくまとまっている。約100ページ。

個人的な収穫は、モデル理論でのコンパクト性定理の使いでと、あと強制法のイメージがわかったこと。

• 復刊.com: 現代数理論理学入門

参考

• 「レーヴェンハイム・スコーレムの定理って変なの?」
• Wikipedia - Löwenheim-Skolem theorem
• 集合論雑記
  • 強制法入門 1.0版

λ. Hikiへのパッチ3つ

• [Hiki-dev:01126] Unqualified use of rdf:resource has been deprecated
• [Hiki-dev:01127] RSSのchannelのURI
• [Hiki-dev:01128] 例外表示時の HTTP Status Code

【2008-07-06 追記】 [Hiki-dev:01199] で CVS HEAD に取り込んで貰えた。

λ. チャーチ・ロッサーの定理の証明に挫折

ここ数日Agdaでチャーチ・ロッサーの定理を証明することに熱中していたのだけど、なんか上手くいかずに詰まっていた。チャーチロッサーの定理の証明の流れの本質的な部分はすぐに書けていたのだけど、細かい部分で色々とひっかかったり嵌ったりとか。

特に任意のラムダ式 M1[x,y], M2[y], M3 に対して M1[x:=M2[y]][y:=M3] = M1[y:=M3][x:=M2[y:=M3]] が成り立つことの証明。構造帰納法で示せば良いのだけど、実際にAgdaで証明を書こうとするとラムダ抽象の場合が面倒過ぎで……。 その後、ラムダ式のデータ型「data Term a = Var a | App (Term a) (Term a) | Lam (Term (Maybe a))」*1がモナドになっている事を証明出来れば良く、直接証明するよりもその方が筋が良さそうという事に気付いたのだけど、「(m >>= f) >>= g = m >>= (\x -> f x >>= g)」の証明のラムダ抽象の場合がやっぱり面倒過ぎで……

結局、まだその部分の証明は書けていないけど、燃え尽きたので中断。

λ. 『謎の彼女X (2)』 植芝 理一

いつの間にか二巻が出ていた。