康托的对角线证法

证明实数是不可数无穷集的著名论证

第1个回答  2008-05-28
停机问题
不存在这样一个程序(算法),它能够计算任何程序(算法)在给定输入上是否会结束(停机)。

那么,如何来证明这个停机问题呢?反证。假设我们某一天真做出了这么一个极度聪明的万能算法(就叫God_algo吧),你只要给它一段程序(二进制描述),再给它这段程序的输入,它就能告诉你这段程序在这个输入上会不会结束(停机),我们来编写一下我们的这个算法吧:

bool God_algo(char* program, char* input)
{
if(<program> halts on <input>)
return true;
return false;
}

这里我们假设if的判断语句里面是你天才思考的结晶,它能够像上帝一样洞察一切程序的宿命。现在,我们从这个God_algo出发导出一个新的算法:

bool Satan_algo(char* program)
{
if( God_algo(program, program) ){
while(1); // loop forever!
return false; // can never get here!
}
else
return true;
}

正如它的名字所暗示的那样,这个算法便是一切邪恶的根源了。当我们把这个算法运用到它自身身上时,会发生什么呢?

Satan_algo(Satan_algo);

我们来分析一下这行简单的调用:

显然,Satan_algo(Satan_algo)这个调用要么能够运行结束返回(停机),要么不能返回(loop forever)。

如果它能够结束,那么Santa_algo算法里面的那个if判断就会成立(因为God_algo(Santa_algo,Santa_algo)将会返回true),从而程序便进入那个包含一个无穷循环while(1);的if分支,于是这个Satan_algo(Satan_algo)调用便永远不会返回(结束)了。

而如果Satan_algo(Satan_algo)不能结束(停机)呢,则if判断就会失败,从而选择另一个if分支并返回true,即Satan_algo(Satan_algo)又能够返回(停机)。

总之,我们有:

Satan_algo(Satan_algo)能够停机=> 它不能停机
Satan_algo(Satan_algo)不能停机=> 它能够停机

所以它停也不是,不停也不是。左右矛盾。

于是,我们的假设,即God_algo算法的存在性,便不成立了。正如拉格朗日所说:“陛下,我们不需要(上帝)这个假设”[4]。

这个证明相信每个程序员都能够容易的看懂。然而,这个看似不可捉摸的技巧背后其实隐藏着深刻的数学原理(甚至是哲学原理)。在没有认识到这一数学原理之前,至少我当时是对于图灵如何想出这一绝妙证明感到无法理解。但后面,在介绍完了与图灵的停机问题“同构”的Y combinator之后,我们会深入哥德尔的不完备性定理,在理解了哥德尔不完备性定理之后,我们从这一同样绝妙的定理出发,就会突然发现,离停机问题和神奇的Y combinator只是咫尺之遥而已。当然,最后我们会回溯到一切的尽头,康托尔那里,看看停机问题、Y combinator、以及不完备性定理是如何自然而然地由康托尔的对角线方法推导出来的,我们将会看到这些看似神奇的构造性证明的背后,其实是一个简洁优美的数学方法在起作用。

Y Combinator
了解Y combinator的请直接跳过这一节,到下一节“哥德尔的不完备性定理”。

让我们暂且搁下但记住绕人的图灵停机问题,走进函数式编程语言的世界,走进由跟图灵机理论等价的lambda算子发展出来的另一个平行的语言世界。让我们来看一看被人们一代一代吟唱着的神奇的Y Combinator…

关于Y Combinator的文章可谓数不胜数,这个由师从希尔伯特的著名逻辑学家Haskell B.Curry(Haskell语言就是以他命名的,而函数式编程语言里面的Curry手法也是以他命名)“发明”出来的组合算子(Haskell是研究组合逻辑(combinatory logic)的)仿佛有种神奇的魔力,它能够算出给定lambda表达式(函数)的不动点。从而使得递归成为可能。事实上,我们待会就会看到,Y Combinator在神奇的表面之下,其实隐藏着深刻的意义,其背后体现的意义,曾经开出过历史上最灿烂的数学之花,所以MIT的计算机科学系将它做成系徽也就不足为奇了[5]。

当然,要了解这个神奇的算子,我们需要一点点lambda算子理论的基础知识,不过别担心,lambda算子理论是我目前见过的最简洁的公理系统,这个系统仅仅由三条非常简单的公理构成,而这三条公理里面我们又只需要关注前两条。

以下小节——lambda calculus——纯粹是为了没有接触过lambda算子理论的读者准备的,并不属于本文重点讨论的东西,然而要讨论Y combinator就必须先了解一下lambda(当然,以编程语言来了解也行,但是你会看到,丘齐最初提出的lambda算子理论才是最最简洁和漂亮的,学起来也最省事。)所以我单独准备了一个小节来介绍它。如果你已经知道,可以跳过这一小节。不知道的读者也可以跳过这一小节去wikipedia上面看,这里的介绍使用了wikipedia上的方式

lambda calculus
先来看一下lambda表达式的基本语法(BNF):

<expr> ::= <identifier>
<expr> ::= lambda <identifier-list>. <expr>
<expr> ::= (<expr> <expr>)

前两条语法用于生成lambda表达式(lambda函数),如:

lambda x y. x + y

haskell里面为了简洁起见用“\”来代替希腊字母lambda,它们形状比较相似。故而上面的定义也可以写成:
\ x y. x + y

这是一个匿名的加法函数,它接受两个参数,返回两值相加的结果。当然,这里我们为了方便起见赋予了lambda函数直观的计算意义,而实际上lambda calculus里面一切都只不过是文本替换,有点像C语言的宏。并且这里的“+”我们假设已经是一个具有原子语义的运算符[6],此外,为了方便我们使用了中缀表达(按照lambda calculus系统的语法实际上应该写成“(+ x y)”才对——参考第三条语法)。

那么,函数定义出来了,怎么使用呢?最后一条规则就是用来调用一个lambda函数的:

((lambda x y. x + y) 2 3)

以上这一行就是把刚才定义的加法函数运用到2和3上(这个调用语法形式跟命令式语言(imperative language)惯用的调用形式有点区别,后者是“f(x, y)”,而这里是“(f x y)”,不过好在顺序没变:) )。为了表达简洁一点,我们可以给(lambda x y. x + y)起一个名字,像这样:

let Add = (lambda x y. x + y)

这样我们便可以使用Add来表示该lambda函数了:

(Add 2 3)

不过还是为了方便起见,后面调用的时候一般用“Add(2, 3)”,即我们熟悉的形式。

有了语法规则之后,我们便可以看一看这个语言系统的两条简单至极的公理了:

Alpha转换公理:例如,“lambda x y. x + y”转换为“lambda a b. a + b”。换句话说,函数的参数起什么名字没有关系,可以随意替换,只要函数体里面对参数的使用的地方也同时注意相应替换掉就是了。
Beta转换公理:例如,“(lambda x y. x + y) 2 3”转换为“2 + 3”。这个就更简单了,也就是说,当把一个lambda函数用到参数身上时,只需用实际的参数来替换掉其函数体中的相应变量即可。

就这些。是不是感觉有点太简单了?但事实就是如此,lambda算子系统从根本上其实就这些东西,然而你却能够从这几个简单的规则中推演出神奇无比的Y combinator来。我们这就开始!

递归的迷思
敏锐的你可能会发现,就以上这两条公理,我们的lambda语言中无法表示递归函数,为什么呢?假设我们要计算经典的阶乘,递归描述肯定像这样:

f(n):
if n == 0 return 1
return n*f(n-1)

当然,上面这个程序是假定n为正整数。这个程序显示了一个特点,f在定义的过程中用到了它自身。那么如何在lambda算子系统中表达这一函数呢?理所当然的想法如下:

lambda n. If_Else n==0 1 n*<self>(n-1)

当然,上面的程序假定了If_Else是一个已经定义好的三元操作符(你可以想象C的“?:”操作符,后面跟的三个参数分别是判断条件、成功后求值的表达式、失败后求值的表达式。那么很显然,这个定义里面有一个地方没法解决,那就是<self>那个地方我们应该填入什么呢?很显然,熟悉C这类命令式语言的人都知道应该填入这个函数本身的名字,然而lambda算子系统里面的lambda表达式(或称函数)是没有名字的。

怎么办?难道就没有办法实现递归了?或者说,丘齐做出的这个lambda算子系统里面根本没法实现递归从而在计算能力上面有重大的缺陷?显然不是。马上你就会看到Y combinator是如何把一个看上去非递归的lambda表达式像变魔术那样变成一个递归版本的。在成功之前我们再失败一次,注意下面的尝试:

let F = lambda n. IF_Else n==0 1 n*F(n-1)

看上去不错,是吗?可惜还是不行。因为let F只是起到一个语法糖的作用,在它所代表的lambda表达式还没有完全定义出来之前你是不可以使用F这个名字的。更何况实际上丘齐当初的lambda算子系统里面也并没有这个语法元素,这只是刚才为了简化代码而引入的语法糖。当然,了解这个let语句还是有意义的,后面还会用到。

一次成功的尝试
在上面几次失败的尝试之后,我们是不是就一筹莫展了呢?别忘了软件工程里面的一条黄金定律:“任何问题都可以通过增加一个间接层来解决”。不妨把它沿用到我们面临的递归问题上:没错,我们的确没办法在一个lambda函数的定义里面直接(按名字)来调用其自身。但是,可不可以间接调用呢?

我们回顾一下刚才不成功的定义:

lambda n. If_Else n==0 1 n*<self>(n-1)

现在<self>处不是缺少“这个函数自身”嘛,既然不能直接填入“这个函数自身”,我们可以增加一个参数,也就是说,把<self>参数化:

lambda self n. If_Else n==0 1 n*self(n-1)

上面这个lambda算子总是合法定义了吧。现在,我们调用这个函数的时候,只要加传一个参数self,这个参数不是别人,正是这个函数自身。还是为了简单起见,我们用let语句来给上面这个函数起个别名:

let P = lambda self n. If_Else n==0 1 n*self(n-1)

我们这样调用,比如说我们要计算3的阶乘:

P(P, 3)

也就是说,把P自己作为P的第一个参数(注意,调用的时候P已经定义完毕了,所以我们当然可以使用它的名字了)。这样一来,P里面的self处不就等于是P本身了吗?自身调用自身,递归!

可惜这只是个美好的设想,还差一点点。我们分析一下P(P, 3)这个调用。利用前面讲的Beta转换规则,这个函数调用展开其实就是(你可以完全把P当成一个宏来进行展开!):

IF_Else n==0 1 n*P(n-1)

看出问题了吗?这里的P(n-1)虽然调用到了P,然而只给出了一个参数;而从P的定义来看,它是需要两个参数的(分别为self和n)!也就是说,为了让P(n-1)变成良好的调用,我们得加一个参数才行,所以我们得稍微修改一下P的定义:

let P = lambda self n. If_Else n==0 1 n*self(self, n-1)

请注意,我们在P的函数体内调用self的时候增加了一个参数。现在当我们调用P(P, 3)的时候,展开就变成了:

IF_Else 3==0 1 3*P(P, 3-1)

而P(P, 3-1)是对P合法的递归调用。这次我们真的成功了!

不动点原理
然而,看看我们的P的定义,是不是很丑陋?“n*self(self, n-1)”?什么玩意?为什么要多出一个多余的self?DRY!怎么办呢?我们想起我们一开始定义的那个失败的P,虽然行不通,但最初的努力往往是大脑最先想到的最直观的做法,我们来回顾一下:

let P = lambda self n. If_Else n==0 1 n*self(n-1)

这个P的函数体就非常清晰,没有冗余成分,虽然参数列表里面多出一个self,但我们其实根本不用管它,看函数体就行了,self这个名字已经可以说明一切了对不对?但很可惜这个函数不能用。我们再来回想一下为什么不能用呢?因为当你调用P(P, n)的时候,里面的self(n-1)会展开为P(n-1)而P是需要两个参数的。唉,要是这里的self是一个“真正”的,只需要一个参数的递归阶乘函数,那该多好啊。为什么不呢?干脆我们假设出一个“真正”的递归阶乘函数:

power(n):
if(n==0) return 1;
return n*power(n-1);

但是,前面不是说过了,这个理想的版本无法在lambda算子系统中定义出来吗(由于lambda函数都是没名字的,无法自己内部调用自己)?不急,我们并不需要它被定义出来,我们只需要在头脑中“假设”它以“某种”方式被定义出来了,现在我们把这个真正完美的power传给P,这样:

P(power, 3)

注意它跟P(P, 3)的不同,P(P, 3)我们传递的是一个有缺陷的P为参数。而P(power, 3)我们则是传递的一个真正的递归函数power。我们试着展开P(power, 3):

IF_Else 3==0 1 3*power(3-1)

发生了什么??power(3-1)将会计算出2的阶乘(别忘了,power是我们设想的完美递归函数),所以这个式子将会忠实地计算出3的阶乘!

回想一下我们是怎么完成这项任务的:我们设想了一个以某种方式构造出来的完美的能够内部自己调用自己的递归阶乘函数power,我们发现把这个power传给P的话,P(power, n)的展开式就是真正的递归计算n阶乘的代码了。

相关了解……

你可能感兴趣的内容

本站内容来自于网友发表,不代表本站立场,仅表示其个人看法,不对其真实性、正确性、有效性作任何的担保
相关事宜请发邮件给我们
© 非常风气网