众所周知伞哥 @田春冰河 在2024年岁尾，在Hol4里完成了某个Böhm定理的形式化证明，额切据说Barendregt原书上的证明实际上是证不出来的，即使是顶尖数学家的直觉也会有不可靠的时候，据说这也是为什么Voevodsky晚年毅然投身形式化证明领域的原因。伞哥很得意的和写在白板上的公式合影留念，是他2024年的高光时刻之一。

++++

我还没去读Barendregt的书和伞哥的证明，但这里可能可以提供一个我们应该终有一日去读一下的冻鸡。

图一是斯坦福PhD Ben Lynn的页面，http://t.cn/A6upXtOL

页面上开篇的意思是，众所周知，图灵机和λ是等价的。如果我们要组合图灵机，就是A图灵机等待B图灵机的计算完成输出结果，作为A的输入；如果我们要组合λ，把一个A表达式apply到B表达式上就行了。

但是！这里有一个微妙但重要的不同。A图灵机和B图灵机之间的通讯只能通过纸带完成，A并不知道B是怎么计算的；但是λ不同，一个cleverly desigened A表达式，它是可以「窥探」B表达式是怎么工作的。

这是Ben Lynn给的比方。准确的说，如果给定两个不同的closed λ term，A和B，Böhm定理给出了一个算法可以构造一个λ表达式X，such that，XA是true但XB是false。这里true和false可以用任意两个不等的λ表达式代表。

++++

所以计算机科学领域奉为经典的图灵机和λ等价说，也要带一点盐摄入，并非是内涵和外延上完全的相等。

上个世纪后半夜一群数学家信心满满杀入计算机科学领域，虽然成果有不少但是工业上的很多实际问题未能得到良好解决，这导致计算机科学和计算机工程之间的鸿沟，和生物化学与烹饪的距离差不多。

从此之后理论计算机科学中相当的一部分「有了数学病却没有数学命」。但是，做计算机工程的人都知道一句话，魔鬼在细节里，这一点对理论领域也不例外。

所以这也许可以构成你该学好一阶逻辑，拓扑，集合，递归，范畴，然后打开Barendregt的λ book亲自一探究竟的原因，也或者，你还有兴趣看看伞哥在hol4里的工作。当然你也可能发现写在这里的东西，和伞哥的工作驴唇不对马嘴完全不是一回事，除了Böhm这个人名之外没有任何联系。但那又怎么样呢？Life is journey，not a destination，知道Böhm，Barendregt，和伞哥，在那些年的夏天究竟干了什么，不也很好么？反正你的时间闲着也是闲着，顶多刷刷微博。