日々の流転

λ. “Mechanizing common knowledge logic using COQ” by Pierre Lescanne

Coqの上で共通認識論理を形式化して色々する話。こういうのはとっくにやりつくされている話だと思っていたが、案外そうでもないらしい。

ヒルベルト流の共通認識論理を深い符号化法(deep embedding)でCoqに埋め込む。作る体系は普通のものではなくてCoqのパワーを生かしたもので、高階述語論理になってるし、論理結合子も→と∀を使ったチャーチエンコーディングで表現するようになっている。

共通認識論理の紹介としても分かりやすい。 ただ、最大不動点に関する話は、A→BのときAがBよりも大きいとしていて変な気がする。 共通認識様相を特徴付ける推論規則として、⊢ φ→ψ∧E_G(φ) から ⊢ φ→C_G(ψ) を導く推論規則があって、これは一種の余帰納法(coinduction)なのだから、A→BのときAよりもBが大きいとすべきだと思うが。

The muddy children という問題について、これを使って実際に証明をしている。ただ、専用のTacticsはまだ用意していない。

また、三賢者と帽子のパズルを例に、共通認識様相が実際には必要ない場合についての説明があった。「⊢ 仮定→結果」の形で示す場合には仮定に共通認識の様相が必要になるが、「事実 ⊢ 結果」の形で示す場合には事実には共通認識様相は不要*1。先日、SPASSで知識の論理を使って論理パズルを解く?で書いた話がまさにこれに当てはまっていて、うわっと思った。

あと、「Epistemic logic is usually mechanized by model checking」と書かれていて、Needham-Schroeder Public-Key Protocol の話が参照されていた。この話はモデル検査では有名な話だけど、知識論理と関係があるとは知らなかった。

それから、この論文とは直接の関係はないけど、ytbさんが知識様相論理をAgda2上に実装しているそうなので、どんな感じになるのか少し気になるのだった。