Curry-Howard 同构的 bug 相当于啥？

Posted 2023-05-08

【中文标题】Curry-Howard 同构的 bug 相当于啥？

【英文标题】：What's the equivalent of a bug by the Curry-Howard isomorphism?Curry-Howard 同构的 bug 相当于什么？

【发布时间】：2017-07-15 14:12:16

【问题描述】：

简单地说，Curry-Howard correspondence 声明一个类型是一个定理，返回该类型的程序是相应定理的证明。

对应是基于数学证明的形式化，在诸如谓词演算之类的语言中，受限于直觉逻辑。但是当数学证明用这些形式语言编写时，它们的错误可以被计算机检测到。例如，Mizar 是一种相对高级的数学语言，加上一个编译器来检查它所写的证明。

因此，Curry-Howard 将程序与数学证明无误地关联起来。因此，Curry-Howard 如何在数学世界中翻译程序错误的概念？综上所述，这不是证明中的逻辑错误。

【参考方案1】：

有错误的程序对应的正确证明与没有错误的程序对应的证明不同。换句话说，有错误的程序对应正确的证明，但不同的证明。打个比方，路径是您走出前门的特定步骤序列。您可能打算步行前往杂货店。也许你走错了路，最终来到了理发店。你仍然走了一条路，只是不是你想要的。

证明中的逻辑错误更类似于编程语言中的运行时或语法错误。在这种情况下，并不是你计算、证明或走错了；但你根本没有计算、证明或行走任何东西。在我们的类比中，这可能就像忘记了如何走路并试图只用你的左肘和下巴来走几步。你将无法完成你的路径——任何路径，无论是对还是错——因为你试图做一些不被视为踩踏的事情。

您可能会考虑一个有趣的挑战 - 编写一个正确、有效的算法，该算法对于任何可能的问题都不正确。

【讨论】：

因此，Curry-Howard 认为一个有错误的程序对应于一个数学定理的有效证明，但没人关心它吗？也许就像证明一个由 5823 个操作组成的自定义代数结构，它们之间有奇怪的计算规则？

至于没用的有效算法，int i = 0; while(true) i++; return 18;怎么样？

【参考方案2】：

很遗憾，我认为 Patrick87 的说法并不完全正确。了解问题中“错误”的含义很重要。我假设“错误”包括影响类型的错误和不影响类型的错误。

需要注意的是，在对应关系下，定理仅与程序的类型特征有关，与值特征无关。所以x := x + 1和x := x + 2这样的程序语句从定理来看是完全等价的。重要的是要认识到，在正常解释中，这些只是抽象定理，而不是关于程序的定理（例如关于它的正确性）。

所以从这里很容易看出很多（也许是大多数）错误根本不会影响相应的定理。例如，如果我们有一个财务计划，并且我们想从毛利中计算净利润，那么写NetProfit := GrossProfit * 0.8 可能是正确的。但是我们可能会输入一个错误并计算税收而不是NetProfit := GrossProfit * 0.2。它对类型没有影响，因此对对应关系没有影响。很多很多真正的错误是这样的：一个错误、溢出错误、误解子程序的行为、数字和字符串拼写错误……

对于确实影响通信的错误，这取决于它们是否会导致有效的定理。如果它得出一个有效的定理，那么您的程序更有可能编译、运行而不会崩溃等。但是，这意味着您有一种类型错误，例如，如果您想将 2 个数字放在一起，例如 1 和 3 -> 13。但是你忘记将它们转换为字符串，所以你得到了 1 和 3 -> 4。另一方面，如果它没有导致有效的定理，那么这意味着你可能有严重错误，并且程序无法编译，或者它会陷入无限循环，或类似的情况。

总而言之，如果您有一个程序具有相应的有效定理，那并不能告诉您太多。该程序仍然可能有错误。另一方面，如果您尝试编写一个没有相应定理的程序，那么这很好地表明您可能会出错。所以这取决于错误的类型，大多数根本不会出现。