你如何证明算法有效？

Question

TL;DR：我如何证明算法适用于每个 n 值？

概述：

我是一名自学成才的程序员，具有线性代数的数学背景。我最近需要通过编写算法来解决 n=100 的问题来证明关系是递归的。

当我找到解决方案时，我到达那里的方式被认为是不可接受的。与我交谈的人说我的算法是一种“统计”算法，而不是实际证明存在递归关系并证明我的算法可以工作。

我一直在解决一些网站上的问题，例如 codesignal、hackerrank 等，但这是我第一次遇到这种将解决方案推广到正式证明的概念。

问题： 如何证明算法适用于每个 n 值？

示例： 让我们以二分搜索为例，忘记我遇到的实际问题。

如果你有一个由 100 个整数组成的数组，按升序排序，你如何证明你的二分搜索算法适用于任何数组和任何 n？

在下面的例子中，假设我们的数组是

arr = list(range(100))

我提出的问题是：

编写一个递归算法，如果值 '42' 在数组中，则返回 True，否则返回 False。

您如何证明（如形式证明）该算法有效？请注意强调算法从启发式解决方案转变为经过验证的算法背后的思考过程和直觉？

Answer 1

42 未被丢弃

如果数组A 已排序，那么如果我们可以显示A[x] > 42，那么A[x + 1] > 42。这是因为，如果对数组进行排序，则每个元素都大于或等于其前身（即A[x + 1] > A[x] > 42）。我们知道这一点是因为 > 运算符是可传递的。

反过来，< 运算符也是如此。

二分搜索应在每一步中拒绝所有大于或小于所需输入的输入，方法是对单个可能性进行抽样，并确定其一侧的所有输入也在需要拒绝（如上所述）。

（编辑：如果x > 42 或x < 42 为真；那么x = 42 必须为假。）

数组变小了

在每个步骤中，至少删除数组的一个元素，除非它等于 42。这是因为如果元素不是 42，则该元素（可能与其他元素一起）将被删除。

如果数组越来越小（假设没有采样 42），并且永远不会删除 42，那么在某些时候，要么采样 42，要么数组为空

结论

如果数组为空，并且由于没有丢弃 42，则永远不会有 42。

如果我们对 42 进行采样，由于没有向数组中引入新元素，因此从 42 开始。

证明！

补充说明

为了证明递归算法有效，你想证明它

1. 结束
2. 产生正确的结果。

它结束是因为在每个递归步骤中，数组越来越小（但不能低于 []）。它产生了正确的结果，因为 42 从未被删除或添加 - 所以最后，如果我们找不到 42，那是因为它从未存在过。在我看来，你的论点不应该依赖任何具体的例子，除了基本情况——否则它可能是统计的。您需要在数学意义上“证明”它。

Answer 2

对于一个简单的正确性证明：你需要证明你的算法可以成功地完成它的设计目标。

因此，以输入案例数据的语句为前提。并计算出它应该暗示输出中所需的后置条件。这证明算法是正确的。

P：关于给定输入的声明

Q：要求输出的语句。

证明 P 蕴含 Q。

照顾角落案例。 确保在所有情况下终止算法。 如果它是一个递归算法，您需要严格证明该算法终止/退出。

编写一个递归算法，如果值 '42' 是，则返回 True 在数组中，否则为 False。

对于此类问题，您还可以使用矛盾证明。首先尝试假设如果不存在 42，算法将返回 true，或者 如果存在 42，算法将返回 false。然后，通过您的算法流程证明您的假设是正确的，并尝试证明这是不可能的，这是一个矛盾。