0 
procedure bit count(S: bit string)
count := 0
      while S != 0
          count := count + 1
          S := S ∧ (S − 1)
return count {count is the number of 1s in S}

ここで、S-1 は、S の右端の 1 ビットを 0 に変更し、その右側のすべての 0 ビットを 1 に変更したビット列です。

なぜこれが正しいのか理解できたので、大まかな説明を書きました。

すべての反復の後、S の右端の 1 ビットとその右側のすべてのビットが 0 に等しく設定されます。文字列全体が 0 であり、1 の数に等しいカウントでループが中断されます。

この種の答えはどの数学コミュニティにも通用しないことを知っているので、正式な証明を書きたいと思っていましたが、それを行う方法がわかりません。私の証明スキルは特にお粗末なので、関連するテクニックの説明をいただければ幸いです。

4

2 に答える 2

1

帰納法を使用した証明は次のようになります。

主張:nアルゴリズムの th 回目の反復の開始時に、n-11 (セット) ビットとcount == n-1.

証明:
ベース:最初の繰り返しで については自明ですn==1- まだセットされたビットは見られず、カウントは 0 に設定され ています
.. 証明: n 回目の反復の後に反復が続きます。反復では、帰納的仮説から、ビット と を見てきました。 反復に達したため、反復は正常に終了しました。つまり、終了条件が満たされていないため、反転ビットがありました。あなたも 1 増やしたので、 th ステップでビット とを裏返しました。k<nn
nn-1n-1n-1count == n-1
nn-1countnncount == n

上記から、アルゴリズムが終了すると、count == #flipped_bits.

QED

上記は部分的な正しさであることに注意してください。これは、アルゴリズムが終了した場合に正しい答えが得られることを証明していますが、終了を保証するものではありません。 が得られるまで、ほとんどの場合右端のビットをフリップできるため、
多くのステップがあることを示すことによって、終了を保証することができます。（終了＋部分的正当性を完全正当性という）|S||S|S = 0

アルゴリズムの証明に興味がある場合は、Hoare Logicに興味があるかもしれません。Hoare Logic は、プログラムが正しいことを検証するための正式なツールを提供します。この研究分野は、ソフトウェア検証として知られています。

于 2012-12-05T06:57:03.160 に答える
0

まず第一に、それは正しくありません。あなたがしたいwhile S != 0、ではありませんwhile S = 0。

証明に関しては、帰納的証明を使用します。ビットが設定されていない場合に正しく機能することを証明し、少なくとも 1 つのビットが設定されている場合、カウントをインクリメントし、設定されているビット数を減らすことを証明します。 1 つ、繰り返します。

帰納的なステップで、唯一の難しい部分はS := S ∧ (S − 1)、 S に設定されたビット数が正確に 1 だけ減らされることを10..0示すN-1こと01..1です。これがバイナリ カウントの基本的な性質です。私はおそらく逆にそれを行うでしょう - 任意の数字 :01..1に対して、次の連続する数字が10..0であることを示してください。

于 2012-12-05T06:33:50.370 に答える