一人CSアドベントカレンダー開催のお知らせ

最初にIsabelle(ここではHOL系しか扱わない)に入門します。って言ってもチュートリアルの解説をするだけです。 ある程度知ってる人が読む意味はないんですが、Isabelle全く知らん人向けに日本語で読める資料ってあんまりなさそうなので、チュートリアルを適当にやるだけでも実は意味があるんでは的な発想でとりあえずこれをやることにしました。

真面目に入門したくて英語にそこまで抵抗ない人は公式のprog-prove.pdf読みに行く方が早いです。

ここでは実際にIsabelle/HOLを使った証明を紹介・解説していきます。今の所IMPの意味論ちょろっとやるみたいな感じです。 Isabelleの解説がメインなので内容は薄いですがIsabelleってこうやって使うんだよ〜証明ってこうやって書くんだよ〜って雰囲気が伝わればいいかなと思っています。 (そういうのが伝わる日本語資料もあんまりない気がしたので)

せっかくなので個人的にこの前お世話になったりしたNominal Isabelle使ってtyped lambda calculusの簡単な証明とかやってみようかなという内容です。 あとかつてIsabelleで圏論(Yoneda lemma示すくらいまで)もやったことあるのでその解説もやってもいいかもしれないということで2日分くらいは余裕を持たせてあります。

この辺は後で変更あるかも知れないのでそのへんはあしからず。

Haskellで最近使ったり使ってなかったりするライブラリの紹介とか解説とかをします。 ここ以外のコンテンツで25日分埋まらなかった場合に備えて空けてある枠なので日数は未定です。 Haskell編の最初にまとめてやるかも不明ですが一応ってことで。

ここからがメインコンテンツで、Haskellを使ってproof assistantを作ります。 (最初に断っておくとproverは作りません。あくまでcheckerとそのassistする部分がメインです。)

多分色々前提になる知識を解説したり、proof assistantを作るには何が必要かとかの説明がいると思うのでそのへんを初めに少し解説します。

proof assistantを実際に作っていきます。

最初はステップアップで徐々に拡張して行く感じで作ろうと思っていたんですが、特に参考にできるものもなく始めてだったので自分で手を動かして作ってみた所そうそう前に進めるはずもなく backwardな変更が出過ぎてステップアップするのつらすぎたので普通に現在のproof assistantのコードの解説になります。

checkerのコア機能の解説→assist機能関係の解説→プラグイン・拡張部分の解説 の順になります。

上で作ったものは当然ですがまともに証明を書こうとすると色々足りないので、今後ちゃんとしたassistantにするにはどういう感じの拡張が欲しいかな〜とかそういう話を、 「開発が間に合わなかったものは全部読者への演習問題にしたらええねん」的な思想により丸投げされるコーナーです。