可计算性

停机问题：给定一个只需要一个输入的程序 P，以及一个对象 x，判断程序 P 在以 x 作为输入时是否会停机

能否用代码实现一个函数 S ，它的参数是 P 和 x ：
1. 如果P(x) 停机，则 S 返回 true
2. 如果P(x) 死循环，则 S 返回 false 

假设可以编写一个过程 isStop ，如果 P(x) 能停机 ，则 isStop 返回 true , 否则返回 false

int isStop(int (*P) (int) , void *x)
{
    // 0 : false, 1 : true
}

死循环定义为：

int loop-forever(int x)
{
    for( ; ; ) {
    }
}

显然有：

isStop(loop-ever, 1) = 0 // false

现在定义一个辅助过程 diag ：

int diag(int (*x) (int))  
{
    if(isStop(x, x))
        loop-forever(1);
    else
        return 42;
}

接下来的问题就是： diag(diag) 的值是多少？

• 如果diag(diag) 触发死循环 ，意味着 isstop(diag, diag)为 true ，根据 isStop 的定义，推理得 diag(diag) 应该停机，这和 diag(diag) 产生死循环相悖
• 如果 diag(diag) 返回 42 ，意味着 isstop(diag, diag) 为 false ，根据 isStop 的定义，可以得到 diag(diag) 不会停机，这和 diag(diag) 返回 42 相悖

根据上面的分析，可以推理出： 过程 isStop 可以被编写 这个假设是 错误的

    停机问题是一个不可被计算的函数，这意味着存在一个函数，可以被定义，但是无法被编程

把思绪回到1931年，那个数学界风起云涌的年代，一个名不经传的20出头的学生，在他的博士论文中证明了一个惊天动地的结论

    在那个年代，希尔伯特的数学天才就像太阳的光芒一般夺目，在关于数学严格化的大纷争中希尔伯特带领的形式主义派系技压群雄，得到许多当时有名望的数学家的支持

    希尔伯特希望借助于 形式化 的手段，抽掉数学证明中的意义
    把数学证明抽象成一堆无意义的符号转换，就连人类赖以自豪的逻辑推导，也不过只是一堆堆符号转换而已

    这样一来，一个日常所谓的，带有直观意义和解释的数学系统就变成了一个纯粹由无意义符号表达的、公理加上推导规则所构成的形式系统
    而数学证明呢，只不过是在这个系统内玩的一个文字游戏

    令人惊讶的是，这样一种做法，真的是可行的！数学的意义，似乎竟然真的可以被抽掉！
    另一方面，一个形式系统具有非常好的性质，平时人们证明一个定理所动用的推导，变成了纯粹机械的符号变换

    希尔伯特希望能够证明，在任一个无矛盾的形式系统中所能表达的所有陈述都要么能够证明要么能够证伪
    这看起来是个非常直观的结论，因为一个结论要么是真要么是假
    而它在它所处的领域/系统中当然应该能够证明或证伪了（只要我们能够揭示出该系统中足够多的真理）

然而，哥德尔的证明无情的击碎了这一企图，哥德尔的证明揭示出， 任何足够强到蕴含了皮亚诺算术系统（PA）的一致（即无矛盾）的系统都是不完备的 ，所谓不完备也就是说在 系统内存在一个为真但无法在系统内推导出的命题 。这在当时的数学界揭起了轩然大波，其证明不仅具有数学意义，而且蕴含了深刻的哲学意义。从那时起这一不完备性定理就被引申到自然科学乃至人文科学的各个角落…至今还没有任何一个数学定理居然能够产生这么广泛而深远的影响

哥德尔的证明非常的长，达到了200多页纸，但其中很大的成分是用在了一些辅助性的工作上面，比如占据超过1/3纸张的是关于一个形式系统如何映射到自然数，也就是说，如何 把一个形式系统中的所有公式都表示为自然数 ，并可以 从一自然数反过来得出相应的公式 。这其实就是 编码 ，现在看来是很显然的：

• 因为一个程序就可以被编码成 二进制数 ，反过来也可以 解码 。但是在当时这是一个全新的思想，也是最关键的辅助性工作之一
• 这正是 程序即数据 的最初想法

现在要证明哥德尔的不完备性定理，只需在假定的 形式系统 T 内表达出一个为 真 但无法在 T 内 推导 出（证明）的 命题 。于是哥德尔构造了这样一个命题 P : T 系统内无法证明 P ，这里的系统 T 当然就是命题 P 所处的形式系统

    哥德尔构造的命题其实就是 “我不可以被证明”，跟著名的说谎者悖论非常相似，只是把“说谎”改成了“不可以被证明”

如果这个命题能够在 T 内表达出来，就可以得出 P为真但无法在T内推导出来 的结论，从而证明 T 的不完备性 ：

1. 假设 T 可以证明出 P ，而因为 P 说的就是 P不可在系统T内证明 ，于是又得到 T 无法证明出P ，产生矛盾
2. 这说明假设 T可以证明P 是错误的，根据排中律，得到 T不可以证明P
3. 由于P说的正是“T系统内无法证明P”，所以 P 就成了一个 正确的命题，同时无法由T内证明 ！

    如果你足够敏锐，你会发现上面这番推理本身不就是证明吗？其证明的结果不就是 P 是正确的？

    然而实际上这番证明是位于 T 系统之外的，它用到了一个关于T系统的假设“T是一致（无矛盾）的”

    这个假设并非T系统里面的内容，所以刚才其实是在T系统之外推导出了P是正确的

    这跟 P 不能在 T 之内推导出来并不矛盾。所以别担心，一切都正常

那么，剩下来最关键的问题就是 如何用形式语言在T内表达出这个P ，上面的理论虽然漂亮，但如果 P 根本没法在 T 内表达出来，又如何能证明 T 内存在这个为真但无法被证明的 P 呢？

于是，就有了哥德尔证明里面最核心的构造，哥德尔构造了这样一个公式：

N(n) is unprovable in T

这个公式由两部分构成：

• n : 这个公式的自由变量，它是一个 自然数 ，一旦给定，那么这个 公式就变成一个明确的命题
• N : 从 n 解码 出的货真价实的（常见的符号形式的） 公式
  • 哥德尔的证明第一部分就是把公式编码
• is unprovable in T ：一个谓词，这里没有用 形式语言 而是用 自然语言 表达出来的
  • 哥德尔证明了它是可以用形式语言表达出来的，大致思路就是：一个形式系统中的符号数目是有限的，它们构成这个形式系统的符号表
  • 可以依次枚举出所有长度为1的串，长度为2的串，长度为3的串…
  • 根据 形式系统 给出的 语法规则 ，可以检查每个串是否是 良构 的公式，其实也就是说，是否符合语法规则
    • 一个形式系统是需要语法规则的，比如逻辑语言形式化之后就会看到 P->Q 是良构，而 ->PQ 则不是
    • 因而可以 枚举出所有的良构的公式来
  • 观察到 形式系统中的证明 也不过就是由一个个的 良构公式构成的序列
    • 推导的过程，不就是一个公式接一个公式嘛，而良构公式构成的序列本身同样也是由 符号表内的符号构成的串
    • 所以只需枚举所有的串，对每一个串检查它是否是一个由良构公司构成的序列（证明）：
      • 如果是，则记录下这个良构公式序列（证明）的最后一个良构公式，也就是它的 结论 。这样便枚举出了 所有的可由 T 推导出的定理
  • 为了表达出 X is unprovable in T ，本质上只需说 不存在这样一个自然数 S，它所解码出来的良构序列以 X 为终结 ！

现在用 UnPr(X) 来表达 X is unprovable in T ，于是哥德尔的公式变成了：

UnPr( N(n) )

现在，到了最关键的部分，首先把这个 公式 简记为 G(n) ：

G(n) : UnPr( N(n) )

但别忘了 G 内有一个自由变量 n，所以G现在还不是一个命题，而只是一个公式，所以谈不上真假

由于 G 也是个 良构的公式 ，所以它也有自己的 编码 g ，当然 g 是一个自然数，现在我们把 g 作为 G 的参数 ，也就是说， 把 G 里面的自由变量 n替换为 g ，于是得到一个真正的 命题 ：

G(g) : UnPr( G(g) )

用自然语言来说，这个命题 G(g) 说的就是 我是不可在T内证明的 。而一开始已经讲过了如何用这个命题来推断出 G(g) 为真但无法在 T 内证明 ，于是这就证明了 哥德尔的不完备性定理

    哥德尔的不完备性定理被称为20世纪数学最重大的发现

    现在知道为真但无法在系统内证明的命题不仅仅是这个诡异的“哥德尔命题”，还有很多真正有意义的明确命题
    其中最著名的就是连续统假设，此外哥德巴赫猜想也有可能是个没法在数论系统中证明的真命题

    大道至简，看上去最复杂的理论其实建立在一个最简单最纯粹的道理之上

康托尔在 无穷集合 和 超限数 方面的工作主要集中在两篇突破性的论文上，这里就不过多谈论数学的细节了，只说康托尔引入对角线方法的动机和什么是对角线方法

绝大多数人刚接触停机问题的时候都有一个问题，图灵怎么能够想到这么诡异的证明，怎么能构造出那个诡异的 说停机又不停机，说不停机又停机 的悖论机器。马上就会看到，这其实只是对角线方法的一个直接结论

还是从反证开始，假设存在这样一个 图灵机 ，它能够 判断 任何程序 在 任何输入 上是否 停机

由于 所有图灵机构成的集合 是一个 可列集 ，所以我们可以很自然地列出下表，它表示每个图灵机分别在每一个 可能的输入 （1, 2, 3,…）下的 输出 ：

• N : 无法停机

• 其余数值： 停机后的输出

        类似哥德尔理论可以把每个图灵机映射到一个自然数，因此能够逐一列出所有的图灵机
  

  Table 1: 图灵机对角线

  	1	2	3	4	…
  M1	N	1	N	N	…
  M2	2	0	N	0	…
  M3	0	1	2	0	…
  M4	N	0	5	N	…
  …

  M1，M2，M3 … 是逐一列出的图灵机，
  
  注意：由于程序即数据，每个图灵机都有唯一索引（编码）
  所以规定在枚举图灵机的时候 Mi 其实就代表编码为 i 的图灵机
  
  当然这里很多图灵机将会是根本没用的玩意，但这不要紧
  
  最上面的一行1 2 3 4 … 是输入数据
  比如矩阵的第一行代表 M1 分别在1，2，3，…上面的输出，不停机的话就是 N 
  

  刚才假设存在这样一个图灵机 H ，它能够判断任何程序在任何输入上能否停机，换句话说， H(i,j) 能够给出 Mi(j) 是 N（不停）呢还是给出一个具体的结果（停）, 其中 i 是 Mi 的 索引 （编码）

  现在来运用康托尔的对角线方法，构造一个新的图灵机 P ：

• P 在 1 上的输出行为跟 M1(1) 不一样
• P 在 2 上的输出行为跟 M2(2) 不一样
• …

总之 P 在输入 i 上的输出跟 Mi(i) 不一样 。只需利用一下万能的 H ，这个图灵机 P 就不难构造出来，如下：

int P (int i) 
{
    if(H(i, i) == 1)  // Mi(i) 停机
        return 1 + Mi(i); // 返回停机后的数值 + 1 
    else // Mi(i) 不停机
        return 0;
}

    也就是说：

    如果 Mi(i) 停机，那么 P(i) 的输出就是 Mi(i) + 1
    如果 Mi(i) 不停机的话，P(i)就停机且输出0

    这就保证了 P(i) 的输出行为跟 Mi(i) 反正不一样 

注意：这个 P 本身是一个图灵机，而上面已经列出了所有的图灵机，所以必然存在一个 k ，使得 Mk = P 。而 两个图灵机相等 当且仅当 它们 对于所有的输入都相等 ，也就是说对于任取的 n ，有 Mk(n) = P(n) ，现在令 n = k ，得到 Mk(k)=P(k) ，根据上面给出的 P 的定义，这实际上就是：

Mk(k) = P(k) ， 根据 P 的定义：

如果 Mk(k) 停机： Mk(k) = P(k) = 1 + Mk(k) 
如果 Mk(k) 不停机：Mk(k) = P(k) = 0，这意味着 Mk(k) 停机

不管哪种情况都是矛盾。于是得出， 不存在那样的 H ，无论多聪明的 H，总存在一个图灵机的停机行为是它无法判断的

    这跟哥德尔定理“无论多‘完备’的形式化公理系统，都存在一个‘哥德尔命题’是无法在系统内推导出来的”从本质上其实是一模一样的

    只不过一般把图灵的停机问题称为“可判定问题”，而把数学的称为“可证明问题”

    如果把那个无法判定是否停机的图灵机作为算法的特例纳入到 我们的 H 当中呢？
    我们把得到的新的判定算法记为H1。然而，可惜的是，在H1下，我们又可以相应地以同样的手法从H1构造出一个无法被它（H1）判定的图灵机来
    你再加，我再构造，无论你加多少个特例进去，我都可以由同样的方式构造出来一个你无法够到的图灵机，以彼之矛，攻彼之盾

    其实这也是哥德尔定理最深刻的结论之一：
    哥德尔定理其实就说明了无论你给出多少个公理，即无论你建立多么完备的公理体系，这个系统里面都有由你的那些公理出发所推导不到的地方
    这些黑暗的角落，就是人类直觉之光才能照射到的地方

对角线方法 能够揭示出 某种自指结构 ，从而构造出一个 悖论图灵机 。实际上，对角线方法是一种有深远影响的方法，哥德尔的证明其实也是这个方法的一则应用。证明与上面的停机问题证明如出一辙，只不过把 Mi 换成了一个 形式系统 内的 公式 fi

现在来简单的看一下这个奇妙方法的几个不那么明显的推论

学过逻辑的人肯定是知道著名的 罗素悖论 的，用数学的形式来描述就是：

R = {X: X不属于X} 

这个悖论最初是从康托尔的 无穷集合论 里面引申出来的。当初康托尔在思考 无穷集合 的时候发现可以称 一切集合的集合 ，这样一个集合由于它本身也是一个集合，所以它就属于它自身。也就是说，现在可以称世界上存在一类 属于自己的集合 ，除此之外当然就是 不属于自己的集合 了。把 所有不属于自己的集合收集起来 做成一个集合 R ，这就是上面这个著名的 罗素悖论 了

R 是否属于 R？：

• 如果 R 属于 R，根据 R 的定义，R 就不应该属于 R

• 如果 R 不属于 R ，则再次根据 R 的定义，R就应该属于R

        这个悖论促使了集合论的 公理化 。后来策梅罗公理化的集合论里面就 *不允许X属于X* 
  
        尽管如此还是没法证明这样的集合论不可能产生出新的悖论。而且永远没法证明，这就是哥德尔第二不完备性定理的结论。
        一个包含了PA的形式化公理系统永远无法在内部证明其自身的一致（无矛盾）性
  
        从而希尔伯特想从元数学推出所有数学系统的一致性的企图也就失败了
        因为元数学的一致性又得由元元数学来证明
        后者的一致性又得由元元元数学来证明。。。
  

  这里只关心罗素是如何想出这个绝妙的悖论的。还是 对角线方法 ！ 罗列出所有的集合：S1,S2,S3 …

  Table 2: 罗素悖论的对角线

  	S1	S2	S3	…
  S1	0	1	1	…
  S2	1	1	0	…
  S3	0	0	0	…
  …

  右侧纵向列出所有集合，顶行横向列出所有集合
  
  0/1矩阵的 (i,j) 处的元素表示 Si 是否包含 Sj，记为 Si(j)
  

  现在只需构造一个新的 0/1 序列 L ，它的第 i 位与矩阵的 (i,i) 处的值恰恰相反： L(i) = 1-Si(i)

  这个新的序列其实对应了一个 集合 ，不妨也记为 L， L(i) 表示 L 是否包含 Si 。根据 L 的定义：

  • 如果矩阵的 (i,i) 处值为 0 ：
    • Si(i) = 0 ： Si不包含Si
    • L(i) = 1 : L 包含 Si
  • 如果矩阵的 (i,i) 处值为1 ：
    • Si(i) = 1 : Si包含Si
    • L(i) = 0 ： L 不包含 Si

  注意：这个新的集合 L 肯定等于 某个 Sk （因为我们已经列出了所有的集合）， L = Sk 。既然 L 与 Sk 是同一集合，那么它们肯定 包含同样的元素 ，从而对于任意 n ，有 L(n) = Sk(n) 。于是通过令 n=k ，得到 L(k) = Sk(k) ，而根据L的定义， L(k) = 1- Sk(k) 。这就有 Sk(k) = 1-Sk(k) ，产生矛盾！

  通过抽象简化以上过程，可以看到，我们构造的 L 其实是 包含了所有不包含它自身的集合的集合 ，用数学的描述正是 罗素悖论

        敏锐的你可能会注意到所有集合的数目是不可数的，从而根本不能 S1, S2… 的一一列举出来
  
        没错，但通过假设它们可以列举出来，我们发现了一个与可列性无关的悖论
  
        所以这里的对角线方法其实可以说是一种启发式方法。
  
        同样的手法也可以用到证明P(A)：A的所有子集构成的集合，也叫幂集无法跟A构成一一对应上面
  

    希尔伯特是在1900年巴黎数学家大会上提出著名的希尔伯特第十问题的

    简言之就是是否存在一个算法，能够计算任意丢番图方程是否有整根

要解决这个问题，就得先严格定义 算法 这一概念。为此图灵和丘齐分别提出了图灵机和lambda calculus这两个概念，它们从不同的角度抽象出了 有效（机械）计算 的概念，著名的 图灵–丘齐命题 就是说： 所有可以有效计算出来的问题都可以由图灵机计算 出来

• 丘齐的 lambda 演算 其实就是 数学推理系统的一个形式化

• 图灵机 则是把这个 数学概念物理化 了

  因为图灵机的概念隐含了实际的物理实现，所以冯・诺依曼才据此提出了奠定现代计算机体系结构的 冯・诺依曼体系结构 ，其遵循的，正是图灵机的概念。而 程序即数据 的理念，这个发端于数学家哥德尔的不完备性定理的证明之中的理念，则早就在黑暗中预示了可编程机器的必然问世

对角线方法是如何 简洁而深刻 地揭示出 递归结构 的。著名的 不完备性定理 、 停机问题 、 Y 组合子 、 罗素悖论 等等如何通过这一简洁优美的方法推导出来

      这一诞生于康托尔的天才的手法如同一条金色的丝线，把位于不同年代的伟大发现串联了起来，并且将一直延续下去