12

アルゴリズムの正当性を証明するためのルール/スキームが存在するかどうか疑問に思っていますか？たとえば、自然数で定義され、以下で定義されている関数$F$があります。

function F(n,k)
begin
  if k=0 then return 1
  else if (n mod 2 = 0) and (k mod 2 = 1) then return 0
  else return F(n div 2, k div 2);
end;

ここで、$ n \ \ text {div} \ 2 = \ left \ lfloor \ frac {n} {2} \ right \ rfloor $

タスクは、$ F（n、k）= \ begin {cases} 1 \ Leftrightarrow {n \ choice k} \ \ text {mod} \ 2 = 1 \ 0 \text{それ以外の場合は}\end{cases}であることを証明することです。 $

それほど複雑には見えませんが（私は間違っていますか？）、この種の証明をどのように構成する必要があるのか​​わかりません。助けていただければ幸いです。

4

3 に答える 3

6

再帰的アルゴリズムの正当性は、多くの場合、数学的帰納法によって証明されます。この方法は2つの部分で構成されます。最初に基礎を確立し、次に帰納的ステップを使用します。

あなたの場合、基本はk = 0の場合、またはkが奇数でnが偶数の場合のすべての場合です。

帰納的ステップでは、f(n,k)が正しい場合f(2*n,2*k)、、、およびがすべて正しいことを証明する必要があります。f(2*n+1,2*k)f(2*n,2*k+1)f(2*n+1,2*k+1)

于 2012-03-02T18:45:32.083 に答える
6

論理を数学的に証明する以外に（例：帰納的証明）、これに関連する計算科学にはいくつかの結果があります。

主題の概要については、ここから始めることができます。正し
さ特定のケースでは、答えが意図したものであることを示すために、部分的な正しさに関心があります。次に、プログラムが終了したことを示す完全な正しさ。

ホーア論理は、部分的な正当性を解決できます。

この特定の問題の終了について：

（n％2 == 0およびk％1 == 1）または（k == 0）の場合、プログラムは終了します。それ以外の場合は、n / 2、k/2の場合に戻ります。kに強い誘導
を 使用すると、プログラムが常にk==0のターミナルノードの1つに到達することを示すことができます。（最初の節で早く終了する可能性がありますが、完全に終了することを示す必要があるだけです。これはそうです）

だから私はあなたに部分的な正しさの証拠を残しました（私はそのことを知らないので）

于 2012-03-02T18:45:50.670 に答える
2

一般的に言えば、あなたは帰納法による証明を試みて正しさを示します。これは、再帰関数の正しさを証明するときに非常にうまく機能します。これは、基本ケースを直接証明でき、関数が「小さい」入力で機能するという事実を使用して、次に大きい入力で機能することを証明できるためです。

この場合、私は十分に根拠のある帰納法による証明を試みます。具体的には、

  1. この関数は、フォーム（n、0）のすべての入力に対して正しいです。
  2. （n'、k'）が辞書式順序で（n、k）よりも小さいようなすべての入力（n'、k'）について、関数が正しいと仮定して、（n、k）に対して正しいことを証明します。

この証明の詳細は、関数の詳細と二項係数のbahvaiorを活用する必要がありますが、一般的なテンプレートは上記のとおりです。

お役に立てれば！

于 2012-03-02T18:40:37.653 に答える