|
不変条件不変条件（英: invariant）とは、コンピュータプログラムの理論における用語で、ある処理の間、その真理値が真のまま変化しない述語 (predicate) であり、その処理シーケンスに対して不変であるという。 用法コンピュータプログラムは一般にそれを実行したときの変化で表されるが、プログラムの不変条件が何であるかを知ることも同様に重要である。これは特にプログラムについて推論するときに便利である。コンパイラ最適化の理論、契約プログラミングの方法論、プログラムの正しさを判定する形式手法など、いずれもプログラムの不変条件を重視している。 プログラマはコード内でアサーションをよく使い、不変条件を明確化する。一部のオブジェクト指向プログラミング言語にはクラス不変条件 (class invariant) を指定する特別な構文がある。 例論理問題での不変条件の特定が便利であることを示すため、MUパズルを例に用いる。このパズルは次の規則からなる。
この4つの規則だけで MI から MU に変換できるか、というのがダグラス・ホフスタッターの考案したMUパズルである。 このパズルをやってみると何時間でもつぶすことができるかもしれない。しかし、全ての規則に対して不変である述語を探し、MU を作ることができないと示す方が早い。論理的に見てみると、I を取り除くには I が3つ連続していなければならない。このことから、次のように興味深い不変条件が導かれる。
この条件が不変条件と言えるのは、この条件が事前に成り立っている場合に、どの変換規則を適用した後も常に同じ条件が成り立っていると言える場合である。各変換規則が I と U の個数に与える効果を見てみると、この条件が不変条件だとわかる。
上の表を見れば明らかなように、この不変条件はどの変換規則を適用した後も成り立つ。したがって、最初に I の個数が3の倍数でないなら、どの規則をどういう順序で適用しても I の個数は3の倍数にはならない。 MI という文字列には I が1つしかなく、3の倍数ではない。MU には I が 0 個あり、0は3の倍数である。したがって、MI から MU への変換は不可能である。 参考文献
関連項目外部リンク |
