帰納法と余帰納法にまつわる伝承

これはAmusement Creators Advent Calendar 2017の14日目の記事です.

adventar.org

最小不動点と最大不動点のよく知られた話とか時相論理に絡めた話をゆるゆるっとするつもりです.
分かりにくかったり変なことを言っていれば気軽にご指摘ください.
記事を書き終わった後に見返してみるとかなりぐだぐだしてます.

先に記号の説明をしておきます.

  • [] ... 空の列
  • [e1, e2, e3] ... 先頭から順に要素がe1, e2, e3であるような列
  • e :: l ... 列lの先頭に要素eを付け加えてできる列

例えば[1, 2, 3]1 :: 2 :: 3 :: []は同じものです.

それと,出てくる関数 Fはすべて単調であると思ってください.

帰納法(最小不動点

次のような列の集合を受け取って列の集合を返すような帰納的な関数を考えましょう.
帰納的というのは「もしxが性質Pを満たすならxをもとにして作ったものもPを満たす」という性質のことです.

 {\begin{align}
F(X) = \{[\;]\} \cup \{ 1:: x \mid x \in X \}
\end{align}}

ここで関数 Fについて閉じている(つまり F(X) \subseteq Xである)ような集合のうち 最小 のものを Fについての最小不動点といって\mu Fと書きます.
関数 Fについて閉じている集合としては例えば

 {\begin{align}
\cdot\quad & \{[\;], [1], [2], [1, 1], [1, 2], [1,1,1], [1,1,2], \cdots\} \\
\cdot\quad & \{[\;], [1], [1, 1], [1,1,1], [1,1,2], [1,2,3], [1, 1, 1, 1], [1,1,1,2], [1,1,2,3], \cdots\}
\end{align}}

などがあり,その中でも最小のもの,つまり最小不動点は直観的にはすべての要素が1であるような列すべてからのみなる集合です.

一般的に最小不動点の近似解を求めるにはKnaster-TarskiとCousot-Cousotという二つの手法が知られています.

Knaster-Tarski

こちらの手法はかなり定義通りで, F(X) \subseteq Xをみたすような集合 Xすべてを計算してそのintersectionを取ります.
しかし現実的には F(X) \subseteq Xを満たす集合 Xすべてを計算するのは難しいので見つかった範囲でのすべての集合のintersectionをとることになります.
見つかった集合が多ければ多いほど近似で得られる集合は小さくなって最後には \mu Fそのものになるので,この近似で得られる集合を Sとすると \mu F \subseteq Sが成り立ちます.
つまりこれは \mu Fの過大近似を求める手法です.

Cousot-Cousot

こちらの手法でのアイデアは「余分なものを含まずに必要なものだけを集めたら最小のものになるはず」です.空集合を初期状態として集合が Fについて閉じたものになるまで必要な要素を追加していきます.
先ほどの例だと

 {\begin{align}
S_0 &= \emptyset \\
S_1 &= F(S_0) = \{[\;]\} \\
S_2 &= F(S_1) = \{[\;], [1]\} \\
S_3 &= F(S_2) = \{ [\;], [1], [1, 1] \} \\
S_4 &= F(S_3) = \{ [\;], [1], [1, 1], [1, 1, 1] \} \\
\end{align}}

と展開していって S_{n+1} = S_nとなるようなnがあれば \mu F = S_nだ,ということです.
もちろんそんなnがいつも見つかるわけでなく,どこか上限を決めて打ち切らないといけません.
無限回繰り返していれば追加されるような要素がこの近似で得られた集合Sには含まれていないかもしれないので, S \subseteq \mu Fであることがわかります.
つまりこれは \mu Fの過小近似を求める手法です.

帰納法(最大不動点

次のような列の集合を受け取って列の集合を返すような余帰納的な関数を考えましょう
帰納的というのは「もしxが性質Pを満たすならxの部品もPを満たす」といったような性質のことです.

 {\begin{align}
F(X) = \{ x \mid (1 :: x) \in X \}
\end{align}}

ここで関数 Fについて整合している(つまり X \subseteq F(X)である)ような集合 Xのうち 最大 のものを Fについての最大不動点といって\nu Fと書きます.
この場合の最大不動点は直観的には1の無限列からのみなるような集合です.

一般的に最大不動点の近似解をもとめるには最小不動点と同様にKnaster-TarskiとCousot-Cousotの二つの手法が知られています.

Knaster-Tarski

やはりかなり定義通りで, X \subseteq F(X)をみたすような集合すべてを計算してそのunionを取ります.
しかし現実的には X \subseteq F(X)を満たす集合すべてを計算するのは難しいので見つかった範囲でのすべての集合のunionをとることになります.
見つかった集合が多ければ多いほど近似で得られる集合は大きくなって最後には \nu Fそのものになるので,この近似で得られる集合を Sとすると S \subseteq \nu Fが成り立ちます.
つまりこれは \nu Fの過小近似を求める手法です.

Cousot-Cousot

こちらの手法でのアイデアは「いらないものを捨てていけば最後にはいるものだけ残るはず」です.全体集合を初期状態として集合が Fについて整合したものになるまでいらない要素を除去していきます.
これまた全体集合が無限集合だと何回いらない要素を除去しても終わらないことがあるのでどこかで操作を打ち切る必要があります. 無限回繰り返していれば除去されるような要素がこの近似で得られた集合Sには含まれているかもしれないので, \nu F \subseteq Sであることがわかります.
つまりこれは \nu Fの過大近似を求める手法です.

まとめ

以上をまとめると

過小近似 過大近似
最小不動点 Cousot-Cousot Knaster-Tarski
最大不動点 Knaster-Tarski Cousot-Cousot

って感じです.

帰納法(最小不動点)と余帰納法(最大不動点

最小不動点の定義と最大不動点の定義を並べてみましょう.

  • 最小不動点 ...  F(X) \subseteq X であるような Xのうち 最小 なもの
  • 最大不動点 ...  X \subseteq F(X) であるような Xのうち 最大 なもの

きれいに対応づいていることが分かると思います.
この対応はめっちゃ綺麗で, \land \lorの対応ぐらい綺麗でかっこいいです.

モデル検査と帰納法・余帰納法

最大不動点の例で出した1の無限列は何かの最小不動点の要素になりえるでしょうか?
実はそうはなりません.なぜかというと最小不動点はベースケース(例だと空列)を用意してそこから構成できるものを集めたものなので必ず終わり(ベースケース)を含んでおり,無限であるようなものは表せないからです.
そう,最小不動点の要素であるような列はかならず有限なので先頭から順番にパクパク要素を食べていくとかならずベースケースに到達するのです.
この性質から最小不動点は「いつか必ずベースケースを満たす」という意味を持つと読むことができます.
逆に,余帰納法は性質Pを満たすものを何回分解しても性質Pを満たすことを表しているので最大不動点は「いつも必ず性質Pを満たす」という意味を持つと読むことができます.
これは「いつか」とか「いつも」とか言っているので時間に関する制約だとみることができて,まさに,まさに,様相論理の一つである時相論理のFとGに対応します.

こういうわけで最小不動点や最大不動点は時相論理と深い関係にあります.

nyan

最小不動点と最大不動点が入り組んだ制約の解析はある条件を満たせばパリティゲームというゲームの必勝戦略が存在するかという問題に帰着できてゲーム理論とも関係があったりします.

もちろんこの記事で余帰納法について述べ切れているわけではありません(そもそも僕は勉強している途中なので).
帰納法帰納法との綺麗な対応関係やその他もろもろはとても面白いのですが,余帰納法知名度帰納法に比べてとても低いように感じられるのが残念です.

参考になったもの

帰納法・余帰納法の説明はやはり型システム入門(Type and Programming Languages)の21章が一番分かりやすいと思います.

その他には住井先生の日記が初学者にはわかりやすかったです.
帰納法と余帰納法の何がどう双対なのか(初等的に) - sumiiの日記
余帰納的定義 - sumiiの日記

この記事はPOPL16の発表スライドを参考にしました.
http://group-mmm.org/~ichiro/talks/popl2016pub.pdf