日々の流転

λ. Feliĉan novjaron !

なんか、いつのまにか新年らしい。特に感慨も何もないんだけど、まあ、酔い落としを。(^^;;

で、今年こそは……(以下略)

λ. GIMP起動時にPlug-Inを自動で起動させるには

むむ、知らなかった。メモメモ。→ Re: [Gimp-developer] Module or plug-in for embedded control of GIMP?

If a plug-in registers a procedure of the type GIMP_EXTENSION with 0 arguments and 0 return values it is automatically started on startup of The GIMP and will stay alive until GIMP is quit.

λ. 明けましておめでとうございます。

昨年は色々と迷惑をお掛けしたと思いますが、本年もぜひよろしくお願い致します。

λ. 『felica - BITTERSWEET FOOLS RECOLLECTION BOOK -』

それなら、学校が始まったらしばらくκ208にでも置いておきますので、適当にご賞味下さいませ。

λ. 読書

『テニスの王子様 16』

許斐 剛 [著]

λ. あけましておめでとうございます。

今年もどうぞよろしくお願いします。

って、あーあ、年明けちゃったよ……

λ. おみくじ

λ. あけましておめでとうございます

旧年中はお世話になりました。今年もよろしくお願いいたします。

まあ、今年もまた溜まったTODOを片付けているうちに、いつの間にか年が明けていたという感じで、あまり感慨も無いんだけどね。 ただ、昨年のまとめや今年の抱負を書いている人を見ると、見習わなくてはと思う。 後でちゃんと書こう……

λ. KAT-MLでの双模倣規則の証明

昨日の「クリーニ代数入門」の続き。 テストつきクリーニ代数のための対話的定理証明器KAT-MLというのを知ったので、早速試してみた。

KAT-ML is an interactive theorem prover for Kleene algebra with tests. The system is designed to reflect the natural style of reasoning with KAT that one finds in the literature. It is available for several platforms.

Windows版のパッケージとしてSML/NJ同梱版と別版があったので、同梱版の方をダウンロードしてくる。 Tcl/Tkで実装されたGUIがあるようだったけど、コマンドラインで使うだけならTcl/Tkは不要なようなので、Tcl/Tkのインストールはしなかった。 ファイルを展開してKAT-ML/Binにあるkat.cmdを実行すると、コマンドライン版が立ち上がる。

何を試そうか迷ったが、とりあえず双模倣規則「p;q = q;r ならば p*;q = q;r*」を証明してみた*1。 簡単かと思っていたら結構大変だった。

• 作業ログ bisimulation.txt
• 結果の証明ファイル bisimulation.xml
• コマンドのダンプ bisimulation.kat
• LaTexにエキスポートした証明 bisimulation.tex
  • PDF bisimulation.pdf

λ. 年末年始

今回の年末年始は非常に日本人らしい過ごし方をした。 31日はコミケに行き、夜は紅白歌合戦を見て、除夜の鐘をつきに行った。 そして、年が明けた後は、(家からだけど)初日の出を見て、それから初詣にも行ってきた。 たまにはこういう季節感のある正月もいいなと思う。 ちなみに、おみくじは大吉だった。 今年は良い事がありそうだ。