數學家的紙上計算機——圖靈機簡介

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

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

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

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

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

我知道你聽了這個問題後還是一頭霧水，什麼叫「形式化語言」，這裡的「邏輯命題」和「算法」又是啥？那我繼續回溯一段歷史。這個問題最早可以追溯到17世紀的萊布尼茲。萊布尼茲在帕斯卡的發明基礎上，改進設計並製造了一臺用機械裝置驅動的計算機械：

(萊布尼茲設計製造的機械計算裝置的複製品)

萊布尼茲還進一步設想，如果將來有一個機器不但能做數學運算，還能做邏輯推理就太棒了。只要直接「告訴」機器你的數學命題，機器能告訴你這個命題正確與否。而且，萊布尼茲還意識到，要達到這一目標，首要的一步的就是需要有一種機器可以讀取的「Formal Language」，現在被翻譯成「形式化語言」。

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

但目前離這一目標還相差很遠，現在能做的最好的也就是讓機器去檢查一個「證明」。我之前介紹「克卜勒猜想」的文章中提到過，黑爾斯為了證明他的證明完全正確，不惜再用11年時間，用群體協作的方法，把他原來的證明用形式化語言重寫了一次，然後交給機器證明檢查軟體，最終確認了他的證明正確。

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/ ，黑爾斯關於克卜勒猜想的證明代碼庫)

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

(京都大學的望月新一教授，2012發布了天書般的有關「abc猜想」的證明。關於他的證明是否成立，目前仍是數學界的一大爭議。)

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

1900年，德國數學家希爾伯特發布了他著名的「二十世紀重大的23個數學問題」，從他發布的問題來看，希爾伯特對構建完美的數學基礎是充滿希望的。其中第10個問題是：

對於一般的丟番圖方程，能否通過某個確定的算法，經過有限的步驟，判定這類方程是否有整數解。

丟番圖方程就是那種未知數比方程個數多的那種方程，一般這種方程都有無窮多個解。但是我們經常會加入只考慮整數解得情況，比如「費馬大定理」所考慮的也是一種丟番圖方程。看得出，希爾伯特的這個問題就是對機器證明問題的一個特例。

---

(維基百科上關於丟番圖方程的介紹)

---

雖然在第二年，羅素悖論被發現，但希爾伯特認為這無傷大雅，畢竟羅素悖論裡這種自指向的命題，怎麼看都不像數學裡正經需要研究的命題。所以，1928年，希爾伯特還把1900年提出的第十個問題一般化了：有沒有的算法，可以在有限步驟內，對任意的形式化的數學命題進行真或假的判斷？

這裡「形式化」的命題我再稍微舉個例子，便於大家理解。各位想必都有體會，數學裡的命題都有「題設」和「結論」兩部分，因為有了某個題設，所以導致某個結論。而題設和結論部分又往往是由若干「存在」或「對任意」這兩個詞開始的句子。比如哥德巴赫猜想是說：

對任意大於2的偶數，存在兩個質數，其和等於這個偶數。

可以發現，只要把「存在」和「對任意」這兩個詞用符號表示出來，，那麼數學命題就很容易全用符號表示出來。而數學家確實發明了兩個符號去表示這兩個詞，謂詞邏輯中稱為「量化符號」。比如哥德巴赫猜想就變成：

偶數a>2, 質數c,d，c+d=a。

這裡我還是用了一些文字，比如「偶數」和「質數」。但是偶數和質數的定義很容易再用其他符號表達出來。你把這些符號全部輸電腦，電腦是可以處理的，雖然電腦完全不理解符號後面所表達的真實含義。

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

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

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

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

扯了那麼多背景介紹，終於可以介紹什麼是圖靈機了。圖靈機是有這樣一種性質的數學概念：所有一階邏輯命題真偽性的判定問題，都可以轉化為判定一個圖靈機是否「停機」的問題。進而圖靈又證明了不存在一個一般的判定圖靈機是否停機的算法，從而否決了希爾伯特尋找一種通用算法進行命題真偽判斷的夢想。

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

---

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

---

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

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

某個格子上方有一個可以讀取格子內信息或寫入信息的裝置，稱為「讀寫頭「。讀寫頭可以在紙上移動，但是只能一格格移動。如果紙帶是硬碟的話，那這種硬碟效率是極低的，但沒關係，圖靈機的設計目標並不是計算效率，而是對計算過程的抽象和簡化。

讀寫頭內部本身能保存一個稱為「狀態」信息，而圖靈機就是能根據當前紙帶位置上的信息以及內部狀態，來決定讀寫頭在當前紙帶的格子上做怎樣的輸出，然後讓讀寫頭向哪個方向移動，以及內部狀態如何變化的一個裝置。

下面說說圖靈機在數學中的定義。

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

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

第二個屬性叫：狀態（State）集合，即這臺圖靈機內部可以處於哪種狀態，也必須是有限的。所有的狀態種類數量稱為這臺圖靈機的「狀態數」。同樣，這裡，具體狀態表示什麼含義是無所謂的，我們只關心有多少種狀態，最少是1種狀態都行。同樣，我們還默認有一種稱為「停機」的狀態，就是圖靈機運算結束，機器停下來的狀態。但這種狀態一般不計算在狀態集合裡。

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

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

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

第三個屬性是初始狀態，即圖靈機運行前，內部所處於的某個狀態。任何時刻，圖靈機只能處於一個狀態。

第四個屬性是：「接受狀態」，或者叫「終止狀態」。也即是圖靈機進入這種狀態後停機。很多情況下，這個接受狀態只有一種，就是之前提到過的停機狀態。

第五個屬性是：轉移函數集合。轉移函數很像是計算機的程序，它決定了圖靈機的變化過程。圖靈機在任何時刻，它所處於的情形是由兩個屬性確定的：當前讀取頭下小方格內的符號和內部狀態。轉移函數因為是函數，它有輸入參數和輸出參數。它的輸入參數就取這兩個屬性的值，它的輸出參數有三個：

• 對當前格子輸出什麼符號；
• 內部狀態變為什麼；
• 以及讀取頭向左還是向右移動，或者不動。

所有轉移函數的集合就決定了一個圖靈機從啟動到停機的過程，如果它會停機的話。當然，有些圖靈機是不會停機的，比如它進入某幾個狀態的循環或者讀取頭永遠向右移動等等。

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

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

---

一個2色-4狀態圖靈機的狀態，顏色，和讀寫頭移動方向的圖標表示，其中狀態0表示停機狀態。（轉自mathworld）

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

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

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

開始時：

起始狀態：讀寫頭位於左數第5擋（用黃點表示），當前紙帶上是0號色，機器處於1狀態。根據前圖規則（上方6小格中的第2格），圖靈機應在當前位置輸出1號色，變為3號狀態，向左移動一格。

第二步：讀寫頭位於左數第4擋，當前紙帶上是0號色，機器處於3號狀態（任何時刻，只有當前讀寫頭位置的狀態值有效）。根據前圖規則（上方6小格中的第6格），圖靈機應在當前位置輸出1號色，變為2號狀態，向右移動一格。

（第三步：讀寫頭位於左數第5擋，當前紙帶上是1號色，機器處於2號狀態。根據前圖規則（上方6小格中的第3格），圖靈機應在當前位置輸出1號色，變為3號狀態，向右移動一格。）

（第四步：讀寫頭位於左數第6擋，當前紙帶上是0號色，機器處於3號狀態。根據前圖規則（上方6小格中的第6格），圖靈機應在當前位置輸出1號色，變為2號狀態，向右移動一格。）

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

---

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

其實之前在哥德爾不完備定理的節目中提到過，哥德爾其實是證明了「萬物皆數字」，所有數學命題都對應一個數字，而圖靈有點像證明了「萬物皆圖靈機」。

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

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

調用P，把U接收到的圖靈機T和輸入傳遞給P。如果P判斷T不會停機，則U停機。如果P判斷T能停機，則U進入死循環。

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

總之，圖靈用圖靈機作為工具，證明了希爾伯特所希望的通用命題真偽判斷算法是不存在的。但要注意一點的是，雖然一般的圖靈機的停機問題是不可判定的，但不表示所有的圖靈機的停機是不可判定。

現在已經證明，對四個狀態以內的圖靈機，都是可判定的。四個狀態時的情況還不知道。從5狀態開始，猜想都是不可判定的了。再比如，如果你將一個已經證明的數學命題正確編碼成圖靈機，則不管這個圖靈機有多少狀態，那麼它必然可以停機。

總結一下要點：

圖靈機有兩個主要參數，符號和狀態。

判斷數學命題的真偽問題可以轉化成判斷圖靈機是否停機問題，但是不存在一個通用算法去判斷圖靈機是否會停機。

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

今天內容那麼多，其實都是為了下一期節目的準備知識，下一期才是重頭戲，敬請期待。

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