大家好，我是大老李。不久前在大老李的微信群中，有一位聽眾轉(zhuǎn)了我一篇文章，是關(guān)于2016年國外研究者發(fā)表的一篇論文，這位研究者開發(fā)出了一個電腦程序，理論上，可以在有限的時間內(nèi)，驗證包括哥德巴赫猜想和黎曼猜想的正確性。

這篇論文中的發(fā)現(xiàn)非常有意思，我很想介紹給大家。但是看懂這篇論文需要的準(zhǔn)備知識比較多，好在多數(shù)準(zhǔn)備知識在大老李之前的節(jié)目中都或多或少提過了，比如哥德爾不完備定理，ZFC公理體系等。但欠缺的有關(guān)圖靈機（Turing Machine）的介紹，所以今天先給大家介紹下圖靈機。

（圖靈，1912年6月23日—1954年6月7日，英國科學(xué)家，數(shù)學(xué)家，被稱為計算機科學(xué)之父）

照例，大老李在介紹一個概念前，要先介紹下為什么要有這個概念。圖靈為什么要提出圖靈機這個概念呢？目的之一是為了回答希爾伯特和他的學(xué)生阿克曼（Wilhelm Ackermann）在1928年提出的一個問題：

是否存在一個算法，對某種形式化語言（Formal Language）中的邏輯命題，能夠判斷該命題的真假，并最終輸出判斷結(jié)果。這個問題后來被稱為“可判定性問題”（Entscheidungsproblem）。

我知道你聽了這個問題后還是一頭霧水，什么叫“形式化語言”，這里的“邏輯命題”和“算法”又是啥？那我繼續(xù)回溯一點歷史。這個問題最早可以追溯到17世紀(jì)的萊布尼茲。萊布尼茲在帕斯卡的發(fā)明基礎(chǔ)上，改進(jìn)設(shè)計并制造了一臺用機械裝置驅(qū)動的計算機械：

(萊布尼茲設(shè)計制造的機械計算裝置的復(fù)制品)

萊布尼茲還進(jìn)一步設(shè)想，如果將來有一個機器不但能做數(shù)學(xué)運算，還能做邏輯推理就太棒了。只要直接“告訴”機器你的數(shù)學(xué)命題，機器能告訴你這個命題正確與否。而且，萊布尼茲還意識到，要達(dá)到這一目標(biāo)，首要的一步的就是需要有一種機器可以讀取的“Formal Language”，現(xiàn)在被翻譯成“形式化語言”。

我想聽眾中可能也有不少人有過這種設(shè)想：數(shù)學(xué)證明的過程，如果全部用符號表示出來，似乎就是一種符號游戲了，甚至于都不需要理解符號所表示的實際意義。如果能把數(shù)學(xué)命題的證明，變成一種有規(guī)律可循的符號游戲，那可以讓計算機去全權(quán)處理，數(shù)學(xué)家也就都下崗了。

但目前離這一目標(biāo)還相差很遠(yuǎn)，現(xiàn)在能做的最好的也就是讓機器去檢查一個“證明”。我之前介紹“開普勒猜想”的文章中提到過，黑爾斯為了證明他的證明完全正確，不惜再用11年時間，用群體協(xié)作的方法，把他原來的證明用形式化語言重寫了一次，然后交給機器證明檢查軟件，最終確認(rèn)了他的證明正確。

let BARV3_SET_OF_LIST4 = prove_by_refinement( `!V ul. packing V /\ barV V 3 ul ==> set_of_list ul = {EL 0 ul,EL 1 ul, EL 2 ul, EL 3 ul}`, (* {{{ proof *) [ REPEAT WEAKER_STRIP_TAC; INTRO_TAC Bump.set_of_list4 [`ul`]; ANTS_TAC; REWRITE_TAC[arith `4 = 3 + 1`] THEN MATCH_MP_TAC Marchal_cells_3.BARV_LENGTH_LEMMA; BY(ASM_MESON_TAC[]); BY(MESON_TAC[]) ]);; (* }}} *)

(形式化證明代碼的例子，摘自 https://github.com/flyspeck/ ，黑爾斯關(guān)于開普勒猜想的證明代碼庫)

說句題外話，關(guān)于現(xiàn)在鬧得沸沸揚揚的日本東京大學(xué)望月新一教授所發(fā)表的，多數(shù)人看不懂的“abc猜想”的證明。如果有人能把望月教授的證明改寫為形式化證明，交給機器檢查，那么所有爭議就都解決了。只是這個工作量，大概要以幾十年起步，所以不知道有沒有人肯這么去做。當(dāng)然要去做，也只有懂望月那套理論的人去做了。這是題外話。

(京都大學(xué)的望月新一教授，2012發(fā)布了天書般的有關(guān)“abc猜想”的證明。關(guān)于他的證明是否成立，目前仍是數(shù)學(xué)界的一大爭議。)

總之，萊布尼茲提出了有關(guān)機器證明的初步設(shè)想，并提出需要確立一種形式化語言。到十九世紀(jì)末，二十世紀(jì)初，數(shù)學(xué)家在數(shù)學(xué)公理化的工作方面做了很多工作，主流數(shù)學(xué)家接受了以策梅洛-弗蘭克爾集合論，加選擇公理所構(gòu)成的ZFC公理系統(tǒng)，作為數(shù)學(xué)的邏輯推理基礎(chǔ)。把皮亞諾算術(shù)公理作為數(shù)學(xué)研究對象的定義基礎(chǔ)。這兩套公理構(gòu)成了數(shù)學(xué)大廈的地基。

1900年，德國數(shù)學(xué)家希爾伯特發(fā)布了他著名的“二十世紀(jì)重大的23個數(shù)學(xué)問題”，從他發(fā)布的問題來看，希爾伯特對構(gòu)建完美的數(shù)學(xué)基礎(chǔ)是充滿希望的。其中第10個問題是：

對于一般的丟番圖方程，能否通過某個確定的算法，經(jīng)過有限的步驟，判定這類方程是否有整數(shù)解。

丟番圖方程就是那種未知數(shù)比方程個數(shù)多的那種方程，一般這種方程都有無窮多個解。但是我們經(jīng)常會加入只考慮整數(shù)解得情況，比如“費馬大定理”所考慮的也是一種丟番圖方程?？吹某?，希爾伯特的這個問題就是對機器證明問題的一個特例。

(維基百科上關(guān)于丟番圖方程的介紹)

雖然在第二年，羅素悖論被發(fā)現(xiàn)，但希爾伯特認(rèn)為這無傷大雅，畢竟羅素悖論里這種自指向的命題，怎么看都不像數(shù)學(xué)里正經(jīng)需要研究的命題。所以，1928年，希爾伯特還把1900年提出的第十個問題一般化了：有沒有的算法，可以在有限步驟內(nèi)，對任意的形式化的數(shù)學(xué)命題進(jìn)行真或假的判斷？

這里“形式化”的命題我再稍微舉個例子，便于大家理解。各位想必都有體會，數(shù)學(xué)里的命題都有“題設(shè)”和“結(jié)論”兩部份，因為有了某個題設(shè)，所以導(dǎo)致某個結(jié)論。而題設(shè)和結(jié)論部分又往往是由若干“存在”或“對任意”這兩個詞開始的句子。比如哥德巴赫猜想是說：

對任意大于2的偶數(shù)，存在兩個質(zhì)數(shù)，其和等于這個偶數(shù)。

可以發(fā)現(xiàn)，只要把“存在”和“對任意”這兩個詞用符號表示出來，，那么數(shù)學(xué)命題就很容易全用符號表示出來。而數(shù)學(xué)家確實發(fā)明了兩個符號去表示這兩個詞，謂詞邏輯中稱為“量化符號”。比如哥德巴赫猜想就變成：

偶數(shù)a>2, 質(zhì)數(shù)c,d，c+d=a。

這里我還是用了一些文字，比如“偶數(shù)”和“質(zhì)數(shù)”。但是偶數(shù)和質(zhì)數(shù)的定義很容易再用其他符號表達(dá)出來。你把這些符號全部輸電腦，電腦是可以處理的，雖然電腦完全不理解符號后面所表達(dá)的真實含義。

以上這種符號表達(dá)出來的命題，就是形式化的一階邏輯命題。

再插個題外話，解釋下什么是“二階邏輯”。一階邏輯中，“存在”和“對任意”這兩個量化符號后面，只能跟一個一般的陳述語句，術(shù)語稱為“斷言”。但如果允許“存在”和“對任意”后面跟另外一個一階邏輯，那么整個命題就是一個二階邏輯命題。好像是:

對任意a(對任意b...，使得對任意c，有a、b、c滿足...) , 存在d(對任何e,使得a、d、e滿足...)，使得 （其他一階邏輯語句...）

看上去就是一階邏輯的遞歸。當(dāng)然，你大概從沒有看到過這種形式的數(shù)學(xué)命題。確實，數(shù)學(xué)中的命題大概99.9%以上都可以用一階邏輯描述出來。倒是有些用一階邏輯可以描述的命題，必須用二階邏輯才能證明，就比如我之前節(jié)目介紹過的“加強的有限拉姆齊定理”。

扯了那么多背景介紹，終于可以介紹什么是圖靈機了。圖靈機是有這樣一種性質(zhì)的數(shù)學(xué)概念：所有一階邏輯命題真?zhèn)涡缘呐卸▎栴}，都可以轉(zhuǎn)化為判定一個圖靈機是否“停機”的問題。進(jìn)而圖靈又證明了不存在一個一般的判定圖靈機是否停機的算法，從而否決了希爾伯特尋找一種通用算法進(jìn)行命題真?zhèn)闻袛嗟膲粝搿?/p>

在理解圖靈機之前，要先確立一種觀念：圖靈機不是一種機器，它是完全用合法的數(shù)學(xué)語言定義出的數(shù)學(xué)概念。我們說它是一種機器，是方便我們理解，但本質(zhì) 上，它是數(shù)學(xué)中的定義。有些媒體把圖靈在二戰(zhàn)期間發(fā)明的破解德軍加密裝置，英尼格瑪機，的機器稱為“圖靈機”，這就錯的太離譜了。事實上，圖靈發(fā)表有關(guān)圖靈機的論文是在1936年，二戰(zhàn)還要3年后再發(fā)生。

(電影《模仿游戲》劇照，圖靈發(fā)明的這個機器破解了德軍的密碼，但這不是圖靈機。)

我這次介紹圖靈機，還是先從臆想中圖靈機外觀開始說起，便于各位理解。根據(jù)多數(shù)科普書中的介紹，圖靈機是這種樣子：

它有一條長長的紙帶，理論上是無限長的，紙帶上劃分了很多小方格子。你可以把這條紙帶想象成電腦硬盤存儲，每個格子就是圖靈機每次操作可以存取的單元大小。

某個格子上方有一個可以讀取格子內(nèi)信息或?qū)懭胄畔⒌难b置，稱為“讀寫頭“。讀寫頭可以在紙上移動，但是只能一格格移動。如果紙帶是硬盤的話，那這種硬盤效率是極低的，但沒關(guān)系，圖靈機的設(shè)計目標(biāo)并不是計算效率，而是對計算過程的抽象和簡化。

讀寫頭內(nèi)部本身能保存一個稱為“狀態(tài)”信息，而圖靈機就是能根據(jù)當(dāng)前紙帶位置上的信息以及內(nèi)部狀態(tài)，來決定讀寫頭在當(dāng)前紙帶的格子上做怎樣的輸出，然后讓讀寫頭向哪個方向移動，以及內(nèi)部狀態(tài)如何變化的一個裝置。

下面說說圖靈機在數(shù)學(xué)中的定義。

數(shù)學(xué)里，用了七個屬性描述圖靈機，就是這七個屬性，唯一決定了一臺圖靈機。七個屬性看上去有點多，但最主要其實是兩個屬性：

第一個屬性叫：符號（Symbol）集合，即這臺圖靈機可以在紙帶上讀取和寫入的符號種類，必須是有限的。所有的符號種類數(shù)量稱為這臺圖靈機的“符號數(shù)”，或者“顏色數(shù)”，簡稱“色數(shù)”。這里，符號具體的樣子是無所謂的，我們只關(guān)心有多少種符號。其中我們還默認(rèn)有一種稱為“空白”的符號，就是紙帶上是空的，這種“空白”也算一種符號，也計算在符號集合里。所以，一般符號集合至少有2個元素，其中一個是空白符。

第二個屬性叫：狀態(tài)（State）集合，即這臺圖靈機內(nèi)部可以處于哪種狀態(tài)，也必須是有限的。所有的狀態(tài)種類數(shù)量稱為這臺圖靈機的“狀態(tài)數(shù)”。同樣，這里，具體狀態(tài)表示什么含義是無所謂的，我們只關(guān)心有多少種狀態(tài)，最少是1種狀態(tài)都行。同樣，我們還默認(rèn)有一種稱為“停機”的狀態(tài)，就是圖靈機運算結(jié)束，機器停下來的狀態(tài)。但這種狀態(tài)一般不計算在狀態(tài)集合里。

以上就是圖靈機最主要的兩種屬性，其他五種屬性是這樣的：

第一個就是前面提到的空白符。這個空白符存在是有必要性的，它其實是可以幫我們區(qū)分紙帶上每一部分信息的邊界在哪里。記得之前我在講信息熵的時候提到，如果只有一個符號是傳遞不了信息的。就有人說一個符號也可以傳遞信息，可以用這個符號的數(shù)量來表示不同信息。但此時你會發(fā)現(xiàn)，必須用空白符。否則你給我發(fā)了100個“A”，我怎么知道這些“A”該怎么斷開？所以空白符是一個必要符號。

第二個屬性是初始輸入，即圖靈機運行前，紙帶上的符號狀態(tài)。

第三個屬性是初始狀態(tài)，即圖靈機運行前，內(nèi)部所處于的某個狀態(tài)。任何時刻，圖靈機只能處于一個狀態(tài)。

第四個屬性是：“接受狀態(tài)”，或者叫“終止?fàn)顟B(tài)”。也即是圖靈機進(jìn)入這種狀態(tài)后停機。很多情況下，這個接受狀態(tài)只有一種，就是之前提到過的停機狀態(tài)。

第五個屬性是：轉(zhuǎn)移函數(shù)集合。轉(zhuǎn)移函數(shù)很像是計算機的程序，它決定了圖靈機的變化過程。圖靈機在任何時刻，它所處于的情形是由兩個屬性確定的：當(dāng)前讀取頭下小方格內(nèi)的符號和內(nèi)部狀態(tài)。轉(zhuǎn)移函數(shù)因為是函數(shù)，它有輸入?yún)?shù)和輸出參數(shù)。它的輸入?yún)?shù)就取這兩個屬性的值，它的輸出參數(shù)有三個：

• 對當(dāng)前格子輸出什么符號；

• 內(nèi)部狀態(tài)變?yōu)槭裁矗?/p>

• 以及讀取頭向左還是向右移動，或者不動。

所有轉(zhuǎn)移函數(shù)的集合就決定了一個圖靈機從啟動到停機的過程，如果它會停機的話。當(dāng)然，有些圖靈機是不會停機的，比如它進(jìn)入某幾個狀態(tài)的循環(huán)或者讀取頭永遠(yuǎn)向右移動等等。

以上就是圖靈機全部7個屬性，我知道你聽的有點暈，但我發(fā)現(xiàn)算盤其實是可以模擬成一個圖靈機的。算盤的每一檔可以看做圖靈機的紙帶上的一個格子。橫檔上的兩個算珠可以表示0-3三種符號，可以認(rèn)為0表示空白符。而橫檔下的5個算珠可以表示0-5，6種狀態(tài)。所以算盤可以看做一個3符號，6狀態(tài)的圖靈機。

如果你在紙上寫好所有符號和狀態(tài)組合下，也就是3*6=18條轉(zhuǎn)移函數(shù)，那么你就完成了一臺圖靈機的定義，可以在算盤上模擬圖靈機的運算。

一個2色-4狀態(tài)圖靈機的狀態(tài)，顏色，和讀寫頭移動方向的圖標(biāo)表示，其中狀態(tài)0表示停機狀態(tài)。（轉(zhuǎn)自mathworld）

使用上述圖標(biāo)表示的，一個2色-4狀態(tài)圖靈機的完整運算過程。上面6個方格內(nèi)是運算規(guī)則（轉(zhuǎn)自mathworld）。因為圖中沒有哪條規(guī)則將機器轉(zhuǎn)為0號狀態(tài)，所以這臺圖靈機永不停機。

現(xiàn)在用算盤演示上述圖靈機的運算過程。用算盤橫檔上方的算珠表示顏色，下方算珠表示狀態(tài)。算盤橫檔上方一共有2顆算珠，最多可以表示3種顏色；下方算珠有5顆算珠，最多可以表示6中狀態(tài)。

本例中，因為只要演示2色-4狀態(tài)的圖靈機，因此只需要使用上方的1顆算珠。算珠在上表示色號0，在下表示色號1。同理，使用下方3顆算珠表示0-4號狀態(tài)。

開始時：

起始狀態(tài)：讀寫頭位于左數(shù)第5擋（用黃點表示），當(dāng)前紙帶上是0號色，機器處于1狀態(tài)。根據(jù)前圖規(guī)則（上方6小格中的第2格），圖靈機應(yīng)在當(dāng)前位置輸出1號色，變?yōu)?號狀態(tài)，向左移動一格。

第二步：讀寫頭位于左數(shù)第4擋，當(dāng)前紙帶上是0號色，機器處于3號狀態(tài)（任何時刻，只有當(dāng)前讀寫頭位置的狀態(tài)值有效）。根據(jù)前圖規(guī)則（上方6小格中的第6格），圖靈機應(yīng)在當(dāng)前位置輸出1號色，變?yōu)?號狀態(tài)，向右移動一格。

（第三步：讀寫頭位于左數(shù)第5擋，當(dāng)前紙帶上是1號色，機器處于2號狀態(tài)。根據(jù)前圖規(guī)則（上方6小格中的第3格），圖靈機應(yīng)在當(dāng)前位置輸出1號色，變?yōu)?號狀態(tài)，向右移動一格。）

（第四步：讀寫頭位于左數(shù)第6擋，當(dāng)前紙帶上是0號色，機器處于3號狀態(tài)。根據(jù)前圖規(guī)則（上方6小格中的第6格），圖靈機應(yīng)在當(dāng)前位置輸出1號色，變?yōu)?號狀態(tài)，向右移動一格。）

之后的推演留給讀者，這臺圖靈機永不停機......

你能看的出來，圖靈機的計算能力是非常簡陋的，但妙就妙在圖靈證明了，所有一階邏輯下的數(shù)學(xué)命題，都可以轉(zhuǎn)化為一個圖靈機，而這個命題的真與假，取決于這個圖靈機能否進(jìn)入停機狀態(tài)。如果停機了，我們就能從這個圖靈機的輸出中得知這個命題是真還是假。

其實之前在哥德爾不完備定理的節(jié)目中提到過，哥德爾其實是證明了“萬物皆數(shù)字”，所有數(shù)學(xué)命題都對應(yīng)一個數(shù)字，而圖靈有點像證明了“萬物皆圖靈機”。

證明了“萬物皆圖靈機”之后就好辦了，希爾伯特的“可判定性問題”就變?yōu)椋?是否存在一個算法，在有限步驟內(nèi)，去判斷任何一個圖靈機在給定輸入的情況下，運行后是否能停機。圖靈證明了，這樣的算法是不存在的。證明方法是大家熟悉的羅素悖論模式：

假設(shè)有這種通用判別算法，叫它算法P。那么定義一種這樣的圖靈機，稱為U，這個圖靈機接受另一個圖靈機T和某個輸入作為它自身的輸入。U的運行模式是：

調(diào)用P，把U接收到的圖靈機T和輸入傳遞給P。如果P判斷T不會停機，則U停機。如果P判斷T能停機，則U進(jìn)入死循環(huán)。

現(xiàn)在問題來了， 既然U也是一臺圖靈機，則把U本身傳遞給U作為參數(shù)會如何？你自己稍微推想下，就會發(fā)現(xiàn)這里面的矛盾，U停與不停都不行，所以就不能有這樣的算法P。以上這個問題就被稱為“圖靈機停機問題”。

總之，圖靈用圖靈機作為工具，證明了希爾伯特所希望的通用命題真?zhèn)闻袛嗨惴ㄊ遣淮嬖诘摹５⒁庖稽c的是，雖然一般的圖靈機的停機問題是不可判定的，但不表示所有的圖靈機的停機是不可判定。

現(xiàn)在已經(jīng)證明，對四個狀態(tài)以內(nèi)的圖靈機，都是可判定的。四個狀態(tài)時的情況還不知道。從5狀態(tài)開始，猜想都是不可判定的了。再比如，如果你將一個已經(jīng)證明的數(shù)學(xué)命題正確編碼成圖靈機，則不管這個圖靈機有多少狀態(tài)，那么它必然可以停機。

總結(jié)一下要點：

圖靈機有兩個主要參數(shù)，符號和狀態(tài)。

判斷數(shù)學(xué)命題的真?zhèn)螁栴}可以轉(zhuǎn)化成判斷圖靈機是否停機問題，但是不存在一個通用算法去判斷圖靈機是否會停機。

圖靈也用圖靈機證明了希爾伯特的“可判定問題中”提出那種算法是不存在的。

今天內(nèi)容那么多，其實都是為了下一期節(jié)目的準(zhǔn)備知識，下一期才是重頭戲，敬請期待。

https://mathworld.wolfram.com/HaltingProblem.html

https://mathworld.wolfram.com/HaltingProblem.html

https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf

https://en.wikipedia.org/wiki/Turing_machine

https://en.wikipedia.org/wiki/Entscheidungsproblem

http://www.alcula.com/suanpan.php

https://mathworld.wolfram.com/TuringMachine.html