什么等同于Curry-Howard同构的bug？

Question

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

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

因此，库里-霍华德将程序与数学证明联系在一起，没有错误。因此，Curry-Howard如何在数学世界中翻译程序错误的概念？如上所述，这不是证明中的逻辑错误。

Answer 1

有bug的程序对应于正确的证明，而正确的证明不同于没有bug的程序所对应的证明。换句话说，有but的程序对应于正确的证明，但不同的证明。打个比方，路径就是你从前门走出来的一系列特定的步骤。你可能打算沿着小路走到杂货店。也许你转错了弯，最后到了理发店。你仍然走了一条路，只是不是你想要的那条。

校样中的逻辑错误更类似于编程语言中的运行时错误或语法错误。在这种情况下，这并不是因为您计算、证明或执行了错误的事情；而是您根本没有计算、证明或执行任何事情。在我们的类比中，这可能就像忘记了如何行走，只用左肘和下巴走了几步。你将无法完成你的路径-任何路径，正确或错误-因为你试图做一些不算步进的事情。

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

Answer 2

不幸的是，我不认为Patrick87的是完全正确的。理解问题中"bug“是什么意思是很重要的。我假设“bug”包括影响类型的错误和不影响类型的错误。

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

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

对于影响对应关系的bug，这取决于它们是否会导致有效的定理。如果它产生了一个有效的定理，那么你的程序很可能会编译，运行而不会崩溃等等。然而，这意味着你搞错了其中一种类型，比如你想把两个数字放在一起，比如1和3 -> 13。但是你忘了把它们转换成字符串，所以你得到的是1和3 -> 4。另一方面，如果它没有产生一个有效的定理，那么它意味着你可能遇到了一些严重的错误，程序不能编译，或者它会陷入无尽的循环，或者诸如此类的事情。

总而言之，如果你有一个具有有效的相应定理的程序，那就不会告诉你太多。程序仍然可以有bug。另一方面，如果你试图编写一个没有相应定理的程序，那么这是一个很好的迹象，表明你可能出错了。因此，这取决于类型的bug，大多数根本不会出现。