Software Foundation vol.1を読んだ

Coqやソフトウェア検証の入門書として知られるSoftware Foundation(以下SF)シリーズのvol.1,Logical Foundationを読むグループを学科で立ち上げて,3年生が始まる前の春休みに皆で読んでいた。3年生の前期が始まると忙しくて中断してしまったが,夏休みに入って私だけ(?)がまた続きを読み始めて,なんとか最後まで読み切ることができた(Exerciseは9割以上は解いた)。ざっくりと感想などを書いてみようと思う。

Software Foundation (SF)とは?

https://softwarefoundations.cis.upenn.edu/

ソフトウェア検証と,その背景にある概念を解説している入門的な教科書シリーズ。『型システム入門(TaPL)』の著者でもあるBenjamin C. Pierceや,"Modern Compilers in ML(タイガー本)"で知られるAndrew Appelなどが中心となって書いている。現在でもこのシリーズの執筆は続けられていて,この記事を書く2週間前くらいまでは3巻構成だったが,ついこの間vol.4が追加された。

余談だが,Princeton, Pennsylvania, MIT, Yaleという東海岸の4大学の検証系の研究者達によるDeepSpecというグループがあって,このSFの著者たちも所属している。そのDeepSpecが主催しているサマースクールでもSFが教材として使われているらしいのだが,今年のサマースクールではSFの公開されている4巻分のみならず,Verifiable Cという未公開の新刊と思われるものも使われていたらしく,これがSFの次のvolumeになるのではないか,と言われているらしい。

感想

読み始める前に

当該Webページで配布されている教材の中には,各章の本文と,そこで使われているサンプルコードを含んだCoqのファイルが含まれているので,ダウンロードしてから使うと良い。 本文がすべてCoqファイルのコメントアウトの中に書かれているのは最初はおどろくが,文章を追いながらその場でCoqを試してみることができるので捗ってよいと思う。

Basics.v〜Tactics.v

Coqの言語でのデータ構造の定義の仕方とか,パターンマッチとか多相性といったような関数型っぽい話がある。と同時に,基本的な証明テクニックも学んでいく。OCamlなどの関数型言語をすでに学んだ人にとっては結構退屈なパートも多いかもしれない。

Basics.vで,Coqの関数は引数の少なくとも1つが確実に減少していなければならないという話があったが,これは実はあとのImpCEvalFun.vでも出てくる通り,停止しない関数を定義するとFalseが証明できるようになってしまうためらしい。面白い。

ここらへんの章(とLogic.v)を読んでいたのが3年生の前期が始まる前で,半年くらい前なので,ほとんど記憶がない。

Logic.v

これまでとは雰囲気が少し変わって,論理記号( \land, \lor, \lnotなど) を扱った証明ができるようになる。古典論理直観主義論理の違いみたいな話も出てくる。最後のExerciseが,古典論理を使って初めて示すことができる命題5つ(パースの法則とか)の同値性を示すというものでなかなか時間がかかった。示す順番を変えたほうがいいのか?とも思ったが,難しいことは考えずに出てくる順番に示す(排中律→パース,パース→二重否定除去,...)のが正解っぽい。

IndProp.v

帰納的に定義される述語を扱う章。今まではデータ型の構成に関する帰納法しか使っていなかったが,この章では述語の構成に関する帰納法を使って証明することを学ぶ(述語の証明をするにあたって,証明木の構成に関する帰納法を回すみたいなイメージ)。

帰納法をテーマにすると難しい問題もつくれてしまいがちなのか,この章はやたらと難しい問題が多く,最難関のlevel5の問題が3つもある。私は問題を基本的には解く主義だったのでこれらにも挑戦しようとしたが,pumpingとpalindrome_converseは悲しいことにまだ解けていない。pumpingに関してはMStarAppのところの帰納法のstep caseが回せず,palindrome_converseに至っては方針が立たない。示せた方がいらっしゃったらぜひ教えていただきたいなぁ。

この章まででCoqの基本的なタクティックの解説がほぼ終わってくる。この章は問題数も多いが,頑張ると結構証明の力がついた気がして成長を感じられる。

Maps.v

Coqで全域写像,部分写像を表現してみる章。短くて内容も簡単な息抜きみたいな章。ここで定義したMappingの型は,後のImp.vの章で,変数とその値を保存している,環境のようなものとして使われる。

ProofObjects.v

Curry-Howard同型を解説している章で,証明(Proof editing modeで使っているタクティックの列)とプログラム(関数やコンストラクタ適用の連続)が対応している,ということが実際のCoqのコードを見ながら実感として理解できるようになる。

あとは,Curry-Howard同型に関連して,全称量化子forallを使った命題は全域関数に対応づけることができるので一番基本的で,その他の論理記号( \land, \lor, \existsなど)やTrue, Falseなどの命題はすべてCoqの上でInductiveに定義されているのだという話が紹介される。ここを読むと,例えばなぜinversionによって H: P /\ Q のような仮定が H1: P, H2: Q のように分解されるのかなどがわかってなるほどという気持ちになる。

Exerciseでは,命題が与えられて,その証明をプログラムとして書きましょう,みたいな問題が多いが,提示されている難易度の割には結構難しかったと思う。あとはLeibniz Equalityの話が出ていて,これはlevel5の割にはシンプルに証明できた気がする。

IndPrinciples.v

CoqでInductiveなデータ型や述語を定義すると,自動的に[定義したものの名前]_indという規則が自動で生成される。例えばnatという型をInductiveに定義するとnat_indという規則が生成されて,内容は(ペアノの公理の)数学的帰納法の原理みたいな感じになる。この章ではInductiveな定義と,そこから生成される*_indの規則の対応を学ぶということをする。inductionタクティックが本質的には,apply *_ind.のsyntax sugarでしかないということがわかってへぇーという気持ちになる。

Rel.v

二項関係の性質を色々示していく章。同値関係とか半順序とかpreorderとかそのへんのお話。natについての(特に<=<についての)自明な補題を示すのに手間取ったりして結構しんどかった。

Imp.v〜ImpCEvalFun.v

vol.2でのプログラム検証の話のための準備と思われる話がされている。Impという,Cライクな小さい(といってもwhile文やif文くらいは使える)手続き型言語を定義して,それで書かれたプログラムを実行すると環境がどう変わるかとか,Impプログラムが決定的であるとか,停止するかどうかといった議論を証明によって行う練習をする。

Impプログラムの評価に関して,これを関数(Fixpoint)を使った実装にすると,一見停止性が保証されないようなプログラムになってしまってCoqが通してくれない。このため,Imp.vではプログラムの評価を関数ではなく述語として定義している。一方ImpCEvalFun.vでは,少し工夫することによってImpの評価器を関数で実装している。

ImpParser.vは,このImpプログラムを実際にどうやって字句解析・構文解析するか,という話で,ひたすらそれを実装するCoqのコードが並んでいる。言葉による解説は少なく,練習問題もなく,ざっと一通りのコードを実行して字句解析器・構文解析器がCoqで実装できるということを実感できればそれでよさそう。

あとImp.vではCoqの便利なタクティックを色々紹介されるのだが,その中にomegaがある。omegaタクティックはプレスバーガー算術というものを使っていて,この算術は決定可能であるという話に興味をそそられたので色々調べてみたが,なぜ決定的なのかはわからなかった…

Extraction.v

名前の通り,Coqのextraction(CoqのプログラムをOCamlHaskellなどのプログラムに変換する機能)の使い方を解説している。

Auto.v

auto, eapply, eautoタクティックなどの解説がある。Coqは賢いなぁという気持ちになる。練習問題がないのが少し悲しい(あってもすべてautoで終わってしまうからかもしれないが)。

まとめ

vol.1はCoqそのものについての解説に紙面を大量に割きつつ,次のvolumeにつながるような話が少しあるという感じだった。結構分量が多くてExerciseを全部解こうとすると時間がかかるので,適度にとばすのが良いかもしれない。

あと個人的な感想だが,夏休みの2ヶ月間はずっとフルタイムインターンをしていた(というか今もしている)ので,Coqの学習は出社前と出社後に毎日ちまちまと進めていたわけだが,やはり1日に2時間くらいしか割けないので進捗が芳しくなくてもどかしい思いをした。社会人になってから勉強するのが難しいというのはこういうことなんだろうなぁ,と実感したので潤沢な時間がある学生のうちに色々やっておきたいものだ。

vol.2も引き続きこつこつ読んでいきたい。