2

私は次の厄介な問題を抱えています。次の関数を実装しました。

function bool less(nat x, nat y) {
    if (y<>0) then
       if (x<>0) then
           return less(x-1,y-1);
       else
           return true;
       end;
    else
       return false;
    end;
end;

すべてのx、yについて、次のless（x、y）とless（y、x）を同時に使用できないことをどのように示すことができますか？

さよなら

4

1 に答える 1

2

まず、 の場合を考えていただきたいless(-1, -2)ので、関数を n ≥ 0 の範囲で定義する必要があります。また、最初の入力が 2 番目の入力と等しい場合、両方の順序付けで true を返します。であるため、x ≠ y であると仮定する必要があります。

矛盾による証明を使用します。

x と y がどちらも 0 以上で x≠y である x と y について、less(x,y) と less(y,x) が両方とも真であると仮定します。

これは、x と y が両方とも非ゼロである間に、そのうちの 1 つがゼロになるまで、それらから 1 を n 回減算し、最初に x をチェックすることを意味します。この関数は、最初のオペランドがゼロに達すると true を返し、2 番目のオペランドがゼロに達し、最初のオペランドがゼロでない場合は false を返します。

これには 2 つのケースがあります。

  1. x が最初にゼロに到達します。この場合、0 = x - n(1) であるため、n = x です。
  2. y は最初にゼロに達します。この場合、0 = y - n(1) であるため、n = y です。

私たちの仮定では、less(x,y) は true を返しました。これは、関数が x 回反復した後、x - x(1) = 0 および y - x(1) > 0 になったことを意味します (y ≠ x であるため、関数は事前に false を返さないでください)。

同様に、less(y,x) は true を返しました。これは、関数が y 回反復され、その後 y- y(1) = 0 および x - y(1) > 0 になったことを意味します (前と同じ理由)。

これにより、 と の 2 つの便利な関係が得られy - x > 0ますx - y > 0。再配置:y > xおよびx > y(関数の意味論的意味ですが、関数がどのように機能するかの定義からこれを達成し、特定の公理で作業できる純粋な数学に還元しました)。

y > xとから、 と のようにx > y並べ替えることができます(x が y より大きい場合、それは y より大きいすべてのものよりも大きいです。y は x よりも大きいため、x は x よりも大きい)。x > xy > y

これは論理的矛盾であるため、(両方とも真であるという) 私たちの仮定は正しくありません。

したがって、矛盾による証明により、x ≠ y かつ x,y ≥ 0 の場合、関数lessは less(x,y) と less(y,x) の両方に対して true を返すことはできません。

(私が証明をしなければならなかったのはしばらく前のことです (私はいくつかのことをしなければならないので、それは良い習慣です) ので、少し錆びているかもしれません.誰かがエラーを見たら、それを指摘してください.そして私はそれを修正しようとします）

于 2010-12-02T19:28:00.957 に答える