1.2 计算的梦想与破灭本文内容摘自本人的开源书《从沙子到车辙 - 一个工程师的理解》 在线阅读/下载from-sand-to-rutsgitclone https://github.com/Lularible/from-sand-to-ruts⭐ 如果对您有帮助欢迎 Star 支持也欢迎通过 GitHub Issues 交流讨论。莱布尼茨的狂野梦想17 世纪的最后几年一位德国哲学家坐在书房里面对满桌的书稿陷入了沉思。他叫莱布尼茨。他想的是这样一件事人类的知识能不能像数学一样计算出来具体地说如果能把所有的概念都编码成符号把所有的推理规则都写成公式那么当两个人有不同意见的时候他们只需要坐下来——“我们来算一算”——就能得出谁对谁错。他把这两个东西叫做Characteristica Universalis通用表意文字和Calculus Ratiocinator推理演算器。他希望创造一个形式化的符号语言表达一切概念定义一套机械的推理规则处理这些符号。任何真理都可以通过符号的纯形式操作来证明。你不是在想你是在算。莱布尼茨甚至设想过一种逻辑计算器——球体上刻着符号通过管道和导轨连接——但 17 世纪的技术完全无法实现。他那时候手上只有黄铜齿轮和阶梯鼓轮连稳定的电源都没有。但请注意莱布尼茨的梦想里已经包含了通用表意文字的所有核心要素。符号 语言的字。推理规则 语言的语法。计算 在规则下操作符号。这个框架——语法 语义 推理——后来成了整个现代数理逻辑的骨架。哥德尔不完备性定理是在这个框架里完成的自指构造图灵机也是在这个框架里定义的计算模型。莱布尼茨是计算机科学的林肯——他没有看到终点但他画出了地图。布尔把逻辑变成代数莱布尼茨之后一百多年数学界在这条路上缓慢推进。第一个实质性突破来自一个意想不到的人。乔治·布尔George Boole的父亲是个鞋匠但对科学极度痴迷——在家里自制望远镜、显微镜、日冕仪。布尔没上过大学在 16 岁之前靠自学掌握了拉丁语、希腊语、法语、德语和意大利语。16 岁时他在一所小学当助教19 岁自己开了一所小学靠教书养家。他在业余时间研究数学。而且不是轻松的研究——他在没有导师、没有大学图书馆、没有同行的条件下自己推演出了不变式理论invariant theory并因此获得了英国皇家学会的皇家奖章。1847 年32 岁的布尔出版了一本薄薄的小册子——《逻辑的数学分析》The Mathematical Analysis of Logic。他在书中提出了一个极其大胆的观点逻辑命题不是哲学的抽象思辨——它们是可以用代数规则来操作的数学对象。AND、OR、NOT 不再是并且“或者”不的口语说法。它们是运算。设 A 今天是晴天 设 B 我去散步 那么 A AND B 今天是晴天 且 我去散步 → A × B A OR B 今天是晴天 或 我去散步 → A B NOT A 今天不是晴天 → 1 - A 真 1, 假 0在这个系统里A A A重复同一命题不增加信息A × A A同一个命题说两遍还是它自己A × (1 - A) 0一个命题不能同时为真又为假——排中律。1854 年他把这套系统扩展成了他一生最重要的著作——《思维的法则》The Laws of Thought。副标题是On which are founded the Mathematical Theories of Logic and Probabilities。他想证明思维本质上是数学运算逻辑推理可以还原为代数演算。但布尔的书在当时几乎无人问津。逻辑学家觉得他太数学化了数学家觉得他太哲学了。布尔 49 岁就去世了——在雨天步行两英里去大学上课浑身湿透然后发了高烧死于肺炎。他的遗孀相信用同样的方式治疗病因的民间偏方——把布尔放在湿床单上——加速了他的死亡。在布尔的有生之年几乎没有人理解他的工作的价值。这个价值等了 80 多年才被重新发现。1937 年MIT 硕士研究生克劳德·香农Claude Shannon写了一篇硕士论文——《继电器与开关电路的符号分析》A Symbolic Analysis of Relay and Switching Circuits。香农指出继电器的开/合、开关的通/断、电路的高电平/低电平——所有这些二值物理状态都可以完美地映射到布尔代数的 TRUE/FALSE。AND 门 串联开关OR 门 并联开关NOT 门 常闭触点。这篇硕士论文被公认为20 世纪最重要的硕士论文——没有之一。它奠基了数字电路设计这个学科。从此以后你设计数字电路不是在画导线和继电器——你是在做布尔代数。而布尔那个穷鞋匠的儿子那个在小学教室里偷偷演算逻辑方程的乡村教师在 80 年前就已经把语法写好了。你之所以能用晶体管搭出逻辑门之所以能在 C 代码里写if (a b)之所以能看着逻辑分析仪上的高低电平推演程序行为——全是因为 19 世纪中叶有个自学成才的爱尔兰数学老师发明了布尔代数而 20 世纪中叶有个 MIT 的研究生把布尔代数映射到了电路上。思维 → 代数 → 电路。思想的物化之路要花一百年。弗雷格逻辑的第一层地基被一场地震摧毁布尔的系统很强但它有一个致命缺陷它只能处理命题之间的关系不能处理命题内部的逻辑结构。所有人都会死这个命题在布尔代数里只能用一个变量 A 来表示。但所有人都会死和苏格拉底是人 → 苏格拉底会死之间到底有什么内在联系布尔代数看不出来。它把命题当作原子——不可分割的基本单元。这个局限被戈特洛布·弗雷格Gottlob Frege打破了。弗雷格是一个脾气孤僻的德国数学教授在耶拿大学教书终其一生几乎不为人知。他于 1879 年出版了一本叫《概念文字》Begriffsschrift的书几乎独自一人发明了现代谓词逻辑。谓词逻辑比命题逻辑多了一样东西它可以把命题拆开。不再是P 表示所有人都会死——而是∀x (Human(x) → Mortal(x))“对于所有的 x如果 x 是人那么 x 是会死的。”弗雷格发明了量词∀对于所有和 ∃存在。他发明了严格的推理规则定义了什么样的符号变换是合法证明什么样的不是。莱布尼茨的通用表意文字在弗雷格的 Begriffsschrift 里第一次有了一个完整、精确、可操作的实现。弗雷格随后花了 20 年试图用这套逻辑系统去奠定整个算术的基础。他的计划是从纯逻辑出发推导出自然数的定义、加法的定义、乘法的定义——最终证明所有的数学真理都可以还原为逻辑真理。他为此写了《算术的基本法则》第一卷 1893 年出版第二卷 1902 年即将付印。然后他收到了一封信。寄信人是英国年轻人伯特兰·罗素。信里只有两页但其中包含的一句话彻底粉碎了弗雷格花了 20 年建造的逻辑大厦。“请考虑所有’不包含自身的集合’的集合——这个集合是否包含自身”这就是罗素悖论设 R { x | x ∉ x }即R 是所有不包含自身的集合的集合。 问R ∈ R 吗 如果 R ∈ R则按定义R 不包含自身 → R ∉ R矛盾。 如果 R ∉ R则按定义R 应该包含在 R 中 → R ∈ R矛盾。也就是说存在一个用弗雷格系统可以合法定义的集合——但它的存在本身就导致矛盾。弗雷格的系统是不一致的。弗雷格的回应令人心碎。他在《算术基本法则》第二卷的后记中写道“一个科学家最不想见到的事情就是在工作完成之后发现自己的基础崩塌了。而我的处境更加难堪因为我的基础不仅崩塌了——还是被伯特兰·罗素先生在我即将付印之前指出的。”弗雷格从此再也没有发表过重要的逻辑著作。他在孤僻和抑郁中度过了余生。9 年后哲学家路德维希·维特根斯坦去拜访弗雷格——弗雷格劝维特根斯坦去剑桥找罗素学习。自己的系统被罗素摧毁了但弗雷格还是把孩子送到摧毁者那里去学习——因为他说罗素是这个领域唯一真正的天才。这份胸襟与他的悲剧同样巨大。罗素和怀特海一项不可能完成的工程罗素悖论让数学界意识到集合论不能是想怎么定义就怎么定义的。你需要严格限制集合的构造方式防止自指悖论。罗素自己的解决方案是类型论Type Theory——一个集合的类型级别必须比它的元素的类型级别高禁止包含自身这种自指构造。他在 1903 年出版的《数学原理》The Principles of Mathematics里勾勒了类型论的基本思想然后在 1910-1913 年间与他的老师阿尔弗雷德·诺斯·怀特海Alfred North Whitehead合著了三卷巨著——《数学原理》Principia Mathematica。这套书是人类历史上最野心勃勃的形式化工程。罗素和怀特海的目标是从一套最基本的逻辑公理出发一步一步、严格地推导出所有已知的数学定理。没有跳跃、没有直觉、没有显然——每一步都必须严格按照逻辑规则。这套书有多疯狂第 1 卷的前 379 页才终于证明了1 1 2。当证明终于到达时作者写了一句干巴巴的评注“上述命题偶尔有用。”全书约 2000 页使用了数百个专门设计的符号很多是罗素自己发明的排版成本高昂到剑桥大学出版社拒绝承担。罗素和怀特海自己掏了 50 英镑资助出版——后来罗素自嘲说“这是人类历史上唯一一本净亏损的数学经典。”Principia Mathematica 证明了形式化的可行性——至少在一部分数学上是可行的。但它也暴露了形式化的地狱难度你连 112 都要花 379 页——那高等数学怎么办罗素证明了自己是对的但同时也证明了这条路在实践上是走不通的。不过Principia Mathematica 在至少一个方面取得了意想不到的成功它为类型论奠定了基础而类型论在一个世纪之后成了编程语言类型系统的核心理论基础。你在 Rust 里写fn foo(x: T) - T在 C 里用模板类型推导——这种类型不匹配就拒绝编译的机制是罗素当年为了防止集合包含自身的悖论而发明的。自指悖论的防护墙一百年后成了编译器里的类型检查器。希尔伯特必须知道必将知道大卫·希尔伯特是 20 世纪初最伟大的数学家——不只是因为他的个人成就更因为他定义了整个数学界的议程。1900 年38 岁的希尔伯特在巴黎第二届国际数学家大会上发表了一场历史性演讲。他列出了23 个未解决的数学问题从连续统假设到变分法的一般理论涵盖了当时数学的几乎所有前沿领域。这 23 个问题定义了 20 世纪数学的研究方向——解决了其中某些问题的人几乎都得了菲尔兹奖或等价荣誉。希尔伯特不是在问问题——他是在给 20 世纪的数学界发考卷。在这 23 个问题中第二个问题特别关键“证明算术公理的相容性。”用简单的话说你能不能在数学内部证明数学不会产生矛盾希尔伯特对这个问题的回答是——能而且必须能。他在 1920 年代提出了一套完整的纲领后来被称为希尔伯特计划Hilbert’s Program把所有数学形式化——把数学语言变成一种严格定义的符号系统公理是符号串推理规则是符号变换规则。证明这个形式系统是完备的complete——所有真命题都能被证明。证明这个形式系统是一致的consistent——不可能同时证明 P 和 NOT P。证明这个形式系统是可判定的decidable——存在一个机械程序能判断任意命题是不是定理。前三条是数学的终极基础第四条——可判定性——和计算直接相关。希尔伯特问的是存在一种机械算法自动判定任意数学命题是否为真吗这个问题后来有了一个德语名字Entscheidungsproblem判定问题。希尔伯特在 1930 年的退休演讲中说了一句刻在他墓碑上的名言“Wir müssen wissen — wir werden wissen.”“我们必须知道——我们必将知道。”他说这句话的时候声音洪亮信心十足。听众鼓掌。他不知道的是这场梦在同一个秋天已被击碎——就在那几天前的另一场会议上。哥德尔一句话击穿一切1930 年 9 月德国柯尼斯堡。第二届关于精确科学认识论的会议期间希尔伯特刚刚发表完那场著名的退休演讲。在同一场会议的另一次圆桌讨论中一个 24 岁的瘦弱年轻人站起来用几乎听不到的声音说了一句话“在包含算术的形式系统中存在不可判定的命题。”台下安静了一会儿。冯·诺依曼坐在前排——据当时在场的人回忆他是唯一一个立刻理解了这句话全部含义的人。他脸都白了。这个发言的年轻人叫库尔特·哥德尔Kurt Gödel。一年后1931 年哥德尔发表了完整的证明论文——《论〈数学原理〉及其相关系统的形式不可判定命题》Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme。这就是哥德尔不完备性定理。定理的精髓其实可以概括为在任何足够强大能表示基本算术的、一致的公理化形式系统中必然存在一个命题它既不能被证明也不能被证伪。哥德尔是怎么做到的他用了一个极其精妙的手段——哥德尔编码Gödel numbering。你不是说所有数学都可以用符号串来表示吗好。那我把每一个符号都分配一个唯一的自然数符号 编码 ¬ 1 ∨ 2 ∀ 3 4 0 5 S (后继) 6 ( 7 ) 8 x1 9 x2 10 ...然后把公式编码成数字。比如公式 “(x1 0)”把每个符号替换成编码得到序列 [7, 9, 4, 5, 8]。然后把这些编码作为素数的指数相乘2⁷ × 3⁹ × 5⁴ × 7⁵ × 11⁸。这产生一个巨大的自然数——但它是唯一的。一个公式对应一个唯一的数从一个数可以唯一地反推出原始的公式。同理证明也可以用同样的方式编码。一个证明是由一系列公式组成的序列每个公式编码成一个数字整个证明序列可以编码成一个更大的数字。这样一来算术系统就有了一个极其珍贵的性质“命题 P 是可证的”——这个元数学陈述可以在系统内部被编码成一个算术命题。也就是说系统可以谈论自己。然后哥德尔构造了一个命题 G它说“G 在这个系统中不可证。”注意这里的自指结构G 说的是关于 G 自己的事。就像说谎者悖论这句话是假的——但哥德尔把它用严谨的数学形式写了出来而且用的是希尔伯特自己要求的形式化符号语言现在看后果如果 G可证那么 G 是真的G 说G 不可证既然可证G 就是假的系统证明了假命题 →系统不一致。如果 G不可证那么 G 是真的因为 G 说G 不可证这恰好就是事实但真命题不可证 →系统不完备。所以任何一致的系统都不完备。希尔伯特的梦想在数学上不可实现。形式系统的代码演示让我们把哥德尔的思想具体化。不用完整的 Peano 算术太复杂我们用一个极度简化的形式系统来感受一下自指是怎么进来的形式系统 MiniMath 词汇0, S, , (, ) 公理1∀x (S(x) ≠ 0) 任何东西的后继都不是 0 推理规则1从 A 可以推出 S(A) 我们想谈论这个系统本身。首先编码 符号 编码 0 1 S 2 3 ( 5 ) 7 x 11 那么公式 S(0) S(S(0)) 编码为 符号序列: [S, (, 0, ), , S, (, S, (, 0, ), ), )] 编码序列: [2, 5, 1, 7, 3, 2, 5, 2, 5, 1, 7, 7, 7] 哥德尔数: 2^2 × 3^5 × 5^1 × 7^7 × 11^3 × 13^2 × 17^5 × 19^2 × 23^5 × 29^1 × 31^7 × 37^7 × 41^7 ≈ 1.3 × 10^78 一个巨大的数字这个数字是唯一的一一每个公式拥有唯一的哥德尔数。你不需要看这个数字——你只需要操作它。一个证明若干公式的序列也有一个哥德尔数。X 是公式 Y 的证明这个关系在系统内可以用算术命题表达——因为X 能被某些素数幂的乘积表示和Y 能被另一些素数幂的乘积表示本质上都是数论命题。哥德尔的洞见就是如果你能在系统里谈论可证性你就能在系统里构造一个说’我不可证’的命题。这个命题——G——在系统里是存在的是可以被写出来的是合法的公式。但系统永远无法证明它也永远无法推翻它。它就是形式体系的盲点——和你的视网膜上那个没有感光细胞的黄斑区一样你用它来看世界却看不到它自己。ISO 26262希尔伯特之梦的现代继承人你可能会问这个 19 世纪到 20 世纪初的数学故事跟我写的汽车软件有什么关系关系非常直接。ISO 26262 本质上就是希尔伯特计划在汽车安全领域的再现——只不过范围被极大地缩小了。希尔伯特想用形式系统覆盖所有数学真理。ISO 26262 想用一套形式化的流程和方法论覆盖所有可能导致汽车功能安全事故的软件缺陷。怎么覆盖第一对象限定。不证明任意程序的任意性质——那已经被赖斯定理判了死刑。只证明这个特定 ECU 软件的安全相关性质。给一个具体的 C 文件、一个具体的控制流图、一个具体的安全目标——然后在这个限定范围内穷尽分析。第二工具辅助。模型检查器如 BTC EmbeddedValidator和抽象解释器如 Astrée在特定子问题上是完备的——给定有限状态空间可以在数学上穷举所有可能的执行路径。Astrée 曾经证明过空客 A380 的飞控软件不存在运行时错误——这比罗素和怀特海证明 112 要务实得多。第三约束回归。如果全自动证明不了就用约束收窄——禁止递归、限制循环上界、限制指针使用——把问题降维到一个工具能吃掉的范围。MISRA C 的规则禁止动态内存分配、禁止递归、禁止函数指针——不是为了让你写着难受是为了让静态分析工具能在有限时间内给出确定答案。这就是希尔伯特精神在工程中的妥协版本“我们能证明的我们说’安全’。我们证明不了的我们用约束让它不发生。”但哥德尔的幽灵仍然盘旋在上空。你在 ECU 上有 100 多个参数每个参数在运行时会取上百种可能的值——状态空间是 100^100 这个数量级。你永远没法穷举。你只能采样、只能分析最坏路径、只能加上安全裕度。就像面板厂里的在线检测你不可能量测每一个面板单元上的每一个 TFT 的阈值电压——你在每片基板上抽几个点做 TEGTest Element Group测试用统计学推断整批的良率。工程中的一切安全论证本质上都是对形式不完备性的统计性补偿。哥德尔的幽灵仍然盘旋在上空。工程上的回应也像希尔伯特一样没有认输。没有说那就算了。给你 64KB SRAM——你仍然写出了一套完整的 UDS 诊断栈。给你 10ms 周期——你仍然在 deadline 前把轮速报文转发到了所有需要它的节点。以有涯求无涯。为什么这跟你有关你现在调试一块 ECU遇到一个 seemingly random 的硬件故障——偶发的 bit flip0.001% 概率的 race condition特定温区下某个外设的寄存器异常。你可能修不好它因为底层的物理波动性本身就在宣告确定性是有限的。SRAM 里的 bit flip 不是抽象理论。在深亚微米制程下芯片内部的 SRAM 单元由一个 6T6 个晶体管结构组成。每一个 bit 是两个交叉耦合的反相器维持着。如果某颗 alpha 粒子来自封装材料中的微量铀/钍衰变穿过 SRAM 单元它会电离硅晶格中的原子产生电子-空穴对——这些额外的电荷可以瞬间翻转反相器的状态。物理世界本身就在给逻辑世界投骰子。这恰恰是哥德尔定理的物理对应在物理层面确定性是近似的。在逻辑层面完备性是不可能的。两个层次上终极确定性都不存在。但你在追查这个故障的过程中学会了电源完整性分析学会了把示波器探针焊到芯片引脚上学会了解读芯片厂的 erratum。这个学习的过程就是价值的实现。哥德尔和希尔伯特的故事讲的其实不是一个数学定理的成败。它讲的是人类设定一个伟大的目标然后以同样伟大的诚实证明这个目标不可能实现。希尔伯特想把所有真理都装进一个形式系统里。他失败了。但这个失败的过程催生了现代数理逻辑、计算机科学的基础、以及哥德尔、丘奇、图灵这一代天才的涌现。希尔伯特的墓志铭说我们必须知道——我们必将知道。哥德尔的回应是“有些事情我们永远无法知道——但这不妨碍我们继续追问。”两者都是对的。本篇小结今天我们做了一件事追踪了一场持续250年的梦——把人类推理机械化——然后看它被击碎。关键结论莱布尼茨画了地图布尔写了语法弗雷格搭了地基——形式化思维是一代代人接力搭建的。哥德尔用一个自指命题击穿了希尔伯特的梦想任何足够强大的形式系统都必然存在不可判定的命题。不可判定不是终点而是起点ISO 26262、MISRA C、静态分析——都是在这个幽灵之下用约束换确定性的工程实践。下一节图灵登场。他用一条纸带和一个状态表给出了计算的精确定义。【下集预告】哥德尔证明了有些命题不可证。但怎么判断一个命题是可证的还是不可证的有没有一套机械步骤能自动判定任何数学命题是否为真这就是希尔伯特第三个问题——判定问题Entscheidungsproblem。要回答它你先得回答一个更根本的问题什么是机械步骤什么是算法什么是计算1935 年剑桥大学。一个 23 岁的研究生躺在草地上脑子里浮现出一个画面——一条无限长的纸带一个读写头一张有限的状态表。直到今天你写的每一行 C 代码在底层都是一条纸带和一个状态表在执行。
从沙子到车辙（1.2）：计算的梦想与破灭
1.2 计算的梦想与破灭本文内容摘自本人的开源书《从沙子到车辙 - 一个工程师的理解》 在线阅读/下载from-sand-to-rutsgitclone https://github.com/Lularible/from-sand-to-ruts⭐ 如果对您有帮助欢迎 Star 支持也欢迎通过 GitHub Issues 交流讨论。莱布尼茨的狂野梦想17 世纪的最后几年一位德国哲学家坐在书房里面对满桌的书稿陷入了沉思。他叫莱布尼茨。他想的是这样一件事人类的知识能不能像数学一样计算出来具体地说如果能把所有的概念都编码成符号把所有的推理规则都写成公式那么当两个人有不同意见的时候他们只需要坐下来——“我们来算一算”——就能得出谁对谁错。他把这两个东西叫做Characteristica Universalis通用表意文字和Calculus Ratiocinator推理演算器。他希望创造一个形式化的符号语言表达一切概念定义一套机械的推理规则处理这些符号。任何真理都可以通过符号的纯形式操作来证明。你不是在想你是在算。莱布尼茨甚至设想过一种逻辑计算器——球体上刻着符号通过管道和导轨连接——但 17 世纪的技术完全无法实现。他那时候手上只有黄铜齿轮和阶梯鼓轮连稳定的电源都没有。但请注意莱布尼茨的梦想里已经包含了通用表意文字的所有核心要素。符号 语言的字。推理规则 语言的语法。计算 在规则下操作符号。这个框架——语法 语义 推理——后来成了整个现代数理逻辑的骨架。哥德尔不完备性定理是在这个框架里完成的自指构造图灵机也是在这个框架里定义的计算模型。莱布尼茨是计算机科学的林肯——他没有看到终点但他画出了地图。布尔把逻辑变成代数莱布尼茨之后一百多年数学界在这条路上缓慢推进。第一个实质性突破来自一个意想不到的人。乔治·布尔George Boole的父亲是个鞋匠但对科学极度痴迷——在家里自制望远镜、显微镜、日冕仪。布尔没上过大学在 16 岁之前靠自学掌握了拉丁语、希腊语、法语、德语和意大利语。16 岁时他在一所小学当助教19 岁自己开了一所小学靠教书养家。他在业余时间研究数学。而且不是轻松的研究——他在没有导师、没有大学图书馆、没有同行的条件下自己推演出了不变式理论invariant theory并因此获得了英国皇家学会的皇家奖章。1847 年32 岁的布尔出版了一本薄薄的小册子——《逻辑的数学分析》The Mathematical Analysis of Logic。他在书中提出了一个极其大胆的观点逻辑命题不是哲学的抽象思辨——它们是可以用代数规则来操作的数学对象。AND、OR、NOT 不再是并且“或者”不的口语说法。它们是运算。设 A 今天是晴天 设 B 我去散步 那么 A AND B 今天是晴天 且 我去散步 → A × B A OR B 今天是晴天 或 我去散步 → A B NOT A 今天不是晴天 → 1 - A 真 1, 假 0在这个系统里A A A重复同一命题不增加信息A × A A同一个命题说两遍还是它自己A × (1 - A) 0一个命题不能同时为真又为假——排中律。1854 年他把这套系统扩展成了他一生最重要的著作——《思维的法则》The Laws of Thought。副标题是On which are founded the Mathematical Theories of Logic and Probabilities。他想证明思维本质上是数学运算逻辑推理可以还原为代数演算。但布尔的书在当时几乎无人问津。逻辑学家觉得他太数学化了数学家觉得他太哲学了。布尔 49 岁就去世了——在雨天步行两英里去大学上课浑身湿透然后发了高烧死于肺炎。他的遗孀相信用同样的方式治疗病因的民间偏方——把布尔放在湿床单上——加速了他的死亡。在布尔的有生之年几乎没有人理解他的工作的价值。这个价值等了 80 多年才被重新发现。1937 年MIT 硕士研究生克劳德·香农Claude Shannon写了一篇硕士论文——《继电器与开关电路的符号分析》A Symbolic Analysis of Relay and Switching Circuits。香农指出继电器的开/合、开关的通/断、电路的高电平/低电平——所有这些二值物理状态都可以完美地映射到布尔代数的 TRUE/FALSE。AND 门 串联开关OR 门 并联开关NOT 门 常闭触点。这篇硕士论文被公认为20 世纪最重要的硕士论文——没有之一。它奠基了数字电路设计这个学科。从此以后你设计数字电路不是在画导线和继电器——你是在做布尔代数。而布尔那个穷鞋匠的儿子那个在小学教室里偷偷演算逻辑方程的乡村教师在 80 年前就已经把语法写好了。你之所以能用晶体管搭出逻辑门之所以能在 C 代码里写if (a b)之所以能看着逻辑分析仪上的高低电平推演程序行为——全是因为 19 世纪中叶有个自学成才的爱尔兰数学老师发明了布尔代数而 20 世纪中叶有个 MIT 的研究生把布尔代数映射到了电路上。思维 → 代数 → 电路。思想的物化之路要花一百年。弗雷格逻辑的第一层地基被一场地震摧毁布尔的系统很强但它有一个致命缺陷它只能处理命题之间的关系不能处理命题内部的逻辑结构。所有人都会死这个命题在布尔代数里只能用一个变量 A 来表示。但所有人都会死和苏格拉底是人 → 苏格拉底会死之间到底有什么内在联系布尔代数看不出来。它把命题当作原子——不可分割的基本单元。这个局限被戈特洛布·弗雷格Gottlob Frege打破了。弗雷格是一个脾气孤僻的德国数学教授在耶拿大学教书终其一生几乎不为人知。他于 1879 年出版了一本叫《概念文字》Begriffsschrift的书几乎独自一人发明了现代谓词逻辑。谓词逻辑比命题逻辑多了一样东西它可以把命题拆开。不再是P 表示所有人都会死——而是∀x (Human(x) → Mortal(x))“对于所有的 x如果 x 是人那么 x 是会死的。”弗雷格发明了量词∀对于所有和 ∃存在。他发明了严格的推理规则定义了什么样的符号变换是合法证明什么样的不是。莱布尼茨的通用表意文字在弗雷格的 Begriffsschrift 里第一次有了一个完整、精确、可操作的实现。弗雷格随后花了 20 年试图用这套逻辑系统去奠定整个算术的基础。他的计划是从纯逻辑出发推导出自然数的定义、加法的定义、乘法的定义——最终证明所有的数学真理都可以还原为逻辑真理。他为此写了《算术的基本法则》第一卷 1893 年出版第二卷 1902 年即将付印。然后他收到了一封信。寄信人是英国年轻人伯特兰·罗素。信里只有两页但其中包含的一句话彻底粉碎了弗雷格花了 20 年建造的逻辑大厦。“请考虑所有’不包含自身的集合’的集合——这个集合是否包含自身”这就是罗素悖论设 R { x | x ∉ x }即R 是所有不包含自身的集合的集合。 问R ∈ R 吗 如果 R ∈ R则按定义R 不包含自身 → R ∉ R矛盾。 如果 R ∉ R则按定义R 应该包含在 R 中 → R ∈ R矛盾。也就是说存在一个用弗雷格系统可以合法定义的集合——但它的存在本身就导致矛盾。弗雷格的系统是不一致的。弗雷格的回应令人心碎。他在《算术基本法则》第二卷的后记中写道“一个科学家最不想见到的事情就是在工作完成之后发现自己的基础崩塌了。而我的处境更加难堪因为我的基础不仅崩塌了——还是被伯特兰·罗素先生在我即将付印之前指出的。”弗雷格从此再也没有发表过重要的逻辑著作。他在孤僻和抑郁中度过了余生。9 年后哲学家路德维希·维特根斯坦去拜访弗雷格——弗雷格劝维特根斯坦去剑桥找罗素学习。自己的系统被罗素摧毁了但弗雷格还是把孩子送到摧毁者那里去学习——因为他说罗素是这个领域唯一真正的天才。这份胸襟与他的悲剧同样巨大。罗素和怀特海一项不可能完成的工程罗素悖论让数学界意识到集合论不能是想怎么定义就怎么定义的。你需要严格限制集合的构造方式防止自指悖论。罗素自己的解决方案是类型论Type Theory——一个集合的类型级别必须比它的元素的类型级别高禁止包含自身这种自指构造。他在 1903 年出版的《数学原理》The Principles of Mathematics里勾勒了类型论的基本思想然后在 1910-1913 年间与他的老师阿尔弗雷德·诺斯·怀特海Alfred North Whitehead合著了三卷巨著——《数学原理》Principia Mathematica。这套书是人类历史上最野心勃勃的形式化工程。罗素和怀特海的目标是从一套最基本的逻辑公理出发一步一步、严格地推导出所有已知的数学定理。没有跳跃、没有直觉、没有显然——每一步都必须严格按照逻辑规则。这套书有多疯狂第 1 卷的前 379 页才终于证明了1 1 2。当证明终于到达时作者写了一句干巴巴的评注“上述命题偶尔有用。”全书约 2000 页使用了数百个专门设计的符号很多是罗素自己发明的排版成本高昂到剑桥大学出版社拒绝承担。罗素和怀特海自己掏了 50 英镑资助出版——后来罗素自嘲说“这是人类历史上唯一一本净亏损的数学经典。”Principia Mathematica 证明了形式化的可行性——至少在一部分数学上是可行的。但它也暴露了形式化的地狱难度你连 112 都要花 379 页——那高等数学怎么办罗素证明了自己是对的但同时也证明了这条路在实践上是走不通的。不过Principia Mathematica 在至少一个方面取得了意想不到的成功它为类型论奠定了基础而类型论在一个世纪之后成了编程语言类型系统的核心理论基础。你在 Rust 里写fn foo(x: T) - T在 C 里用模板类型推导——这种类型不匹配就拒绝编译的机制是罗素当年为了防止集合包含自身的悖论而发明的。自指悖论的防护墙一百年后成了编译器里的类型检查器。希尔伯特必须知道必将知道大卫·希尔伯特是 20 世纪初最伟大的数学家——不只是因为他的个人成就更因为他定义了整个数学界的议程。1900 年38 岁的希尔伯特在巴黎第二届国际数学家大会上发表了一场历史性演讲。他列出了23 个未解决的数学问题从连续统假设到变分法的一般理论涵盖了当时数学的几乎所有前沿领域。这 23 个问题定义了 20 世纪数学的研究方向——解决了其中某些问题的人几乎都得了菲尔兹奖或等价荣誉。希尔伯特不是在问问题——他是在给 20 世纪的数学界发考卷。在这 23 个问题中第二个问题特别关键“证明算术公理的相容性。”用简单的话说你能不能在数学内部证明数学不会产生矛盾希尔伯特对这个问题的回答是——能而且必须能。他在 1920 年代提出了一套完整的纲领后来被称为希尔伯特计划Hilbert’s Program把所有数学形式化——把数学语言变成一种严格定义的符号系统公理是符号串推理规则是符号变换规则。证明这个形式系统是完备的complete——所有真命题都能被证明。证明这个形式系统是一致的consistent——不可能同时证明 P 和 NOT P。证明这个形式系统是可判定的decidable——存在一个机械程序能判断任意命题是不是定理。前三条是数学的终极基础第四条——可判定性——和计算直接相关。希尔伯特问的是存在一种机械算法自动判定任意数学命题是否为真吗这个问题后来有了一个德语名字Entscheidungsproblem判定问题。希尔伯特在 1930 年的退休演讲中说了一句刻在他墓碑上的名言“Wir müssen wissen — wir werden wissen.”“我们必须知道——我们必将知道。”他说这句话的时候声音洪亮信心十足。听众鼓掌。他不知道的是这场梦在同一个秋天已被击碎——就在那几天前的另一场会议上。哥德尔一句话击穿一切1930 年 9 月德国柯尼斯堡。第二届关于精确科学认识论的会议期间希尔伯特刚刚发表完那场著名的退休演讲。在同一场会议的另一次圆桌讨论中一个 24 岁的瘦弱年轻人站起来用几乎听不到的声音说了一句话“在包含算术的形式系统中存在不可判定的命题。”台下安静了一会儿。冯·诺依曼坐在前排——据当时在场的人回忆他是唯一一个立刻理解了这句话全部含义的人。他脸都白了。这个发言的年轻人叫库尔特·哥德尔Kurt Gödel。一年后1931 年哥德尔发表了完整的证明论文——《论〈数学原理〉及其相关系统的形式不可判定命题》Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme。这就是哥德尔不完备性定理。定理的精髓其实可以概括为在任何足够强大能表示基本算术的、一致的公理化形式系统中必然存在一个命题它既不能被证明也不能被证伪。哥德尔是怎么做到的他用了一个极其精妙的手段——哥德尔编码Gödel numbering。你不是说所有数学都可以用符号串来表示吗好。那我把每一个符号都分配一个唯一的自然数符号 编码 ¬ 1 ∨ 2 ∀ 3 4 0 5 S (后继) 6 ( 7 ) 8 x1 9 x2 10 ...然后把公式编码成数字。比如公式 “(x1 0)”把每个符号替换成编码得到序列 [7, 9, 4, 5, 8]。然后把这些编码作为素数的指数相乘2⁷ × 3⁹ × 5⁴ × 7⁵ × 11⁸。这产生一个巨大的自然数——但它是唯一的。一个公式对应一个唯一的数从一个数可以唯一地反推出原始的公式。同理证明也可以用同样的方式编码。一个证明是由一系列公式组成的序列每个公式编码成一个数字整个证明序列可以编码成一个更大的数字。这样一来算术系统就有了一个极其珍贵的性质“命题 P 是可证的”——这个元数学陈述可以在系统内部被编码成一个算术命题。也就是说系统可以谈论自己。然后哥德尔构造了一个命题 G它说“G 在这个系统中不可证。”注意这里的自指结构G 说的是关于 G 自己的事。就像说谎者悖论这句话是假的——但哥德尔把它用严谨的数学形式写了出来而且用的是希尔伯特自己要求的形式化符号语言现在看后果如果 G可证那么 G 是真的G 说G 不可证既然可证G 就是假的系统证明了假命题 →系统不一致。如果 G不可证那么 G 是真的因为 G 说G 不可证这恰好就是事实但真命题不可证 →系统不完备。所以任何一致的系统都不完备。希尔伯特的梦想在数学上不可实现。形式系统的代码演示让我们把哥德尔的思想具体化。不用完整的 Peano 算术太复杂我们用一个极度简化的形式系统来感受一下自指是怎么进来的形式系统 MiniMath 词汇0, S, , (, ) 公理1∀x (S(x) ≠ 0) 任何东西的后继都不是 0 推理规则1从 A 可以推出 S(A) 我们想谈论这个系统本身。首先编码 符号 编码 0 1 S 2 3 ( 5 ) 7 x 11 那么公式 S(0) S(S(0)) 编码为 符号序列: [S, (, 0, ), , S, (, S, (, 0, ), ), )] 编码序列: [2, 5, 1, 7, 3, 2, 5, 2, 5, 1, 7, 7, 7] 哥德尔数: 2^2 × 3^5 × 5^1 × 7^7 × 11^3 × 13^2 × 17^5 × 19^2 × 23^5 × 29^1 × 31^7 × 37^7 × 41^7 ≈ 1.3 × 10^78 一个巨大的数字这个数字是唯一的一一每个公式拥有唯一的哥德尔数。你不需要看这个数字——你只需要操作它。一个证明若干公式的序列也有一个哥德尔数。X 是公式 Y 的证明这个关系在系统内可以用算术命题表达——因为X 能被某些素数幂的乘积表示和Y 能被另一些素数幂的乘积表示本质上都是数论命题。哥德尔的洞见就是如果你能在系统里谈论可证性你就能在系统里构造一个说’我不可证’的命题。这个命题——G——在系统里是存在的是可以被写出来的是合法的公式。但系统永远无法证明它也永远无法推翻它。它就是形式体系的盲点——和你的视网膜上那个没有感光细胞的黄斑区一样你用它来看世界却看不到它自己。ISO 26262希尔伯特之梦的现代继承人你可能会问这个 19 世纪到 20 世纪初的数学故事跟我写的汽车软件有什么关系关系非常直接。ISO 26262 本质上就是希尔伯特计划在汽车安全领域的再现——只不过范围被极大地缩小了。希尔伯特想用形式系统覆盖所有数学真理。ISO 26262 想用一套形式化的流程和方法论覆盖所有可能导致汽车功能安全事故的软件缺陷。怎么覆盖第一对象限定。不证明任意程序的任意性质——那已经被赖斯定理判了死刑。只证明这个特定 ECU 软件的安全相关性质。给一个具体的 C 文件、一个具体的控制流图、一个具体的安全目标——然后在这个限定范围内穷尽分析。第二工具辅助。模型检查器如 BTC EmbeddedValidator和抽象解释器如 Astrée在特定子问题上是完备的——给定有限状态空间可以在数学上穷举所有可能的执行路径。Astrée 曾经证明过空客 A380 的飞控软件不存在运行时错误——这比罗素和怀特海证明 112 要务实得多。第三约束回归。如果全自动证明不了就用约束收窄——禁止递归、限制循环上界、限制指针使用——把问题降维到一个工具能吃掉的范围。MISRA C 的规则禁止动态内存分配、禁止递归、禁止函数指针——不是为了让你写着难受是为了让静态分析工具能在有限时间内给出确定答案。这就是希尔伯特精神在工程中的妥协版本“我们能证明的我们说’安全’。我们证明不了的我们用约束让它不发生。”但哥德尔的幽灵仍然盘旋在上空。你在 ECU 上有 100 多个参数每个参数在运行时会取上百种可能的值——状态空间是 100^100 这个数量级。你永远没法穷举。你只能采样、只能分析最坏路径、只能加上安全裕度。就像面板厂里的在线检测你不可能量测每一个面板单元上的每一个 TFT 的阈值电压——你在每片基板上抽几个点做 TEGTest Element Group测试用统计学推断整批的良率。工程中的一切安全论证本质上都是对形式不完备性的统计性补偿。哥德尔的幽灵仍然盘旋在上空。工程上的回应也像希尔伯特一样没有认输。没有说那就算了。给你 64KB SRAM——你仍然写出了一套完整的 UDS 诊断栈。给你 10ms 周期——你仍然在 deadline 前把轮速报文转发到了所有需要它的节点。以有涯求无涯。为什么这跟你有关你现在调试一块 ECU遇到一个 seemingly random 的硬件故障——偶发的 bit flip0.001% 概率的 race condition特定温区下某个外设的寄存器异常。你可能修不好它因为底层的物理波动性本身就在宣告确定性是有限的。SRAM 里的 bit flip 不是抽象理论。在深亚微米制程下芯片内部的 SRAM 单元由一个 6T6 个晶体管结构组成。每一个 bit 是两个交叉耦合的反相器维持着。如果某颗 alpha 粒子来自封装材料中的微量铀/钍衰变穿过 SRAM 单元它会电离硅晶格中的原子产生电子-空穴对——这些额外的电荷可以瞬间翻转反相器的状态。物理世界本身就在给逻辑世界投骰子。这恰恰是哥德尔定理的物理对应在物理层面确定性是近似的。在逻辑层面完备性是不可能的。两个层次上终极确定性都不存在。但你在追查这个故障的过程中学会了电源完整性分析学会了把示波器探针焊到芯片引脚上学会了解读芯片厂的 erratum。这个学习的过程就是价值的实现。哥德尔和希尔伯特的故事讲的其实不是一个数学定理的成败。它讲的是人类设定一个伟大的目标然后以同样伟大的诚实证明这个目标不可能实现。希尔伯特想把所有真理都装进一个形式系统里。他失败了。但这个失败的过程催生了现代数理逻辑、计算机科学的基础、以及哥德尔、丘奇、图灵这一代天才的涌现。希尔伯特的墓志铭说我们必须知道——我们必将知道。哥德尔的回应是“有些事情我们永远无法知道——但这不妨碍我们继续追问。”两者都是对的。本篇小结今天我们做了一件事追踪了一场持续250年的梦——把人类推理机械化——然后看它被击碎。关键结论莱布尼茨画了地图布尔写了语法弗雷格搭了地基——形式化思维是一代代人接力搭建的。哥德尔用一个自指命题击穿了希尔伯特的梦想任何足够强大的形式系统都必然存在不可判定的命题。不可判定不是终点而是起点ISO 26262、MISRA C、静态分析——都是在这个幽灵之下用约束换确定性的工程实践。下一节图灵登场。他用一条纸带和一个状态表给出了计算的精确定义。【下集预告】哥德尔证明了有些命题不可证。但怎么判断一个命题是可证的还是不可证的有没有一套机械步骤能自动判定任何数学命题是否为真这就是希尔伯特第三个问题——判定问题Entscheidungsproblem。要回答它你先得回答一个更根本的问题什么是机械步骤什么是算法什么是计算1935 年剑桥大学。一个 23 岁的研究生躺在草地上脑子里浮现出一个画面——一条无限长的纸带一个读写头一张有限的状态表。直到今天你写的每一行 C 代码在底层都是一条纸带和一个状态表在执行。
