问题标签 [proof]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
haskell - haskell 实例的适用法律证明
我们通过 Haskell 平台获得的 Applicative 类型类的所有 Haskell 实例是否已被证明满足所有 Applicative 定律？如果是，我们在哪里可以找到这些证据？
Control.Applicative的源代码似乎不包含任何证据证明适用于各种情况的法律确实成立。它只是提到
然后它只是在评论中说明法律。
对于其他类型类（Alternative 和 Monad）的实例，我也发现了类似的情况。
这些图书馆的用户是否应该自己验证这些法律？
但我想知道这些法律的严格证明是否已经由开发商在其他地方给出？
同样，我知道对于 IO Monad 的应用（或 Monad）定律的严格证明，一般来说，它涉及与外部世界的对话，可能非常复杂。
谢谢。
string - 使用奥格登引理与常规抽引引理进行上下文无关语法
我正在学习问题中词条之间的区别。我能找到的每个参考都使用了这个例子：
以显示两者之间的区别。我可以找到一个使用常规引理来“反驳”它的例子。
选择 w = uvxyz, st |vy| > 0, |vxy| <= 页。假设 w 包含相等数量的 b、c、d。
我选择了：
抽 y 只会增加 a 的数量，如果 |b|=|c|=|d| 起初，它现在仍然会。
（如果 w 没有 a 的类似论点。然后随便抽你想要的。）
我的问题是，奥格登引理如何改变这种策略？“标记”有什么作用？
谢谢！
algorithm - 梳排序是否被证明是正确的？是真的吗？
我一直在对 Comb Sort 进行一些研究，并试图弄清楚该算法是否已被证明是正确的。但是，我似乎无法找到有关该算法的大量文档。不过，这是一个非常简单的算法——基本上是冒泡排序的一种变体——我猜这个证明并不复杂。有没有人知道我在哪里可以找到更多关于这方面的信息，或者关于如何从头开始证明它的想法？
对于不熟悉 Comb Sort 的人，您可以在Wikipedia 文章中找到伪代码。
computer-science - 是否有任何按位运算符法则？
从代数定律的角度思考，我想知道在位操作领域是否存在任何官方指南，类似于代数。
代数例子
a - b =/= b - a
让a = 7和b = 5
a - b = 2b - a = -2
让a = 10和b = 3
a - b = 7b - a = -7
因此if a > b，b - a将负等价于a - b。正因为如此，我们可以说
|a - b| = |b - a|。
其中|x|表示 的绝对值x。
按位示例
a | b =/= a + b
注意无符号字节操作：10 | 5 = 15，它是同义词10 + 5 = 15
但是，如果两者a和b等于 5 并且我们OR它们，结果将是 5，因为a = b，这意味着我们只是在相互比较相同的确切位，因此没有任何新内容。
同样，如果b = 7和a = 10我们OR他们，我们将有 15 个。这是因为
因此，我们可以有效地得出结论a | b =/= a + b。
haskell - 显示单子在组合下未关闭的具体示例（有证据）？
众所周知，应用函子在组合下是封闭的，但单子不是。然而，我一直很难找到一个具体的反例来证明单子并不总是组成。
这个答案给出[String -> a]了一个非单子的例子。在玩了一会儿之后，我直觉地相信它，但这个答案只是说“无法实现加入”而没有真正给出任何理由。我想要更正式的东西。当然 type 有很多函数[String -> [String -> a]] -> [String -> a]；必须证明任何这样的功能都不一定满足单子定律。
任何例子（附有证明）都可以；我不一定要特别寻找上述示例的证明。
binary-tree - 使用归纳证明二叉树属性
我在使用归纳法证明二叉树属性时遇到了麻烦：
我的设置正确吗？如果是这样，我该如何展示这些东西。我所尝试的一切最终都变得一团糟。谢谢您的帮助
proof - 证明小于和小于或等于 nat
假设以下定义（前两个取自http://www.cis.upenn.edu/~bcpierce/sf/Basics.html）：
我想证明以下几点：
我能做的最远的事情就是证明blt_nat_flip假设blt_nat_flip0。我花了很多时间，我快到了，但总的来说，它似乎比它应该的要复杂。有人对如何证明这两个引理有更好的想法吗？
到目前为止，这是我的尝试：
c - XOR 的关联属性的逻辑证明
我遇到了一个常见的编程面试问题：给定一个无符号整数列表，找到一个在列表中出现奇数次的整数。例如，如果给定列表：
解决方案将是整数 5，因为它在列表中出现 3 次，而其他整数出现偶数次。
我最初的解决方案涉及设置一个排序数组，然后遍历数组：对于每个奇数元素，我将添加整数，而对于每个偶数元素，我将减去；最后的总和是解决方案，因为其他整数会抵消。
但是，我发现通过简单地对每个元素执行 XOR 来实现更有效的解决方案——您甚至不需要排序数组！也就是说：
我从离散结构类中回忆起，关联属性适用于 XOR 操作，这就是该解决方案有效的原因：
和：
虽然我记得 Associative Property 适用于 XOR，但我很难找到 XOR 特定属性的逻辑证明（互联网上的大多数逻辑证明似乎更侧重于 AND 和 OR 操作）。有谁知道为什么关联属性适用于 XOR 操作？
我怀疑它涉及包含 AND 和/或 OR 的 XOR 身份。
functional-programming - 实践中的 Lambda 演算
如何选择语言，实际计算的一个 lambda 项 (λx.y)((λx.xxx)(λx.xxx))？换句话说，需要一种语言对正常的顺序归约和弱类型系统。
algorithm - 寻找类似的已知问题
我试图证明这个优化问题的计算机复杂性：
给定一个连通图 G = (V, E) 和一个集合 S ⊊ V。找到一个连通子图 G'= (V', E')：
主题：
当并非所有顶点都必须包含在树中时，它看起来像是最小生成树问题的概括。是否有一个已知问题可以通过归约来证明这个问题的复杂性？