@裴喜龙 老师太看得起我了，我真的只是个程序员[允悲]。王小平教授的说法应该是给计算理论的入门者的不深奥的解释，但即便如此其中很多表述我也不懂。但我仍然感谢裴老师在微博上展开严肃学术讨论，我只能知无不言言无不尽，说错了怪我。[二哈]

++++

我要先说一些大的前提，我相信这个前提对很多和我类似的非数学或专业CS理论背景的人，有参考价值。因为我有几年的时间兜兜转转不得入门之法，非常的frustrated；到现在我也没有什么逻辑学和计算机语言理论的造诣可言，但我可以说我知道怎么入门了。

哲学，物理，数学，和计算，是四件不同的事情。

我是物理背景的；物理（以及电子，通讯）是一门什么样的学科呢？用柯南的话说，真相只有一个。即使说物理学还没有达到基本作用全部统一，但不妨碍我们相信任何物理现象背后它具有唯一的模型，只是这个模型它可能有混杂的地方，比如既需要考虑电磁作用，又有热力学的影响，甚至有量子效应，但这只是在说，它要满足所有的方程，而不是再说，它有多个不同的理论解释。

++++

数学不是这样的，至少现代数学不是。

计算机语言理论源自逻辑学，这个是对的，我至少看到过Per Martin-Lof原话说逻辑语言的表达力不够，所以计算科学家们不断在发明他们需要的表达力的语言。但这个表述不算严格，因为逻辑系统的extension，是有严格定义的，类似代数系统的extension，Martin-lof的表述应该不是指这个意思。

数理逻辑的发展有一些milestone，但非常非常重要的一个问题是，绝大多数数理逻辑发展的目的，是为了数学，不是为了计算；这一点必须放在考虑问题时的首要位置。希尔伯特拥抱公理化方法之后，希望盖一个完美的数学大厦，用公理系统描述所有的数学，从算术系统开始；而哥德尔不完备定理，说这件事情不可能。

哥德尔不完备是一个特别deep and profound的结果。它让很多数学家反反复复回到这个远点重新思考和重新出发。这里要指出数学本身作为一个抽象学科的问题所在。数学非常抽象，但是它的information content，不管什么理论，不是包罗一切的，无论它的符号是什么含义，当它组合在一起时它能表达的语义，就是formula的数量，就象信息论里的编码一样，你编码空间就那么大，或者是可列的，不能寄希望于道生一一生二二生万物，二生无穷这个是可以的，但二生万物不能。这是和物理学或其它自然科学相比巨大的思维差异。自然科学首先有无穷的现象（哲学：存在先于本质），如果有新的现象超越了已有的理论，那你仍然可以不断的观察现象摸索规律，你不会因为发现了新的现象把老的掀了，就算是量子力学和相对论，都不是对牛顿力学的否定，因为在两者之间有巨大的宏观尺度，牛顿力学就是对的，『足够好的近似。』

但数学是回到原点掀桌子的，因为并没有无穷尽的现象给你研究。你要有新的insight，新的method，新的tools，就得倒回去看哪儿可能出了问题，怎么改才行。至少在逻辑学这个方向，这是干了很多次的。

所以孤立的拿出来一个数学定理期望它有多么profound的影响不断去参透它，象大家不断的思考热力学第二定律的限制那样，这个通常会产生很大的困惑，和不适用的想法；保守的做法更好，先理解它的目的和上下文，在最小的环境下理解然后再看能不能有更大范围的适用性。这样不容易产生太多困惑和矛盾。

哥德尔不完备对于逻辑学当然是非常重要的。但是它有个前提，是算术的假设，希尔伯特给它的证明论加上了有限（finitary method）的限制，直觉的理解可以是证明的步骤是有限的，证明是不断的apply rules，得到一个sequence。

但哥德尔不完备不是证明论的终点，实际上Gentzen的工作在非常大的意义上不逊于哥德尔的。Gentzen打破了这个finitary method的限制，等于是说引入了更强的规则（在meta theory层面上，逻辑学区分theory和meta theory，前者是被研究的对象，后者是推演这些formula，证明论所说的rules，都不是theory level的，都是meta theory level的），他证明了他的系统的一致性。我不确定这是不是王教授说的『加固』。

现代逻辑学的方向非常多，而且和计算机应用相关的也非常多，经典逻辑（predicate），高阶逻辑（HOL），直觉逻辑，时序逻辑（modal logic的一种，在model checking中广泛使用），substructural logic（rust的linear logic和affine type？）等等。绝大多数，是被当作数学（模型）使用的，其中的一些，和计算机语言理论的关系紧密（直觉逻辑，substructural logic）。

CMU三剑客（Steve Awodey，Robert Harper，Frank Pfenning）搭起来的计算机语言理论框架，Category Theory，Proof Theory，Type Theory，以直觉逻辑为核心。反而和经典逻辑关系不大。

经典逻辑的很多成功和可计算理论的关系更大一系。而且MIT的课程上，第一课，Sipser开门见山的说，他搞了一辈子这个领域，但是也要诚实的告诉大家，这个领域中的重大理论问题，框架性的工作，在1950年之前就差不多结束了，之后都是修修补补没有特别大的进展。我的理解，哥德尔的工作就算这个时期的重大理论问题之一了。

++++

计算机语言理论，John C. Reynolds的早一点的教材里比较了Logic语言和Programming Language。他归纳的，两者都有ast（abstract syntax），denotational semantics（语义），inference rules，binding/substitution。

两者的不同，逻辑语言没有停机问题；在Harper的书上，如果我的理解不错的话，现代计算语言理论更常用dynamics来表达，计算语言是表述『计算』的。

这个地方要抽丝剥茧的理开差异是有点费劲的。个人的理解，核心在那个denotational semantics上。denotation这个词本来是语言学上来的，早期的逻辑学家的数理逻辑书上（例如Church的）花大量的笔墨解释。比如说『微博CEO』『来去之间』『高飞王』，这都是name or composition of names，但几个形式上（form）不同的名词或词组指向了同一个人，就是那个有肉体的人（denotation）。逻辑学在早期非常艰苦的拆开了syntax和semantics，denotation就是meaning，是semantics。这一点没有意外，因为在第一代逻辑学家里，他们关心的都是数学，计算机还没有。

Lambda确实制造了一些麻烦。这个演算系统是不是也可以有denotational semantics呢？这是Dana Scott的工作，而且Dana Scott拿的是图灵奖，因为第一个图灵奖获得者Allen Perlis就确立了Lamba在计算机语言理论里的地位。在这个时候计算机语言理论还没有很高的独立性，它是应用数学。

这里有个插曲是曾经困扰我好几年的我也写出来。（untyped）Lambda是一个演算系统，或者更general的叫term rewriting system，这是关于（untyped）Lambda的最权威的一本书，Barendregt的The Lambda Calculus里明确表达的。这个Lambda里没有诸如true/false这样的语义（模型论）定义，所以它不是一个逻辑系统。

但是在经典逻辑里，现在一般称HOL，就是伞哥用的那个证明器的名字，Lambda用于表达Higher Order Logic，它比给每个Order一套带着下脚标的Quantifier的表达更简洁。HOL最初的论文，Church 1940，最早给出了Simple Type，但是它的目标跟发展Type Theory一毛钱关系也没有，当时大家还在热烈的探讨怎么消灭罗素悖论，Ramsey有一篇有影响力的文章，Church说你看我的Lambda干这个也行。

Type Theory里，Lambda一般被称为computation substrate；但是还是回到目的上说，这些人更关心证明器，更关心证明器里如何表达数学，因为类型论里有著名的Curry Howard Correspondence，即Program = Proof，这是这个语境下computation的含义，它实际上在说Lambda变换承载了证明步骤（熟悉科霍同构的人会知道formula or predicate，被编码在type里）。这里的Type Theory，表达成typed lambda也没有问题。

所以这里有untyped lambda（和计算理论或计算复杂度理论中的recursion theory对等，也和图灵机对等），pure lambda（Barendregt写了很厚的一本，Dana Scott的domain theory更多的隶属于这个部分），HOL（经典逻辑，高阶逻辑，而且现代HOL也有多态这些复杂的type了，只是它基于经典逻辑而不是直觉逻辑），typed lambda（计算机语言理论的主流跑到intuitionistic logic去了，但是CMU的大牛们非要另起炉灶一个新名字：constructive logic）。

这一段希望我的理解是对的，也欢迎有人讨论。Lambda作为一个演算工具在不同的系统里发挥着不同的角色，但是如果是自学成才选手，这里也会产生大量的frustration。

++++

denotational semantics应该还是有一些地方在用的，但是它显然已经在计算机语言理论中被踢出C位了，替代它的是operational semantics，来自Burstall的得意门生，Plotkin。Operational Semantics非常容易理解，而且对工程一个实际的编程语言也非常有用，但是它也给现代计算机语言理论埋下一个雷：这样定义的语义too dynamic，就象我们说和Java相比，JavaScript too dynamic一样。

在逻辑语言里，如果我们把逻辑语言看作一种方法论的话，如果要证明一个语言里的每个formula都具有某种属性，『唯一』的方法是用一种叫作structural induction的技术去从axiom开始证明，然后证明这个属性在所有的rules（or proof过程）里都hold；Harper的那本书里全是这样的证明，从头到尾；好消息是这个证明非常的『套路化』，坏消息则是，awkward。数学上很多东西让人感受到全局观，对称性等等。structural induction就是，太detail了。

证明器我用的不多，但证明器里也一样充斥着这个。但也许不是一个问题，因为证明器目前对专业的数学家而言也用量很大，如果他们不在抱怨，说明我的看法太肤浅了。但Harper书上的习题确实不怎么令人愉悦。

++++

一抬头发现码了快4000字了，赶紧打住。最后我们说，计算模型，这个不唯一。

Lambda是很好的sequential program的表达，但是并行和并发呢？至少目前计算机语言理论的书里还不能把Process Calculi完全踢出去。而且别忘了经典的automata还是计算模型，automata连接起来成为io automata也是并发或者并行的表达，有不少电子工程和通讯方向的人搞这类研究。还有Petri Net。未来可能还会有新的模型被提出来。

可能在非常多的时候，当我们听到诸如计算，类型，Lambda，逻辑等词汇的时候，我们得学会Isaiah Berlin在访谈节目里介绍哲学家如何思考那样，首先要问自己这个词汇的上下文是什么？这个问题的目的是什么？它试图解决什么问题？用哪个方法论。

所以说回来我非常赞同王小平教授表达的，大一统理论在我们这个时代完全是胡扯，一点可能性都看不到。我们只能接收彼此之间在哲学（认知论，比如经典逻辑语义的true vs直觉逻辑语义的provable），在对符号的interpretation上，存在对立和矛盾的理论中，选一个称手的解决问题的思维工具。

柯南说的真相只有一个，sorry，在逻辑学和计算科学里，不存在的。[二哈]

http://t.cn/A6prpYsb