如何证明函数始终不可交换

Question

我有以下令人烦恼的问题。 我已经实现了以下功能：

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;

How can I show that for all x,y the following less(x,y) 和 less(y,x) 不可能在 同一时间？

再见

Answer 1

好吧，首先我会要求你考虑 less(-1, -2) 的情况，所以我们必须将函数定义在 n ≥ 0 的范围内。此外，当第一个输入等于第二个输入，对于两个排序都会返回 true，因此我们必须假设 x ≠ y。

我会使用矛盾证明。

假设对于某些 x 和某些 y，其中 x 和 y 都 ≥ 0 且 x≠y，则 less(x,y) 和 less(y,x) 均为 true。

这意味着虽然 x 和 y 都不为零，但您需要将它们减去 n 次，直到其中一个为零，首先检查 x。当第一个操作数达到零时，该函数返回 true；当第二个操作数达到零且第一个操作数非零时，该函数返回 false。

有两种情况：

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，并且该函数事先没有返回 false）。

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

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

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

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

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

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