Liar Paradox and Halting Problem

Liar Paradox
首先来看一下什么是liar paradox。Liar paradox的雏形来自于一个叫作Epimenides的克里特人，他说：“所有克里特人都是说谎者。”这常常被认为等同于liar paradox，其实不然，因为如果他说的是真话，那么他就在说谎；如果他在说谎，说明至少还有一个克里特人说的是真话，这并不矛盾。最早的liar paradox版本是由生活在公元前4世纪希腊的麦加拉学派（Megarian）哲学家Eubulides提出的。他说：

A man says that he is lying. Is what he says true or false?

如果他说的是真的，那么他在说谎；如果他说的假的，那么他没在说谎。

后来又出现了一些liar paradox的变种，比较有名的有：

This sentence is false.

下面的悖论又名"Jourdain's Card Paradox"：有一张卡片，一面写着：

The sentence on the other side of this card is true.

而在卡的另一面却写着：

The sentence on the other side of this card is false.

Halting Problem
Halting Problem是计算理论中的经典问题。它的意思，简而言之就是：对于一段程序和有限的输入，决定其是终止还是永久运行。说白了就是设计一个算法来判断一段程序是否会进入死循环。Alan Turing在1936年证明了不存在这样的算法。

在SICP课程的最后一讲[4]中，为了说明不是任何事物都是可计算的，使用了这样一个例子来证明不存在halting problem的算法。

首先，假设存在这样的算法，则存在函数(halts? p)：

（halts? p)
=> #t if (p) terminates
=> #f if (p) does not terminates

现在有如下程序：

(define (contradict-halts)
    (if (halts? contradict-halts)
        (loop-forever)
        #t))

(contradict-halts)
=> ???????

很容易，我们可以定义(loop-forever)为：

(define (loop-forever)
    ((lambda (x) (x x))
    (lambda (x) (x x))))

这就是著名的Y combinator。

这里使用的就是liar paradox的精髓，如果这段程序会终止，则让它无限循环；如果程序不终止，则让它返回#t。

Resources
[1]. Liar paradox on Wikipedia.org
[2]. Some paradox
[3]. Halting problem on Wikipedia.org
[4]. Video courses of SICP