问题标签 [proof-of-correctness]

1）假设我们有一个常见的0-1背包问题。给定一组从 1 到 n 编号的 n 个项目，每个项目都有一个权重 w_i 和一个值 v_i，以及最大权重容量 W。这里我们需要选择一些对象，使 v_i 的总和最大化，这样所选对象的 w_i 总和不会超过给定的 W 数。

2）现在假设我们遇到了同样的问题，但是我们需要选择对象，使它们的值之和最小，并且它们的权重之和不能小于给定的数字。

知道第一个问题是 NP 完全的，我怎么能证明第二个问题具有相同的复杂性，换句话说也是 NP 完全的？

可能这是一个非常简单的解决方案，我只是愚蠢，但我找不到这个 while 循环的不变量。为了证明 (a+b) <= 2x，你可以取 (x+y>a+b)，所以这可能是不变量的第一部分，但对于第二部分，为了证明 2x<= (a+b +1）......你到底在做什么？我尝试了一切，但为此浪费了两个小时。

我觉得它应该很明显，我只是看不到它。

我理解关于证明部分正确性的理论。我只是找不到循环不变量，所以不变量将不胜感激，无需解释理论。

证明下列程序的部分正确性

我想证明我对multi-paxos的实现是正确的。有什么有效的例子可供我测试吗？或者可以有其他一些方法来说服其他人我的实现是正确的。

我试图找到一些包含示例的论文，但大多数论文只是指定了算法。

我正在使用 AGDA 做一些经典的数学证明。我想证明一组基数n的子集数等于2^n（即pow（2，n））。为此，我的策略如下：

1) 编写一个函数 sub n，给定每个自然数，它返回小于或等于 n 的所有可能的自然数子集的列表。

2) 编写两个函数“length”和“pow”，分别计算列表的长度和 2^n

3) 将 3 个函数放在一起证明该陈述。

但是，我在解决第 1 点时遇到了麻烦）。我的想法是让函数返回一个“list Nat”类型的列表，但是我在实现递归时遇到了一些问题。基本上，我对归纳步骤的想法是将“n”两个新子集的每个子集关联到：自身和添加“n+1”的子集。

你认为这是一个有效的策略吗？此外，我该如何解决第 1 点的问题？谢谢

考虑出现在 Codeforces（额定 1500）中的这个问题：

有 n 个拳击手，第 i 个拳击手的重量为 ai。他们每个人在比赛前可以改变权重不超过1（权重不能等于0，即必须保持正数）。权重始终是整数。

有必要选择人数最多的拳击队，队伍中所有拳击手的体重都不同（即唯一）。

编写一个程序，对于给定的当前值，ai 将找到一个团队中拳击手的最大可能数量。

一些拳击手的体重可能在一些变化后是 150001（但不会更多）。

输入 ：第一行包含一个整数 n (1≤n≤150000)——拳击手的数量。下一行包含 n 个整数 a1,a2,…,an，其中 ai (1≤ai≤150000) 是第 i 个拳击手的体重。

输出 ：打印一个整数——团队中可能的最大人数。

这是我实现的代码，被 Codeforces 接受为正确提交（Python 3.7）：

但是，我无法严格证明该算法一定会给出正确的答案。例如，当 inputlist 为 [1, 1, 1, 2, 2, 5 , 8] 时，[1, 2, 3, 4, 7, 8]（我的算法）和 [1, 2, 3, 6, 7, 8] 是正确的输出 boxerset，尽管这两种情况的答案都是 6。

我的问题是这样的：

如何证明我的算法是正确的？我的证明如何证明在所有可能的合法拳击手选择中，我的算法选择的拳击手数量最多（这就是我如何证明我不存在其他选择拳击手的数量可以是大于我的算法所做的选择）？

我尝试过反证法但无济于事（尽管我认为证明必须具有反证法的自然结构）。

https://codeforces.com/problemset/problem/1203/E

我们计划在一座山上建造一个滑雪场，山上有几座山峰。为了让滑雪路线尽可能的长，我们决定通过削山填海的方式，使这座山只有一个山峰。为了节省施工成本，我们必须尽量减少切割和填充量。我们将问题表述如下：

给定一个整数元素列表 f，创建一个新列表 g（整数元素）：

1. 总和（f）=总和（g）
2. g的元素只有一个峰；g 必须单调增加，直到峰值然后单调减少。
3. 我们希望将成本降到最低；成本为 sum((f[i] - g[i])**2 for i in range(len(f))

此外，为了使问题简单，我们排除了具有多个最大峰值的输入，即没有给出 [3, 6, 5, 6, 2]。

下面的代码是我的解决方案（非常直观）。解决方案中的峰值将与给定列表中的最大峰值相同。然后，当 g 不是山状（先增加后减少）时，将两个元素的值修改为它们的平均值。

我检查了代码是否返回了正确的解决方案。但是，我无法证明其正确性。

我有以下 ATS 代码：

代码的动机是使用依赖类型系统完成一个简单的练习：证明整数的乘法是关联的。证明的想法是将 3 个整数变量 a,b,c 分解为它们符号的可能情况，然后将问题简化为证明自然数乘法的结合性，我们可以使用归纳法。

从数学上讲，这种策略应该是合理的（尽管分解案例并制定巨大的决策树很乏味）。问题是，当我尝试使用命令编译上述文件时patscc assoc.dats，我收到以下错误消息：

坦率地说，我不知道如何解释这个错误信息。什么是约束C3NSTRprop(C3TKmain(); S2Eeqeq(S2Eintinf(0); S2Evar(abc(4303))))？

我想为下面的一段代码找到一个循环不变量，我似乎无法弄清楚这段代码中呈现的任何类型的关系。

该算法的目标是找到二叉树中所有元素的总和。它将节点存储在一个名为 的堆栈中s。

我注意到这res是所有当前节点的父节点及其父节点左侧的总和，但我不知道如何将其表述为循环不变量。

Leetcode 描述

给定一个长度为的字符串n，您必须确定该字符串是否为回文，但您最多可以删除一个字符。

例如：“aba”是回文。
"abca" 也是有效的，因为我们可以删除 "b" 或 "c" 以获得回文。

我见过许多采用以下方法的解决方案。

用两个指针left分别right初始化为字符串的开始和结束字符，只要和所指向的两个字符相等，就保持同步递增和left递减。rightleftright

当我们第一次遇到 and 所指向的字符之间的不匹配时left，right并说这些是专门的索引iand j，我们只是检查string[i..j-1]or是否string[i+1..j]是回文。

我清楚地知道为什么会这样，但让我困扰的一件事是当我们第一次看到不匹配时我们采取的方法的方向。

假设我们不关心时间效率，只关注正确性，我看不出是什么阻止我们尝试删除一个字符，string[0..i-1]或者string[j+1..n-1]尝试查看整个结果字符串是否会变成回文？更具体地说，如果我们采用第一种方法并
看到两者都不是回文，那么是什么阻止我们回溯到我描述的第二种方法，看看是否删除一个字符或会产生一个回文？string[i..j-1]string[i+1..j]string[0..i-1]string[j+1..n-1]

我们能否在数学上证明为什么这种方法无用或根本不正确？

我试图证明选择排序的正确性，其中我应该只使用数学谓词逻辑来证明程序的正确性，我发现很难将下面给出的英语语句写成谓词并继续证明正确性遵循推理规则，

我必须在谓词中写的语句是，

1. a[0...i-1]已排序

2. 中的所有条目a[i..n-1]都大于或等于 中的条目a[0..i-1]。