## 定義 保存される不変条件(preserved invariant)とは、状態機械([[状態機械]])上の述語Pであって、状態qでP(q)が真であり、かつq→rという遷移が存在すれば、P(r)も真であるという性質を満たすものである。**不変条件原理(The Invariant Principle)**は、保存される不変条件が開始状態で真であれば、その状態機械のすべての到達可能な状態で真であると主張する。これは状態機械向けに再定式化した帰納法の原理そのものであり、開始状態での成立が基底部、不変条件の保存の証明が帰納段階に対応する。不変条件原理は1967年にCarnegie Tech(現Carnegie Mellon University)でRobert W. Floydによって定式化され、Floydの不変条件原理とも呼ばれる。なお、不変条件の**否定**は一般には保存される不変条件にならない(ある状態が¬Pを満たしても、遷移先の状態はPを満たしうる)。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] §5.4.3–§5.4.4) Floydはプログラムの検証を2つの性質に分解した。**部分正当性(partial correctness)**は「結果が出れば必ず要求を満たす」という性質で、不変条件原理でしばしば証明できる。**停止性(termination)**は「プロセスが必ず何らかの結果を出す」という性質で、整列原理([[整列原理]])に基づき、状態に値を割り当てる**導出変数(derived variable)**が遷移ごとに狭義単調減少することを示すことで証明できる。値域が整列集合である狭義単調減少の導出変数が存在すれば、その状態機械のすべての実行は停止する。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] §5.4.5–§5.4.6) ## 横断的知見 - 第2章の[[整列原理]]は「整列集合の値を単調減少に割り当てられれば計算は無限には続かない」という停止性証明の一般原理を第2章§2.4の時点で述べていたが、その具体的な適用対象(状態機械上の導出変数)は本ページの土台となる第5章§5.4.5–§5.4.6で初めて与えられる。第5章は、整列原理単体では抽象的だった「単調減少割り当てによる停止性証明」を、部分正当性(不変条件原理)と停止性(整列原理+導出変数)という検証の2性質への分解として具体化し、高速べき乗算プログラムの停止性(レジスタzの値が遷移ごとに半減し整数値のまま0に到達する)という実例で完成させている。すなわち第2章は原理を、第5章はその原理を計算モデル(状態機械)に落とし込む方法論を担っており、両者は「原理とその工学的応用」という相補的な関係にある。(Source: [[@2015__MIT__Mathematics for Computer Science - Chapter 2 The Well Ordering Principle]], [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]]) ## 未解決の問い - 不変条件の発見は本章では人手による洞察(南東ジャンプロボットの導出変数v(x,y):=y+x/(x+1)など)に依存しているが、不変条件を自動的に(あるいは半自動的に)発見する手法にはどのようなものがあるか。 - 弱単調減少する導出変数だけでは停止性が保証されない(値が一定のまま無限に続く実行がありうる)ことが本章で注意されているが、弱単調減少の導出変数から停止性を導くには他にどのような追加条件が必要か。 - 部分正当性・停止性という2性質への分解は、並行プログラムや分散システムの検証(ライブネス・セーフティという性質分解)とどう対応するか。 ## 関連 - source: [[@2015__MIT__Mathematics for Computer Science - Chapter 5 Induction]] - 概念: [[状態機械]] —— 不変条件が定義される土台となる抽象モデル。/ [[帰納法]] —— 不変条件原理はその状態機械向け再定式化。/ [[整列原理]] —— 停止性証明で導出変数の値域として使われる整列集合の出所。 ## 出典 - Eric Lehman, F. Thomson Leighton, Albert R. Meyer, *Mathematics for Computer Science*, revised 2015-05-18, Chapter 5.