日々の流転

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

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

まあ、今年もまた溜まった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