はてなブックマーク

去年のアドベントカレンダーの続きです！ Coqみたいな定理証明器のおもちゃみたいなのをHaskellを使って1年と48時間ぐらいで作れるかな？って話です。 去年の記事は http://qiita.com/kikx/items/10d143edc090bdfec477 http://qiita.com/kikx/items/b0eda41bc7b9036ac18d http://qiita.com/kikx/items/57aad1867b89f8955611 です。 去年の記事で型検査と計算はできたので、証明支援を行う部分を作っていきます。 対話環境の作成 対話的にコマンドを実行するコードを書くのは本質とは関係ないので、なるべく手抜きで作りましょう。ghciをそのまま使う方法もありますが、グローバルなIORefを引数で渡して回ったりしないといけないのでちょっと使いにくいです。簡単な方法とし

この記事は定理証明アドベントカレンダー2013のたぶん7日目の記事です 誰でも定理証明器を作れるようになろうという趣旨です。ここではCoqのパクリみたいなサブセットを48時間で作ります。 タイトルの元ネタは http://en.wikibooks.org/wiki/Write_Yourself_a_Scheme_in_48_Hours です。というわけで、使う言語はHaskellですが、他の言語でも特に問題ないと思います。 定理証明器の部品は以下のものが必要です。 記述言語 カーネル 証明支援言語 その他 記述言語はCoqではGallinaといわれてる部分です。立派なプログラミング言語をひとつ設計しないといけません。このプログラミング言語によって、定理のステートメントを記述したり、証明を記述したり、関数を書いたり、データ構造を定義したりします。 カーネルは記述言語のインタープリタになります