形式验证的历史和方法

形式验证的历史和方法 - 极道

这篇文章主要介绍了形式验证领域的历史和数学起源，涉及了形式推理的历史演变、可证明的递归函数、逆向数学和构造性数学中的类型论。

文章还提到了形式验证对编程语言理论的影响，包括类型系统的发展和依赖类型语言的应用。

文章下一部分将探讨形式验证领域的实践方面，如SMT求解器、程序逻辑、模型检查等。

• 形式验证的历史和根源：从莱布尼兹到哥德尔，探讨形式推理的发展历程和数学逻辑的起源。
• 可证明的递归函数：研究算术理论中可证明的递归函数，展示了哥德尔不完备性定理的另一种表述。
• 逆向数学和类型论：探索逆向数学、构造性数学中的类型论以及类型论对编程语言理论的影响。

详细点击标题

摘要：

1、我们所说的形式化验证，是指可以对语句进行形式化证明的技术，而且这种证明的合理性在某种程度上是有保证的。

从历史上看，形式方法的思想出现在现代。形式推理的最初思想属于 17 世纪德国数学家和哲学家戈特弗里德·威廉·莱布尼茨 (Gottfried Wilhelm Leibniz)。他独立于艾萨克·牛顿爵士发明了微积分。

此外，莱布尼茨还引入了我们都熟悉的积分符号系统。读者可以阅读Stephen Wolfram 撰写的博客文章，更详细地探讨莱布尼茨的表示法。

莱布尼茨认为：

• 任何智力话语都应该使用类似于代数符号系统的符号语言来统一描述。这种语言是一种让每个人表达数学和哲学思想的工具。
• 推理过程应该按照一定的规则进行，根据这些规则保证合理性。
• 推理应该通过微积分推理器来表示，这是一种广义的微积分，其语言具有普遍性。
• 真正的辩论可能会简化为看起来像逻辑演算中的推理的计算。（注意：辩论不是辩证法下的狡辩）

上述构想的成果实现：

• 19世纪中叶，乔治·布尔提出用代数的方式研究亚里士多德逻辑。布尔与奥古斯塔斯·德·摩根一起观察了逻辑定律与集合运算定律之间的对应关系。这些定律现在被称为布尔代数公理，是元素集合运算的抽象。现在，布尔代数的概念远远超出了纯粹的逻辑论述。
• 戈特洛布·弗雷格（Gottlob Frege）开发了一个基于语法而不是代数计算的框架。弗雷格的方法主要是句法的，并且基于描述谓词和运算的语言。该系统称为Begriffsschrift，德语为概念符号。Begriffsschrift历史上是谓词逻辑的第一个公理化表示，即具有普遍和存在量词的关系和属性的逻辑。
• 公理系统是一组包含公理且在推理规则下封闭的格式良好的公式。公理是原始句子。推理规则是从现有定理获得新定理的一种方法。弗雷格的意图是对基本数学概念的纯粹逻辑解释，因此将数学视为逻辑的一个分支。这个纲领现在被称为逻辑主义。
• 1900年代，英国哲学家、数学家伯特兰·罗素注意到弗雷格的系统是不一致的，并发现了其中的悖论：现代读者可能将罗素悖论 称为理发师悖论
• 罗素对哲学和数学基础的看法与弗雷格一样，是一位逻辑学家。罗素计划的目的是以纯粹逻辑的方式并同时一致地描述数学的基础。目的是调查数理逻辑语言在算术概念描述中的表达能力。《数学原理》包含罗素提出的类型论的第一个版本，作为康托集合论的替代品。推荐观看BBC连续剧《伟大的哲学家》
• 希尔伯特纲领和公理化方法：任何数学理论都应该有一个正式的公理对应物。以公理化方式表示数学理论的第一次尝试是希尔伯特在 1890 年代提出的欧几里得几何版本。此外，通常的数学证明必须在那些公理理论中形式化

2、类型论也源于伯特兰·罗素在《数学原理》逻辑主义纲领中的思想。
类型概念的提出是为了避免自我参照现象，这种现象暗示着罗素悖论。

• 朴素集合论中的自引用在于隶属谓词，根本没有任何限制。
• 罗素的层次结构为区分宇宙的悖论提供了一个解决方案

完整的类型系统在《数学原理》中进行了描述。

类型理论在 1940 年代成为 lambda 演算的一个分支，当时 Alonzo Church 用类型扩展了他的 lambda 演算，以避免 lambda 项中的自应用。

类型理论作为证明理论的一个分支以两种方式影响编程语言理论：

第一个视角包括类型编程语言的理论。类型系统的开发最初是从证明理论的角度发展而来的。例如，多态 lambda 演算（广泛称为系统F⁡F）由 Jean-Yves Girard 提出，用于描述直觉二阶算术的可证明递归函数类。现在，我们考虑系统F⁡F作为 Haskell 中实现的参数多态性的公理化描述。

第二个视角被称为构造类型理论。从程序员的角度来看，这种形式提供了依赖类型的 lambda 演算系统。因此，类型系统为进行基于 Curry-Howard 形式验证的编程语言提出了底层形式主义。一些潜在的依赖类型语言，例如 F*、Lean 和 Arend。