証明された証明支援器をScalaで書いてみた
この記事はTheorem Proving Advent Calendarの7日目の記事である。
静的型付き関数型言語は言語処理系の実装が容易であることから多くの場合、証明支援器(proof assistant)が実装されている。例えばStandard MLではIsabelle/HOL、OCamlでCoq、HaskellでAgdaが実装されている。
しかしながら、Twitter社が使っていることなどで最近有名になっている関数型言語のScalaはそのような証明支援器はあまり見受けられない。これはScalaが言語処理系だけでなく一般のアプリケーションでも効果的であることを示している。そうは言ってもScalaで証明支援器を書いてもいいんじゃないかと思ったので書いてみた。
実装に関して、証明支援器のモデルを実装したCoqのライブラリを使用した。coq2scalaを使ってこれをScalaのライブラリとして使った。*1ソースコードは以下で公開している。
ソースコードをダウンロードしてmakeしたのちに
scala Top
と打てば対話環境が起動する。使えるコマンドは以下の6つだ。最後にピリオド"."を打つ必要があることに注意しよう。*2構文やエラーメッセージはオリジナルのOCaml版と揃えた。
Infer t. #項tを型チェックし、型を表示する
Check t : T. #項tが型Tを持つかどうかチェックする
Axiom x : T. #T型の変数xを公理として仮定する
List. #現在仮定されている公理の列を列挙する
Delete. #公理を削除する
Quit. #終了する
例えば簡単な論理式(∀P, PならばP)の証明は(λP:Prop. λH:P. H)という恒等関数で表現できるが、その証明は次のようにCheckコマンドでチェックできる。∀の式は丸括弧"()"で、λ式はカク括弧"[]"で表現している。
h2o:coqincoq_scala imai$ scala Top Check [P:Prop][H:P]H : (P:Prop)P->P. Correct.
「Correct.」と表示されたら成功だ。もっと複雑な論理式にも挑戦してみよう。
CCなので式の構文は項も型も同じである。その構文は以下のようなBNFで定義している。
<expr> ::= | "Set" | "Prop" | "Kind" #定数 | <ident> #変数参照 | "[" <idents> ":" <expr> "]" <expr> #関数抽象(ラムダ式) | "let"<ident>":"<expr>"="<expr>"in"<expr> #ローカル変数束縛 | "(" <idents> ":" <expr> ")" <expr> #forall型 | <expr> "->" ... "->" <expr> #関数型 | <expr> " " ... " " <expr> #関数適用
まとめ
- Coq extraction pluginさえ用意すれば証明支援器が簡単にかけるよ
- Scalaは関数型言語だからDSLも簡単に書けるよ
- coq2scala使ってね
