algorithm - 你如何证明算法有效？

Question

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

概述:

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

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

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

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

例子:让我们以二分查找为例，忘记我遇到的实际问题。

如果您有一个包含 100 个整数且按升序排列的数组，您如何证明您的二分查找算法适用于任何数组和任何 n？

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

arr = list(range(100))

我提出的问题是:

Write a recursive algorithm that will return True if the value '42' is in the array and False otherwise.

您如何证明(如形式证明)该算法有效？请注意突出算法从启发式解决方案变成经过验证的算法的那一刻背后的思维过程和直觉？

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，那是因为它从未存在过。你的论点不应该依赖于任何具体的例子，在我看来，除了基本情况——否则它可能是统计的。您需要在数学意义上“证明”它。