去る1月12日、定理証明支援系ツールCoqの初心者向けチュートリアルが開催された(http://kokucheese.com/event/index/23667/)。今後も2月2日 (http://kokucheese.com/event/index/23744/)、2月9日、2月16日と引き続き開催されていく予定である。 本記事では、開催の様子をレポートする。
定理証明支援系ツールCoq(Coq Proof Assistant)とは
Coqとは、定理証明支援系ツールの一種である。定理証明支援系ツールとは、コンピュータプログラムによって数学的定理の証明を行うツールである。詳細はProofSummit2011のイベントレポートを参照いただきたい。
Coqチュートリアル開催の背景
ProofSummit2011においても、@tmiya_氏によるCoqの入門解説が行われていた。
ただし、この入門解説は、実際には8時間程度のチュートリアルの抜粋であった。
そのため、対象者を初心者向けに絞り、気軽に質疑応答しながらCoqに親しめる機会を設けよう、という趣旨から、今回のチュートリアルが開催された。
開催の様子
まず最初は形式手法の概説である。一口に形式手法といっても、定理証明支援系以外にモデル検証などの様々な技術がある。定理証明支援系の強みは、実装コードの生成が可能な点である。CoqにおいてもOCamlやHaskellなどのプログラミング言語生成機能が装備されている。逆に弱みとしては、証明に対する習熟が必要な点がある。ただし、定理証明支援系の基本はプログラミング言語であるため、基本的にプログラミング言語と同様に習熟可能である。
続いて、Coqのプログラミング言語としての文法の解説が行われた。Coqの文法は、数学の証明に合致するように構成されているため、独特なキーワードが使われる。ただし、関数型プログラミング言語に慣れている人にとっては、基本概念に関しての違和感はないはずだ。パターンマッチ文は、HaskellやOCamlといった関数型プログラミング言語とほぼ同一である。またユーザ定義型の定義も簡単に行える。
ユーザ定義型としてブール型を定義したところで、簡単な証明としてド・モルガンの法則を証明するという演習が行われた。証明というと難しい印象を受けるかもしれない。その場合は、ド・モルガンの法則の正しさをどうやって確認するかを考えてみると良いだろう。通常は全部の入力値に対して真理値表を作成して確認するはずだ。実は、Coqでも基本的な証明の考え方は同様であり、すべて場合分けをして、結果を確認するのである。
チュートリアルの最後には十分な質問時間があった。基礎的な質問に関しても講師から丁寧な説明があり、非常に充実したチュートリアルであった。
今後に向けて
今後は順次、2月2日、2月9日、2月16日と開催していく予定である。次回以降は少しずつ複雑な証明に挑戦していくため、「プログラムを証明するってどういうこと?」という方はこの機会にご参加いただきたい。
関連情報
Coqチュートリアル開催のきっかけとなったイベント
※ ProofSummit2011 http://partake.in/events/ac41261d-6026-4d09-8814-5ad3e58446e8
Coqに関する議論が日本語で行われている勉強会
※ Formal Methods Forum http://groups.google.com/group/fm-forum
※ ProofCafe http://proofcafe.org/wiki/
Coqチュートリアルの申し込みサイト
※ 2月2日 http://kokucheese.com/event/index/23744/
※ 2月9日 http://kokucheese.com/event/index/25867/
※ 2月16日 http://kokucheese.com/event/index/25868/