『Software Foundations vol.3』レビュー

概要

『Software Foundations』（『ソフトウェアの基礎』）という無料のオンライン教科書があります。大学院の学生を想定している6巻構成のテキストで、Coqを使って、プログラムやアルゴリズムの形式証明をしながら、ボトムアップでソフトウェアの各種構成部品を作っていくものです。

Vol3.の練習問題を一通り終わらせたので、アウトプットをします。具体的には、Vol3. において扱われた考え方や興味深い課題を紹介します。

参考リンク:

• SoftwareFoundations 公式
  • 公式。ペンシルバニア大がホスト。年１程度で改稿され続けています
• 『Software Foundations vol.1』レビュー
  • 私によるvol 1. のレビューです

#01. 場合分け分析の二つの手法 ～sumboolとreflect～

出典: Perm.v, Decide.v

bool値はいつも場合分け分析ができます。例えば x:bool に対して destruct x eqn:?などのタクティックを使えば x=?true の場合と x=?false の場合とに分岐します。一方 Propに対しては場合分け分析はできません。例外としてコンテキストや環境に H:P∨~P や H:P∨Q がある時には destruct H とすることで P の場合と ~P や Qの場合とに分岐します。

というわけで、個別の Prop については場合分け分析ができることが多いのですが、その際に計算を伴うことが多いため簡約を推し進めるようにもしておきたいところです。つまりPropでの定理 H: P∨Q ではなくTypeでのnonopaqueな定理（計算手続きでもある定理）H: {P}+{Q}を構成するためにsumbool を使います。例えばnatでは eq_dec: forall a b, {a=b}+{a<>b} がCoqのライブラリに登録されています。nonopaqueなのでif (eq_dec 2 1) then true else false は destruct せずとも false へと簡約できます。if (eq_dec a 1) then true else false は destruct (eq_dec a 1) でa=1とa<>1に分岐すると同時に簡約できます。

場合分け分析のためのもう一つの別のアプローチがあります。Propの場合分けをBoolの場合分けへと翻訳するのです。つまり「P:Propの成立 ⇔ b =? trueの成立」と「~Pの成立 ⇔ b=?falseの成立」というようにPと連動するような b:bool を構成すると場合分け分析ができるのです。その際の道具立てが reflect型です。なお、より一般に「P:Propの成立 ⇔ b =? trueの成立」と「Qの成立 ⇔ b=?falseの成立」というようにPとQと連動するbを構成できる場合にの道具立てはBoolSpec型です。いくつか例をあげます:

• 関数x=?y は x=y をリフレクトする意図で構成されています。その証明項は eqb_reflect という名前でCoqに登録されています。
• 関数x<?y は x<y をリフレクトする意図で構成されています。その証明項は leb_reflect という名前でCoqに登録されています。
• 同じ関数 x<?yは x<yと y<=x とに連動する意図で構成されているともいえます。そのBoolSpecの証明項は leb_spec という名前でCoqに登録されています。

reflect型/BoolSpec型をもつ項をdestruct することで場合分け分析ができます。例えば destruct (eqb_reflect a b) をすると H:a=b と H:a<>b とに分岐します。なお、Boolでの値を知りたい場合にはTipsが必要です。以下のように destruct する前に値を知るための領域をコンテキストに確保しておくのです:

Goal 4 <> 5.
Proof. 
assert (H:= eqb_reflect 4 5). (* H : reflect (4 = 5) (4 =? 5) *)
remember (4=?5) as b.         (* Heqb: b= (4=?5) *)
destruct H. discriminate.     (* Heqb: true=(4=?5) *)
assumption.                   (* Heqb: false=(4=?5) *)
Qed.

まとめます。Propの場合分け分析の手法は, sumbool を使った方法と、reflect/BoolSpec を使った方法の二つがあります。できることは同じです。sumbool を使った方法は Bool の世界を経由しないので多くの場合すっきりと書けます。 reflect/BoolSpec を使った方法は Bool の世界での追従物を構成する分だけややこしいものの、BoolとPropを行ったり来たりするのが楽になります。reflectで場合分けできるようにしておくと対応するsumboolの方は reflect_dec で簡単に作れます。

02. 仕様と実装～ADTへの道～

出典: Sort.v, Merge.v, Selection.v, SearchTree.v, Multiset.v, ADT.v

プログラミングの世界において、「実装が正しい」と主張するためには、実装が仕様に準拠していることを確認します。仕様をテストケースにおとしこみ、実装がテストをパスすることを確認できれば「実装がおおよそ正しい」とみなすわけです。一方Coqでは仕様に準拠していることを直接証明できるので「実装が正しい」ことが証明できます。

例えば、マージソート・選択ソート・交換ソートといった異なる３つのアルゴリズムの正しさは、「ソートアルゴリズムである」⇔「入力リストと出力リストが同一要素で構成され、かつ、出力リストがソート済みである」を証明することで正当化できます。

もう一つの例は Map型（連想記憶型や辞書型などともよばれます）です。これはリストを使って実装できますし、関数を使って実装できますし、二分木を使って実装することもできます。重要なのはMap型がどう実装されたかではなく、その性質・振舞いです。つまり、Map型に固有の操作があり（例：キーから値を引く、キーを指定して値を更新する等々）、Map型に固有な振舞いをする（キーの値は、別のキーでの更新に依存しない等々）という点です。各実装はこれらの性質を証明できることで正しさを確認できます。

天下り的・代数学的・公理的に仕様を定義した型をADTと呼びます。Map型はADTの一例であり、リストによる実装など複数のモデルを持ちます。他の例にはキューやモノイドなど色々あります。ADTに適切な振舞いを定義していれば、ADTの性質やADTを使った構成物の性質の分析に、モデル固有の性質は不要です。実装を忘れてしまっていいというわけです。特徴的な文章を ADT.v から引用します:

Note what we've happily achieved: we can reason about the behavior
of an ADT entirely from its specification, rather than depending
on the implementation code. This is what specification comments
in interfaces attempt to achieve in real-world code.

03. 実装の検証～もう一つのアプローチ～

SearchTree.v, ADT.v,

仕様を定めて実装を検証する方法は、直接ADTを型にもつ値を構成するだけではありません。

それは、参照モデルM0を経由して各実装の検証をするものです。Model based specificationといいます。M0をベースに、M1,M2,....とモデルを改良――例えばパフォーマンス向上――させていくときに便利な方法です。一般的にいって M1,M2,... が複雑になるにつれ、それらが意図したとおりの振る舞いをするのかを検証するのが難しくなっていきます。そこで、M1,M2,...上の実装の振舞いを何らかの形で M0での実装の振舞いとして翻訳・関連づけられれば、M1がM0と同じ挙動をすることが保証されるという考えです。その目的で導入されるABSと名称されがちなモジュールは、ADTのインターフェースに加え、M0への翻訳Absが上手くいくための公理*_relateを含ませます。以下のようなイメージです

• キュー型を実装したい。単リストを使って簡単な実装M0ができた。さて、性能上の問題があるため、双リストを使った実装M1も作ってみたが、これが仕様を満たすか怪しい。まず、M0の内部実装の list とM1の内部実装である list*list がどう対応づくかについての関数 Abs:list*list->list を構成する。それを使い各インターフェース――例えばエンキュー――についてM0とM1が適切に対応しているかを確認する。つまり「M0実装でのエンキューという操作は、M1実装でのエンキューという操作と一致する（対象のAbsを前提として）。

テクニカルノート

■ 関数の停止性に関する３つの工夫

出典: Merge.v, Select.v

マージソートにおける merge はそのままでは停止性を満たしません。一回のループで二つの引数のどちらかは必ず小さくなるので人間からみれば停止性は明らかですが……。そこで関数定義の中でヘルパ関数merge_auxを定義してそれを呼び出すという形にすることで停止性を保証します。merge本体は第一引数、merge_auxは第二引数が小さくなるからです。

マージソート本体 mergesort に関してもそのままではCoqが停止性を保証できないので、Function mergesort l {measure length l} := というように、停止性を入力リストの長さを指標とすることで無事に定義できます。なお、Functionで定義すると、mergesort_equationという1ステップ実行の式が自動で得られます。simpl ではめちゃくちゃになるのでこれを使うと分析が楽になります。また、便利な帰納原理も得られます。

選択ソートにおける selsort は停止性を証明できません。しかし 停止する再帰の深さが理論上確定するので、それを燃料/fuel として引数に渡し、再帰のたびに燃料を減らすという形でCoqに停止性を保証させています。別解として Function selsort' l {measure length l} := で定義もしています。

■ subset typeで represent invariantを消す

出典: ADT.v

ADTの公理には representation invariant を含むことが多いです。ADTが持つ要素の型t に対してADTの公理の多くが forall (x:t), P x -> ... という形式になるということです。具体例として Map型を二分木で実装することを考えます。木構造はどんな木構造でもよいわけではなく、左ノードの値が右ノードの値より大きくなっているような性質 BST を満たしていないといけません。なので性質の多くは forall t, BST t -> .... のような形をとります。それを反映したADTにおける公理もまた、そのような形式になるのは納得のいくところです。

それを踏まえたうえで、このinvariantを消去する方法があります。要はADTの要素 tの型を、tに論理的な制限を付けた型にすればよいのです。subset型を使うと上手くいきます。先の例では、要素の型を t ではなく {t|P t} にしてしまえばいいのです。各種公理は、要素を取り出す sig_proj1 などを使った修正が必要となりますが、ADTを使う側からすると、公理がよりシンプルになるので、ひと手間かけてADTを修正する価値はあります。

■ FMap を使ってみる

出典: Color.v

Coqの標準ライブラリを眺めると集合に関するFMap系のライブラリがあるのに気づきます。しかしどう使っていい物やら訳が分からないうえ、インターネット上で検索しても使い方を見つけるのが難しいです。Color.v の前半部はFMapの使い方を丁寧に説明しています。具体的には、Coq標準ライブラリのFMap, FSet を Positive型 をkey としたモデル PositiveSet で使います。現在では MSet の方を使うべきなのですが、FMap で感触をつかんでおけば MSet でも全く同様にして使えます。

■ Ltac を真面目にやらないと証明がきつい

出典: RedBlack.v

ある程度レイヤの高い命題の証明では、場合分けの数が膨大になります。そこでLtacを自分で定義して「コンテキストに……があれば……を呼び出す」など条件分岐・パターンマッチなどの制御構造を含んだone-offなLtacを作ったり、制御構造を含んだone-offなGareillaコード片を作る必要があります。RedBlack.vのある定理ではなんと60+もの分岐がでてくるので自動化は必須です。

■ 実装したアルゴリズム・データ構造

• ソート
  • ソートの３つの定義とその同値性 (Perm.v)
  • アルゴリズム: 選択ソート(Sort.v), 挿入ソート(Insert.v), マージソート(Merge.v)
  • ソートの定義における Permutationに関する定義 を Multisetに関する同値な定義がありうることの検証(Multiset.v)
• Map型
  • List での実装, 関数での実装
  • 二分木での実装 (SearchTree.v)
  • バランスされた二分木での実装 RB
  • 列挙 elementsによるリストとMapの間の完全性
• キュー型
  • １つもしくは２つのリストを使ったキュー実装 (ADT.v)
  • 優先度付きキューの実装 (Priorityqueu.v)
• subtype 実演 (ADT.v)
• FMapの使用法とColor問題への適用

05. 感想

世間一般でイメージされているCoqの使われ方の勉強という感じでした。Vol1（Coqの使い方）, Vol2 （操作論的意味論やラムダ計算）はそれはそれで興味深いのですが、Vol 3でやったようなあれこれの方が何かと役に立ちそうな気がします。後半は論文を読まないと進めないところがあったので流してしまった部分があり、しばらくしたらやり直そうかと思います。