8

いくつかの不変条件と組み合わせた誘導を使用して、アルゴリズムの正当性を証明する方法を理解するのに苦労しています。つまり、不変量はどのように検出され、帰納的仮説はいつ使用されますか？特に二分探索の場合はどうでしょうか？私はまだ直感的な反応を見つけることができなかったので、誰かがここでこのトピックに光を当てることができることを望んでいました。

4

4 に答える 4

13

二分探索が次のように定義されていると仮定しましょう。

def binary_search(a,b,e,x):
  n = e-b
  if n==0: return None
  m = b + int(n/2)
  if x<a[m]: return binary_search(a,b,m,x)
  if x>a[m]: return binary_search(a,m+1,e,x)
  return m

どこ

  • aは値の配列です-ソートされていると想定されます
  • [b、e）は、bからeまでの範囲であり、bを含みますが、eは含まれません。これは、検索対象です。
  • xは私たちが探している値です

この関数の目的は、iの値が存在する場合はa [i] == xである場合はiを返し、それ以外の場合はNoneを返すことです。

binary_searchは、サイズがゼロの範囲で機能します。

  • 証明：範囲に要素が含まれていない場合、n == 0であり、関数はNoneを返します。これは正しいです。

binary_searchが0からnまでの任意のサイズの要素の範囲で機能すると仮定すると、バイナリ検索はサイズn+1の要素の範囲で機能します。

  • 証拠：

    配列はソートされているため、x <a [m]の場合、すべてのk>mに対してx<a[k]です。これは、範囲[b、m）のみを検索する必要があることを意味します。範囲[b、m）は必然的に範囲[b、e）よりも小さく、バイナリ検索はn + 1より小さいサイズのすべての範囲で機能すると想定しているため、[b、m）でも機能します。

    x> a [m]の場合、同様のロジックが適用されます。

    x == a [m]の場合、関数はmを返します。これは正しいです。

于 2012-12-04T05:59:41.853 に答える
5

ソートされた配列がであると仮定しましょうa[0...n]。二分探索は、この配列を再帰的に3つの部分に分割することで機能します。中央の要素mは、左側の部分がすべての要素であり<= m（配列は仮定によって並べ替えられているため）、右側の部分はすべての要素が含まれています>=m（これも配列であるため）。仮定によってソートされます）。

不変量を定式化する方法は？

まず、二分探索がどのように機能するかを考えてみましょう。キー（検索対象のアイテム）がk真ん中の要素と比較した場合m。

  1. の場合k = m、私は自分のアイテムを見つけました（これ以上何もすることはありません）

  2. に表示される場合、配列のその部分のすべての要素がであるため、配列の右側の部分に表示されないk < m ことは確かです。したがって、配列の左側の部分に表示される必要があります（表示される場合）ka>= m > k。

  3. もしそうなら、私は確かに知っていますk > m .....。

では、このような再帰的計算の各ステップで何を保証できるでしょうか。各ステップで、2つのインデックスを識別し、「がその要素である場合は、その間に表示される必要がある」i, jと主張できます。これは、すべての再帰ステップに当てはまるため不変であり、各ステップで、アイテムが見つかるか、この範囲が空になるまでこの範囲を絞ります（範囲は空ではありません）。ka[0...n]i, ji, ji < j

誘導はどのように機能しますか？

  • 基本ケースの場合はi = 0, j = n。不変量は自明に成り立ちます。

  • 帰納的ステップの場合、不変量がいくつかの再帰的ステップに対して成り立つと仮定しpますi = i_p & j = j_p。そして、次の再帰ステップのためにi, j、不変条件がまだ保持されるように更新されることを証明する必要があります。ここで、上記の手順2）および3）の引数を使用する必要があります。

  • 範囲i, jは厳密に減少しているため、計算を終了する必要があります。

私は何かを逃しましたか？

于 2012-12-04T15:15:58.757 に答える
3 
/** Return an index of x in a.
 *  Requires: a is sorted in ascending order, and x is found in the array a
 *  somewhere between indices left and right.
 */
int binsrch(int x, int[] a, int left, int right) {
  while (true) {
    int m = (left+right)/2;
    if (x == a[m]) return m;
    if (x < a[m])
    r = m−1;
    else
    l = m+1;
  }
}

重要な観察は、binsrchが分割統治法で機能し、何らかの方法で「より小さい」引数に対してのみそれ自体を呼び出すことです。

P（n）を、右左=nの入力に対してbinsrchが正しく機能するというアサーションとします。P（n）がすべてのnに対して真であることを証明できれば、binsrchがすべての可能な引数で機能することがわかります。

規範事例。n = 0の場合、left = right=mであることがわかります。xが左右の間にある場合にのみ関数が呼び出されると想定したため、x = a [m]の場合である必要があります。したがって、関数は配列aのxのインデックスであるmを返します。

誘導ステップ。binsrchは左右≤kである限り機能すると仮定します。私たちの目標は、左右= k+1の入力で機能することを証明することです。x=a[m]、x <a [m]、x>a[m]の3つのケースがあります。

    Case x = a[m]. Clearly the function works correctly.

    Case x < a[m]. We know because the array is sorted that x must be found between a[left] and a[m-1]. The n for the recursive call is n = m − 1 − left = ⌊(left+right)/2⌋ − 1 − left. (Note that ⌊x⌋ is the floor of x, which rounds it down toward negative infinity.) If left+right is odd, then n = (left + right − 1)/2 − 1 − left = (right − left)/2 − 1, which is definitely smaller than right−left. If left+right is even then n = (left + right)/2 − 1 − left = (right−left)/2, which is also smaller than k + 1 = right−left because right−left = k + 1 > 0. So the recursive call must be to a range of a that is between 0 and k cells, and must be correct by our induction hypothesis.

    Case x > a[m]. This is more or less symmetrical to the previous case. We need to show that r − (m + 1) ≤ right − left. We have r − (m + 1) − l = right − ⌊(left + right)/2⌋ − 1. If right+left is even, this is (right−left)/2 − 1, which is less than right−left. If right+left is odd, this is right− (left + right − 1)/2 − 1 = (right−left)/2 − 1/2, which is also less than right−left. Therefore, the recursive call is to a smaller range of the array and can be assumed to work correctly by the induction hypothesis.

すべての場合で帰納的ステップが機能するため、binsrch（およびその反復バリアント）は正しいと結論付けることができます。

x> a [m]の場合のコーディングを間違え、mをm + 1ではなく左として渡した場合（簡単です！）、作成したばかりの証明はその場合は失敗することに注意してください。実際、右=左+1の場合、アルゴリズムは無限ループに入る可能性があります。これは、注意深い帰納的推論の価値を示しています。

参照：http ：//www.cs.cornell.edu/Courses/cs211/2006sp/Lectures/L06-Induction/binary_search.html

于 2012-12-04T05:38:53.400 に答える
1

二分探索の各ステップの後にそれを証明する必要がありますarr[first] <= element <= arr[last]

これと終了から、二分探索が終了すると結論付けることができますarr[first] == element == arr[last]

于 2012-12-04T05:59:01.233 に答える