2026年8月,独立研究者Oleg Kiselyov在个人网站okmij.org更新了一篇读书笔记,把出版于1910年的三卷本巨著《数学原理》(Principia Mathematica,罗素与怀特海合著)第一章重新细读了一遍,给出一个不算小的判断:这本书"读起来像一本现代编程语言教材"。他逐页摘出第8页的指称透明性、第12页关于定义的论述、第15页的"命题函数",认为PM几乎已经写出了lambda演算,甚至预见了类型、continuation和直觉主义。
这类"老书里早就有了"的细读很有阅读快感,但把一部1910年的逻辑学著作直接接到21世纪的编程语言谱系上,中间空出来的几十年和好几位关键人物,恰恰是判断这篇随笔靠不靠谱的地方。
命题函数像lambda演算,像到什么程度
PM第15页引入"命题函数"φx̂:"x is hurt"单独看没有真假,要代入具体的x才能判断。Kiselyov据此认为,这里已经有了自由变量、约束变量、替代和alpha等价——lambda演算的核心机制。
这个类比不算离谱。罗素和怀特海确实观察到,"φx̂"这个符号本身不涉及x,换成"φŷ"意思不变,这和现代程序员理解绑定变量的作用域是同一件事。但PM从未给出抽象和应用这两个操作的一般规则,也没有说明如何用一个函数去处理另一个函数——lambda演算真正的威力恰恰在这里。命题函数更像是对"含参数的命题"做了一次语言学式的命名,离一套可以自我复合、自我求值的演算系统,还差着一大截。
"类型"这个词一样,含义差了一整层
PM第21页第一次用"type"这个词,要求两个函数必须"作用于同类型的参数"。Kiselyov称这可能是"type"现代意义上最早的用法之一。
问题是,罗素这里说的类型,是分支类型论——一套专门用来阻止罗素悖论一类自指陷阱的层级结构,给命题和量化按阶排序。现代编程语言里的类型,刻画的是接口、副作用、资源归属这些计算层面的东西,两者目的完全不同。
更麻烦的是,分支类型论建好之后,罗素和怀特海很快发现它太严格,连一些日常数学推理都做不了,于是引入了可化归公理——假设高阶函数总能在低阶层级上被表示出来。这个公理在PM体系内部一直被视为一种权宜之计,直接削弱了分支类型论最初防悖论的设计初衷。Kiselyov整篇欣赏式细读里,一次都没提到这个公理。
- 风险.忽略可化归公理,等于回避了PM类型论最大的自我妥协,评价其"现代性"时容易只看优点
any与all,预见直觉主义还是自相矛盾
Kiselyov文章里最耐人寻味的一处,是PM第18-19页坚持区分"任意"(any)和"所有"(all)——这被他读成对直觉主义的提前预见。
但PM整体是一套彻底的经典逻辑主义体系,接受无限制的排中律,依赖可化归公理这类非直谓性手段。直觉主义的核心主张恰恰是拒绝普遍排中律,要求每个存在性证明都给出构造性证据。这两套立场在方法论上是正面冲突的,不是谁预见了谁。Kiselyov自己在原文里也承认"两个概念在他们的理论中等价",只是一句话带过,没有展开这个矛盾。
用经典逻辑的书,很难说自己预见了拒绝经典逻辑的思潮
真正的谱系隔着几十年、好几个人
从PM到今天的编程语言理论,中间并不是一条直线。真正起作用的是丘奇的lambda演算、图灵机、库里的组合逻辑与类型指派、哥德尔的递归函数论,以及后来把逻辑证明和程序对应起来的Curry-Howard同构。这条谱系各自独立发展,最后才在类型论里汇合。
现代类型论用宇宙、归纳类型和规范化结果,重新搭建了逻辑、数据、证明和计算之间的对应关系,这套东西跟罗素当年的层级结构关系不大。Coq、Agda、Lean这些证明助理真正的祖先在这条线上,不在PM。
- 结论.PM缺的不是灵感,是操作语义——它告诉你命题该怎么排层级,却没告诉你程序该怎么跑
PM该被摆在哪个位置
对逻辑史研究者和证明助理开发者来说,这不是吹毛求疵。把PM当成编程语言的直接源头,会让人误以为类型系统的设计目标从一开始就是刻画计算,而实际上防悖论和描述计算,是两套不同的工程问题,只是在术语上撞了车。PM该有的位置,是一份重要的思想资源——它提出了指称透明性、绑定变量这些至今好用的观察——而不是lambda演算或类型论的直接源头。下次再看到"这本老书早就预见了X"式的技术史文章,值得先问一句:预见的是概念本身,还是仅仅是一个相似的名字。