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 的范围内。此外，当第一个输入等于第二个输入时，两个排序都将返回 true , 所以我们必须假设 x ≠ y。

我会使用矛盾证明。

假设对于一些 x 和一些 y，其中 x 和 y 都 ≥ 0 且 x≠y，less(x,y) 和 less(y,x) 都为真。

这意味着虽然 x 和 y 都是非零，但您从它们中减去 n 次，直到其中一个为零，首先检查 x。该函数在第一个操作数达到零时返回真，在第二个操作数达到零而第一个非零时返回假。

有两种情况：

  1. x 首先达到零。在这种情况下，n = x，因为 0 = x - n(1)。
  2. y 首先达到零。在这种情况下，n = y，因为 0 = y - n(1)。

根据我们的假设，less(x,y) 返回 true，这意味着函数迭代了 x 次，之后 x - x(1) = 0 并且 y - x(1) > 0（因为 y ≠ x，并且函数没有'不要事先返回假）。

类似地，less(y,x) 返回 true，这意味着函数迭代了 y 次，之后 y- y(1) = 0 并且 x - y(1) > 0（与之前的原因相同）。

这给了我们两个有用的关系：y - x > 0和x - y > 0。重新排列：y > x和x > y（函数的语义含义，但是我们已经从函数如何工作的定义中实现了这一点，并且我们已经将其简化为可以使用某些公理的纯数学）。

从y > xand x > y，您可以重新排列为x > xand y > y（如果 x 大于 y，则它大于 y 大于的所有事物。y 大于 x，因此 x 大于 x）。

这是一个逻辑矛盾，因此我们的假设（他们都是真的）是不正确的。

因此，通过矛盾证明，当 x ≠ y 且 x,y ≥ 0 时，该函数less不能同时为 less(x,y) 和 less(y,x) 返回 true。

（自从我不得不做证明以来已经有一段时间了（尽管我将不得不做一些事情，所以这是一个很好的做法）所以我可能有点生疏。如果有人看到错误，请指出我会尝试修复它）

于 2010-12-02T19:28:00.957 回答