代码之家 › 专栏 › 技术社区 › Scott Skiles

你如何证明算法有效?

algorithm

Scott Skiles · 技术社区 · 6 年前

tl;dr:我如何证明一个算法对n的每个值都有效?

概述:

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

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

我已经在网站上解决了一些问题,如代码信号、黑客等级等,但这是我第一次遇到将解决方案概括为正式证据的概念。

问题: 如何证明一个算法对n的每个值都有效?

例子: 让我们以二进制搜索为例,忘记我面临的实际问题。

如果你有一个100个整数的数组,按升序排序,你如何证明你的二进制搜索算法适用于任何数组和任何n?

在下面的示例中,假设我们的数组是

arr = list(range(100))

我提出的问题是:

编写一个递归算法,如果值“42”在数组中则返回true,否则返回false。

你如何证明(在正式的证明中)这个算法有效?请注意,在算法从启发式解决方案转变为经验证的算法的瞬间,要突出思想过程和直觉。

2 回复 | 直到 6 年前

Max 6 年前

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就从那里开始。

证明!

为了证明递归算法有效,您需要证明它

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

Kaidul 6 年前

对于一个简单的正确性证明:您需要证明您的算法能够成功地完成它的设计目的。

所以,以输入案例数据的语句为前提。并指出它应隐含输出所需的岗位条件。这证明了算法的正确性。

P:关于给定输入的语句

Q:所需输出的语句。

证明P表示Q。

小心角落的箱子。在任何情况下都要确保算法的终止。如果它是递归算法,则需要严格证明该算法终止/退出。

编写一个递归算法,如果值“42”为在数组中,否则为false。

对于此类问题,您也可以使用 矛盾证明 . 首先尝试假设 如果不存在42,算法将产生真值。 或 如果存在42,算法将返回false . 然后,通过你的算法流程证明你的假设是正确的,并试图证明这是不可能的,一个矛盾。