ProofSummit 2014 & JSSST Coq Tutorial


名古屋で開催された ProofSummit 2014 と、同じく名古屋大学で開催されている日本ソフトウェア科学会のチュートリアル:定理証明支援系Coq入門 に参加しました。

ProofSummit は各種の定理証明系(今年は Coq, Agda, Mizarの話がありました)とその応用について年に一回(大体8月末〜9月初に)開催しているイベントで、2010年に開催された Coq庵 から数えると今年で5回目です。「Coq を使ってみた」的な初心者の発表から、定理証明系を使って計算機科学の研究をしているような研究者による発表など幅広い内容の発表があります。今年の発表のかなりの部分に付いては、上記リンクから発表資料が参照出来ると思います。
ProofSummit 今年は定理証明イベントと一緒に開催する関数型言語イベントが中止になったり、東京で ScalaMatsuri が開催されていたりなどで、ちょっと参加人数が減りましたが、来年もまた開催したいし、来年こそはなんかネタを用意して参加したいです。

Coq チュートリアルは、産総研でCoqを使って研究されている Affeldt さんによる、Coq を使う意義/Coqについて/Coqの拡張であるssreflectのチュートリアル、でした。聞きに行った主眼はssreflectのチュートリアルだったのですが、前半の定理証明系やCoqについての話の部分も非常に面白かったです。発表資料は Affeldt さんのページから取得出来ます。
Coq チュートリアルは、100人以上が参加の、非常に盛況なチュートリアルでした。

その前の NII Shonan Coq セミナーと合わせて、この夏は Coq が熱い夏でした。今年のイベントとしてはあと、12/3-5に「高信頼な理論と実装のための定理証明および定理証明器」というのが九州で開催されます。

NII Shonan School on Coq 参加報告


NII Shonan School on Coq に参加して来ました。

Coq というのは定理証明支援系のソフトウェアです。関数型言語に興味のある方の中にはカリー=ハワード対応という言葉をご存知の方もいるのではないかと思いますが、これはプログラム⇔証明、型⇔命題という対応がある、というものです。Coq は依存型という、通常の静的型付け言語 (Haskell とか Scala など) より強力な型システムを用いることで、述語論理 (「全てのεに対して、あるδが存在して、どうのこうの」の様な量化子を含んだ式を表現出来る論理) の証明に対応するプログラムを書き、そしてその証明が正しいかを型検査することで機械的に確認出来ます。

じゃあ Coq を使うと何が良いのかというと、まず数学的な定理の証明を機械検証可能な形で証明出来ます。最近だとケプラー予想の機械的証明が話題になりましたね。他にも四色問題などが定理証明系の上で証明されています。どちらも数学者の人力では証明の検証が難しい問題です。
それとは別に、ソフトウェアが満たすべき仕様を述語論理で記述して、プログラムを実装し、実装が仕様を満たすことを証明出来ます。ユニットテストなどのテストでは網羅的でなかったりなどの問題がありますがCoqを使えばそのような問題はありません。
では、そんな素晴らしいツールがなぜ世の中で広く使われていないのかというと…単純に証明を書くのは難しいからです。Coqで証明を書くにはCoqの技術を磨く必要があります。
そしてその機会が、今回のセミナーという訳です。

セミナーは、葉山のセミナーハウスにて合宿形式5日間コース(半日の鎌倉見物含む)で開催され、内容はCoqの開発元のINRIAから訪れた講師によるCoqチュートリアルでした。
朝から夕食の時間までCoqに関する授業あるいは課題による実習、その後も解けなかった問題を寝るまで解く、というハードな毎日でした。私自身はここんとこあまりCoqで何かを証明してなかったので、多少錆び付いていたCoqのスキルを取り戻す良い機会でした。

残念ながら講義資料は参加者以外に公開されていない様です(パスワードで保護)。ただ、Coq については名古屋のProofCafeや、東京だとSF読み進捗ダメです会議 #9 #readcoqart #Coq(こちらは私も参加しています)といった勉強会が定期開催されているので、興味があれば参加されるとCoqについて学べると思います。