数学证明和计算机程序等同

数学证明和计算机程序等同 - 极道

数学证明可以表示为计算机程序，反之亦然。这种对应关系被称为库里-霍华德同构，它在逻辑和计算机科学的概念之间建立了等价关系。

逻辑中的命题相当于编程中的类型，证明相当于程序。

具体来说，证明一个陈述为真可以理解为编写一个“驻留”或实例化相应类型的程序。

这种对应关系可应用于形式验证软件和设计函数式编程语言，以及开发使用编程技术来辅助数学推理的交互式证明助手。

类型理论
著名的罗素悖论：在一个村庄里住着一位理发师，他为所有不给自己刮胡子的人刮胡子，而且只给他们刮胡子。
理发师自己刮胡子吗？

• 如果答案是肯定的，那么他一定不能给自己刮胡子（因为他只给不给自己刮胡子的男人刮胡子）。
• 如果答案是否定的，那么他必须给自己刮胡子（因为他给所有不给自己刮胡子的人刮胡子）。

这是伯特兰·罗素在尝试使用集合概念建立数学基础时发现的悖论的非正式版本。也就是说，定义一个包含所有不包含自身的集合而不遇到矛盾的集合是不可能的。

罗素表示，为了避免这种悖论，我们可以使用“类型”。

这些类别的具体值称为对象。例如，如果有一个名为“Nat”的类型，意思是自然数，那么它的对象就是 1、2、3 等等。研究人员通常使用冒号来表示对象的类型。数字7是整数类型，可以写成“7：Integer”。

您可以有一个函数，它接受类型 A 的对象并吐出类型 B 的对象，或者将一对类型 A 和类型 B 的对象组合成一种新类型，称为“A × B”。

因此，解决这个悖论的一种方法是将这些类型放入层次结构中，这样它们只能包含比它们自己“更低级别”的元素。那么类型就不能包含自身，这避免了造成悖论的自引用。

类型=逻辑命题
库里和霍华德表明，类型从根本上等同于逻辑命题。

当一个函数“驻留在”一种类型时，当你可以成功定义一个作为该类型对象的函数时，你就有效地证明了相应的命题是正确的。

因此，接受类型 A 的输入并给出类型 B 的输出（表示为类型 A → B）的函数必须对应于一个含义：“如果 A，则 B”。

例如，以命题“如果正在下雨，则地面是湿的”为例。在类型理论中，这个命题将由类型为“Raining → GroundIsWet”的函数建模。看似不同的公式实际上在数学上是相同的。

好处
尽管这种联系听起来很抽象，但它不仅改变了数学和计算机科学从业者对他们工作的思考方式，而且还导致了这两个领域的一些实际应用。对于计算机科学来说，它为软件验证（确保软件正确性的过程）提供了理论基础。通过根据逻辑命题构建所需的行为，程序员可以从数学上证明程序的行为符合预期。它还为设计更强大的函数式编程语言提供了坚实的理论基础。

对于数学来说，这种对应关系导致了证明助手的诞生，也称为交互式定理证明器。这些是帮助构建形式证明的软件工具，例如 Coq 和 Lean。在 Coq 中，证明的每一步本质上都是一个程序，并且通过类型检查算法来检查证明的有效性。数学家还一直在使用证明助手——尤其是精益定理证明器——来形式化数学，其中涉及以严格的、计算机可验证的格式表示数学概念、定理和证明。这使得有时非正式的数学语言可以由计算机进行检查。

研究人员仍在探索数学和编程之间这种联系的后果。最初的库里-霍华德对应将编程与一种称为直觉逻辑的逻辑融合在一起，但事实证明，更多类型的逻辑也可以接受这种统一。

自库里提出见解以来的一个世纪里，我们不断发现越来越多的‘逻辑系统 X 对应于计算系统 Y’的实例。

研究人员已经将编程与其他类型的逻辑联系起来，例如线性逻辑（包括“资源”的概念）和模态逻辑（处理可能性和必然性的概念）。