帰納法と余帰納法にまつわる伝承
これはAmusement Creators Advent Calendar 2017の14日目の記事です.
最小不動点と最大不動点のよく知られた話とか時相論理に絡めた話をゆるゆるっとするつもりです.
分かりにくかったり変なことを言っていれば気軽にご指摘ください.
記事を書き終わった後に見返してみるとかなりぐだぐだしてます.
先に記号の説明をしておきます.
[]
... 空の列[e1, e2, e3]
... 先頭から順に要素がe1
,e2
,e3
であるような列e :: l
... 列l
の先頭に要素e
を付け加えてできる列
例えば[1, 2, 3]
と1 :: 2 :: 3 :: []
は同じものです.
それと,出てくる関数はすべて単調であると思ってください.
帰納法(最小不動点)
次のような列の集合を受け取って列の集合を返すような帰納的な関数を考えましょう.
帰納的というのは「もしxが性質Pを満たすならxをもとにして作ったものもPを満たす」という性質のことです.
ここで関数について閉じている(つまりである)ような集合のうち 最小 のものをについての最小不動点といってと書きます.
関数について閉じている集合としては例えば
などがあり,その中でも最小のもの,つまり最小不動点は直観的にはすべての要素が1であるような列すべてからのみなる集合です.
一般的に最小不動点の近似解を求めるにはKnaster-TarskiとCousot-Cousotという二つの手法が知られています.
Knaster-Tarski
こちらの手法はかなり定義通りで,をみたすような集合すべてを計算してそのintersectionを取ります.
しかし現実的にはを満たす集合すべてを計算するのは難しいので見つかった範囲でのすべての集合のintersectionをとることになります.
見つかった集合が多ければ多いほど近似で得られる集合は小さくなって最後にはそのものになるので,この近似で得られる集合をとするとが成り立ちます.
つまりこれはの過大近似を求める手法です.
Cousot-Cousot
こちらの手法でのアイデアは「余分なものを含まずに必要なものだけを集めたら最小のものになるはず」です.空集合を初期状態として集合がについて閉じたものになるまで必要な要素を追加していきます.
先ほどの例だと
と展開していってとなるようなnがあればだ,ということです.
もちろんそんなnがいつも見つかるわけでなく,どこか上限を決めて打ち切らないといけません.
無限回繰り返していれば追加されるような要素がこの近似で得られた集合Sには含まれていないかもしれないので,であることがわかります.
つまりこれはの過小近似を求める手法です.
余帰納法(最大不動点)
次のような列の集合を受け取って列の集合を返すような余帰納的な関数を考えましょう
余帰納的というのは「もしxが性質Pを満たすならxの部品もPを満たす」といったような性質のことです.
ここで関数について整合している(つまりである)ような集合のうち 最大 のものをについての最大不動点といってと書きます.
この場合の最大不動点は直観的には1の無限列からのみなるような集合です.
一般的に最大不動点の近似解をもとめるには最小不動点と同様にKnaster-TarskiとCousot-Cousotの二つの手法が知られています.
Knaster-Tarski
やはりかなり定義通りで,をみたすような集合すべてを計算してそのunionを取ります.
しかし現実的にはを満たす集合すべてを計算するのは難しいので見つかった範囲でのすべての集合のunionをとることになります.
見つかった集合が多ければ多いほど近似で得られる集合は大きくなって最後にはそのものになるので,この近似で得られる集合をとするとが成り立ちます.
つまりこれはの過小近似を求める手法です.
Cousot-Cousot
こちらの手法でのアイデアは「いらないものを捨てていけば最後にはいるものだけ残るはず」です.全体集合を初期状態として集合がについて整合したものになるまでいらない要素を除去していきます.
これまた全体集合が無限集合だと何回いらない要素を除去しても終わらないことがあるのでどこかで操作を打ち切る必要があります.
無限回繰り返していれば除去されるような要素がこの近似で得られた集合Sには含まれているかもしれないので,であることがわかります.
つまりこれはの過大近似を求める手法です.
まとめ
以上をまとめると
過小近似 | 過大近似 | |
---|---|---|
最小不動点 | Cousot-Cousot | Knaster-Tarski |
最大不動点 | Knaster-Tarski | Cousot-Cousot |
って感じです.
帰納法(最小不動点)と余帰納法(最大不動点)
きれいに対応づいていることが分かると思います.
この対応はめっちゃ綺麗で,との対応ぐらい綺麗でかっこいいです.
モデル検査と帰納法・余帰納法
最大不動点の例で出した1の無限列は何かの最小不動点の要素になりえるでしょうか?
実はそうはなりません.なぜかというと最小不動点はベースケース(例だと空列)を用意してそこから構成できるものを集めたものなので必ず終わり(ベースケース)を含んでおり,無限であるようなものは表せないからです.
そう,最小不動点の要素であるような列はかならず有限なので先頭から順番にパクパク要素を食べていくとかならずベースケースに到達するのです.
この性質から最小不動点は「いつか必ずベースケースを満たす」という意味を持つと読むことができます.
逆に,余帰納法は性質Pを満たすものを何回分解しても性質Pを満たすことを表しているので最大不動点は「いつも必ず性質Pを満たす」という意味を持つと読むことができます.
これは「いつか」とか「いつも」とか言っているので時間に関する制約だとみることができて,まさに,まさに,様相論理の一つである時相論理のFとGに対応します.
こういうわけで最小不動点や最大不動点は時相論理と深い関係にあります.
nyan
最小不動点と最大不動点が入り組んだ制約の解析はある条件を満たせばパリティゲームというゲームの必勝戦略が存在するかという問題に帰着できてゲーム理論とも関係があったりします.
もちろんこの記事で余帰納法について述べ切れているわけではありません(そもそも僕は勉強している途中なので).
余帰納法と帰納法との綺麗な対応関係やその他もろもろはとても面白いのですが,余帰納法の知名度が帰納法に比べてとても低いように感じられるのが残念です.
参考になったもの
帰納法・余帰納法の説明はやはり型システム入門(Type and Programming Languages)の21章が一番分かりやすいと思います.
その他には住井先生の日記が初学者にはわかりやすかったです.
帰納法と余帰納法の何がどう双対なのか(初等的に) - sumiiの日記
余帰納的定義 - sumiiの日記
この記事はPOPL16の発表スライドを参考にしました.
http://group-mmm.org/~ichiro/talks/popl2016pub.pdf