Think Stitch
PRINCIPIA  最近の更新


多変数のループ不変条件

雷は去りました。 そこで(?)もう1つループ不変条件の話を書くことにします。

ループ不変条件のところで2種類のループ不変条件をご紹介しました。 1つは何かが溜まっていくという感じのものです。 これを累積型と呼ぶことにします。 もう1つはエネルギー保存の法則に似ているもので、いままで計算した部分と、これから計算する残りの部分とを「ある意味」合わせたものが一定であるという形をしているものです。 こちらをエネルギー保存型と呼ぶことにします。 式で書くとこんな感じです。

累積型:
エネルギー保存型:

ここで i はループ変数で、+に丸がついている演算は、問題に応じて異なる何か足し算のようなものです。 足し算そのもののこともあるし、和集合だったり、条件の成り立つ範囲の広さだったりします。

イメージを描くと次のような感じになります。

要はループ変数で示される位置のどちら側を式で表しているかというだけの違いです。

ループ変数が2個ある場合

次にループ変数が2個ある場合を考えます。 ループ変数を i, j とすると、ループ不変条件は次のような形になるでしょう。

累積型:
エネルギー保存型:

例題: ソート済み配列の共通部分

実際に例を見ることにします。 昇順にソートされた2つの整数配列が与えられたとき、この2つの配列両方に含まれている整数を求めるとします。 つまり共通部分を求めるということです。 配列はソートされていますから、前から順番に見ていけば簡単に求められます。

2つの配列を s, t とします。 結果を格納する変数 u とします。 これは集合を表すとします。 配列 v の一部分を v[i:j] で表すことにします。 これはインデックス k が i <= k < j の範囲にある部分列という意味です。 さらに集合を扱う文脈では、配列 v も部分列 v[i:j] も、含まれている整数の集合を表すとします。 特に混乱はないと思います。

事後条件は次のようになります。

u = s ∩ t

累積型ループ不変条件

すると、配列 s を i まで、配列 t を j まで見た時点でのループ不変条件を次のような形で表すことができるでしょう。

u = s[0:i] ∩ t[0:j]

これは典型的な累積型のループ不変条件です。

エネルギー保存型ループ不変条件

同じようにエネルギー保存型ループ不変条件を書くこともできます。

u ∪ (s[i:M] ∩ t[j:N]) = s ∩ t

ここで M, N はそれぞれ配列 s, t の大きさです。 ここでの「合わせる」演算は和集合 ∪ です。 右辺は定数であることを確認しておきます。

ループ条件

ところで、ループ条件はどうなるでしょうか。 ループを終了するのは、ループ変数 i または j のどちらかが、配列の終わりに達したときです。 つまり次のようになります。

ループ条件: i < M & j < N

2つの型の違い

するとループ脱出後には、この否定が成り立つことになります。 それは i >= M または j >= N です。 i, j の範囲と合わせると、i = M または j = N ということです。

これはちょっと困ったことです。 例えば i = M になったとします。 累積型ループ不変条件の場合は次のようになります。

u = s ∩ t[0:j]

j < N かもしれないので、これから事後条件はいえません。

一方、エネルギー保存型の場合は次のようになります。

u ∪ (s[M:M] ∩ t[j:N]) = s ∩ t

ここで s[M:M] は空集合ですから、s[M:M] ∩ t[j:N] も空集合になり、したがって事後条件が成り立ちます。

なぜこのようなことが起こるかというと、ループ変数が2個以上ある場合、累積型とエネルギー保存型ではカバーしている範囲が異なるのです。 イメージで描くとこんな感じです。

累積型ではループ変数の一方が終端に達しても余りの領域ができてしまいます。 一方、エネルギー保存型では、どの変数が終端に達してもすべての領域が埋め尽くされます。

そんなわけで、ループ変数が2個以上ある場合は、エネルギー保存型の方がきれいに処理できます。 もちろん累積型でも後処理を行えば証明はできますけど、あまり美しくありません。

追記

上で示したループ不変条件は正当性の証明で必要な条件の一部です。 もちろんこれ自体もループ中ずっと成立するのでループ不変条件ですけど、これだけでは条件が弱くてプログラムの正当性は証明できません。 でもこの条件が主要な項であることに違いはありません。 誤解されるかもしれないと思って書きました。

ちなみに残りの条件は・・・書くのはやめておきます。 あまり楽しみを奪っては申し訳ないので。

2013/09/02
© 2013,2014,2015 PRINCIPIA Limited