數學、程式和機器

(從數理邏輯、λ-Calculus、圖靈機到現代電腦的那段歷史)

陳鍾誠

2022年4月20日

Transcript

1. 數學、程式和機器 ( 從數理邏輯、 λ-Calculus 、圖靈機到現代電腦的那段歷史 ) 陳鍾誠 2022 年 4 月 20 日 程式人 程式人 本文衍生自維基百科
2. 第一個故事 數學
3. 故事的起源 • 得從數學家希爾伯特 (David Hilbert) 開始說起
4. 希爾伯特
5. 1900 年 • 希爾伯特在一場德文演講中提出了 20 世 紀希望能解決的 23 個數學問題
6. 這 23 個問題 • 影響非常深遠！
7. 目前，有些問題已經解決
8. 有些問題還在研究中
9. 希爾伯特提出這些問題之後 • 開啟了一個數學的《大航海時代》 • 吸引來很多數學家，試圖解決這些問題
10. 像是 • 羅素、哥德爾、 Church 、圖靈 ...
11. 於是 • 羅素先登場了！
12. 羅素
13. 1900 年 • 羅素正致力於撰寫一本 把數學系統公理化的書籍！
14. 那本書稱為《數學原理》
15. 數學原理 • 企圖將整個數學體系 建構成一棟穩固的大廈！
16. 於是你會看到 • 羅素在試圖證明 1+1=2
17. 問題是 • 到底要怎麼證明 1+1=2 呢？
18. 答案當然是 • 依靠一組公理系統 • 然後透過邏輯法則去推出來！
19. 其中最重要的公理系統 • 就是《一階邏輯》了！
20. 一階邏輯 • 得從符號開始學起 https://zh.wikipedia.org/wiki/%E4%B8%80%E9%98%B6%E9%80%BB%E8%BE%91
21. 然後用類似函數的語法 • 組成 predicate 與 function
22. 就像程式語言一樣
23. 只是改成邏輯的語言
24. 以及邏輯的代換法則
25. 然後透過推論法則
26. 從三條邏輯公理
27. 與四條量詞公理
28. 就能進行演譯推論 • 像是證明 not(not A)=>A
29. 或者證明 • 若 A 則 B=> 非 B 則非 A
30. 我們可以從公理系統 • 透過嚴格的邏輯法則 推導出各種數學定理！
31. 這些邏輯理論 • 並非《羅素》所發明的 • 而是承襲了《弗雷格》的一階邏輯 • 而《弗雷格》又承襲了《布林》的 布林邏輯體系
32. 但是羅素到底要如何證明 • 1+1=2 呢？
33. 這還缺了一點東西 • 那就是《皮亞諾公理系統》
34. 皮亞諾公理系統
35. 皮亞諾公理的一階邏輯描述
36. 於是 • 定義 : 1=S0 , 2=SS0 • 然後你就可以證明 – S0+S0=S(S(0+0))=SS0
37. 所以羅素在數學原理一書中 • 終於證明了 1+1=2 ...
38. 但是當羅素開始想 • 《集合論》該怎麼用邏輯表達時
39. 他發現了一個問題 • 用白話文說，就是： –一個不包含自己的集合 該怎麼定義？
40. 羅素把它寫成數學 • 結果發現，死定了！
41. 用白話文說 • A= 一個不包含自己的集合 • 於是若 A 包含自己， A 就不應該是 A 的成員，但若 A 不包含自己， A 就應該是 A 的成員
42. 這個講法有點繞口 • 所以羅素發明了另一個悖論 • 稱為理髮師悖論！
43. 理髮師悖論 • 有一個理髮師，他宣稱 – 要為所有不自己理頭髮的人理頭髮 – 但是不為任何自己理頭髮的人理頭髮 • 請問他做得到嗎？
44. 這個問題 • 當然是做不到！
45. 因為 • 他到底要不要為自己理頭髮呢？ – 如果他自己理，那就違反第二條 – 如果他不自己理，他就違反第一條
46. 理髮師悖論 • 其實有個解套方法 • 假如那個理髮師是 Snoopy 那就沒有問題了！
47. 當羅素發現這些悖論之後說 • 當我所建構的科學大廈即將完工之時， 卻發現它的地基已經動搖了 ... Hardly anything more unwelcome can befall a scientific writer than that one of the foundations of his edifice be shaken after the work is finished
48. 於是羅素的數學原理 • 就很難寫下去了 ...
49. 但是 • 這只是《集合論》上的一個小傷口 • 不代表《數論》上也會有同樣的問題 或者《一階邏輯》本身也會有悖論！
50. 終於 • 在 1929 年，傳來了好消息 • 哥德爾證明了一階邏輯不會有悖 論，史稱《哥德爾完備定理》。
51. 哥德爾完備定理 • 一階邏輯系統是一致且完備的，也就是所有的一階邏輯定理都可 以透過機械性的推論程序證明出來，而且不會導出矛盾的結論。
52. 但是隔年 • 當哥德爾嘗試把數論的皮亞諾公設放進 去時，一開始還算順利 • 不過當哥德爾把乘法符號也加進去時， 卻發現了一個悖論！
53. 為了陳述這個悖論 • 哥德爾寫下了長達 101 頁的論文 • 史稱《哥德爾不完備定理》
54. 哥德爾不完備定理
55. 在這裡 • 我們當然無法寫下該定理的證明 …
56. 但是 • 我們可以用程式人的想法寫下 哥德爾的思路邏輯！
57. 哥德爾不完備定理的程式型 • 不存在一個程式，可以正確判斷一個 – 「包含算術的一階邏輯字串」 是否為定理 ... • 要證明這件事，我們可以用反證法 ！
58. 首先假設 • 存在一個程式可以判斷某字串是否為定理
59. 然後提個問題
60. 於是我們會發現有兩種可能 • 一種是無法證明所有定理 ( 不完備 ) 另一種是會產生矛盾 ( 不一致 ) http://programmermagazine.github.io/201403/book/pmag.html
61. 所以我們得到了結論 • 不存在一個程式，可以正確判斷一個 – 「包含算術的一階邏輯字串」 是否為定理！
62. 這樣的結論 • 是在還沒有電腦，沒有程式的年代 透過純粹的數學推論證明出來的！ • 這是為何必須寫上 101 頁的原因
63. 第二個故事 程式
64. 當哥德爾證明了以下兩個定理之後 • 哥德爾完備定理 • 哥德爾不完備定理
65. 數學家 • 還是有事可以做！
66. 因為 • 那個年代還沒有電腦可以玩 也沒電視可以看 不想數學要幹嘛呢？
67. 於是有一個人 • 他叫做 Alonzo Church • 發明了一種稱為 λ Calculus 的數學！
68. λ Calculus 長這樣 • 語法 • 運算 https://en.wikipedia.org/wiki/λ_calculus
69. 放大一點 語法 運算
70. 看來很抽象 • 其實就是匿名函數的定義與呼叫 語法 運算
71. 如果用現代的語法 • 就像這樣
72. 也可以只傳部分參數進去 • 這就是函數呼叫的 curry 技巧
73. 但是 • Church 厲害的地方是 將一切都用 λ calculus 定義 • 包含 0, 1, 2, true, false, if, 等等程式語言的元素
74. 以下這篇文章 • 只要你靜下心來看，會發現 λ-Calculus 說明得很清楚 https://github.com/sgillespie/lambda-calculus/blob/master/doc/lambda-calculus.md
75. 讓我們從頭開始 • 認識 λ Calculus 的語法和語義
76. λ Calculus 的語法 • 變數 Variable – x, y, z, a, b, c ... • 函數定義 λ abstraction – λv. body • 函數呼叫 Function Application – f x y z ( 其中 f 是函數 )
77. 變數綁定 • λ x. x –x 變數被綁定了 • λ y. f y –y 被綁定， f 沒有
78. 函數範例 • λx. x – 單位函數 f(x)=x • λx. λy. x – 傳回第一個參數 f(x,y)=x • λx. λy. y – 傳回第二個參數 f(x,y)=y
79. Curry • λ 後面只能跟著一個變數，不允許多 個參數，要模擬多參數函數，就必須要 能傳回少一個參數的函數 • 這個手法稱為 currying
80. 多參數函數 • λf. λx. λy. f x y 可以縮寫成 λf x y. f x y
81. 於是 Church Numerals 誕生了 • 用函數代表數值 0,1,2,3... – 0: λ f x. x – 1: λ f x. f x – 2: λ f x. f (f x) – 3: λ f x. f (f (f x)) 這時你的心裡一定會想：幹，這三小！
82. 然後我們可以定義 succ 函數
83. 有了以上的語法 • 我們就可以定義《運算》了
84. λ Calculus 有三種運算 • Beta reduction • Alpha conversion • Eta conversion
85. Beta Reduction • 函數套用 :(λ x. body) y 將 body 裏的 x 用 y 取代 • 範例 – 0: (λ f x. x) – succ: (λ n f x. f (n f x)) – succ(0) = succ (λ f x. x) → λ f x. f ((λ f x. x) f x) → λ f x. f x → 1
86. Alpha Conversion • 當變數名稱相衝時，需要改名
87. Eta Conversion • 當某參數綁定卻沒影響時，可簡化
88. 有了以上這些 • 我們就可以寫 λ Calculus 程式了
89. 怎麼寫？
90. 像是這樣
91. 然後你就可以運算
92. 運算 ...
93. 再運算 ...
94. 終於得到 add 2 3 = 2+3 = 5
95. 其實 • 你可以用 JavaScript 做到 λ-Calculus 所做的事
96. Guilherme J. Tramontina 就這樣做了
97. 你可以用 node.js 執行
98. 不過 • Church 是數學家，當然不會只做到這樣
99. Church 在 1936 年證明了 • λ-Calculus 裏有些 《不可解的問題》 (Unsolvable Problem)
100. Church 的論文
101. 這是論文的主定理 • 要寫一個函數判斷某運算式有沒有正規形式是不可能的
102. 第三個故事 機器
103. 就在 Church 證明發表的那年 • 也就是 1936 年，圖靈 (Alan Turing) 證明 了一個定理 • 那就是《停機問題》 (Halting Problem) 是不可解的！
104. 圖靈 (Alan Turing)
105. 不過圖靈的證明 • 是建構在圖靈機之上的
106. 圖靈機 • 是一台可讀寫磁帶的機器
107. 但圖靈用數學描述它 https://zh.wikipedia.org/wiki/%E5%9B%BE%E7%81%B5%E6%9C%BA
108. 因為當時 • 根本就沒有電腦 • 圖靈只能用數學描述他的機器
109. 然後用數學證明 • 停機問題是不可解的
110. 這是圖靈的論文 https://www.cs.virginia.edu/~robins/Turing_Paper_1936.pdf
111. 後來二次大戰爆發 • 圖靈參與了《破解德軍密碼》的計畫
112. 德軍所使用的 Enigma 密碼機 https://en.wikipedia.org/wiki/Enigma_machine
113. 被圖靈的 Bombe 機破解 https://en.wikipedia.org/wiki/Bombe
114. 這個故事後來被拍成電影
115. 二次大戰末期 • 電腦開始被製造出來
116. 像是 1944 年的 MARK I
117. 1946 年的通用型電腦 ENIAC
118. 這些電腦 • 雖然大部分不像圖靈機那樣以磁帶為主 而是擁有記憶體，然後資料從磁帶讀入 不過基本上都和圖靈機具有同樣的能力 只是速度會比純粹的磁帶機快很多 ...
119. 馮紐曼 • 曾經使用過 Mark I 和 ENIAC 電腦 並且參與了新電腦 EDVAC 的研發
120. 他寫了一份 101 頁的報告
121. 該報告 • 提出了預儲程序的觀念 將程式與資料放在同一塊記憶體內 這種架構後來被稱為《馮紐曼架構》
122. 馮紐曼架構 https://en.wikipedia.org/wiki/Von_Neumann_architecture 資料和程式都 放在裡面
123. 這樣的結構 • 是後來電腦的主流結構
124. 在戰爭結束後 • 圖靈因為同性戀問題而被判化學閹割 後來咬了一口含氰化物的蘋果而死亡 https://en.wikipedia.org/wiki/Alan_Turing
125. 但是他對計算機的夢想 • 卻持續的不斷發展 ...
126. 計算機 • 變得愈來愈快，愈來愈強大 ...
127. 同時 • Church 對程式的夢想也繼續發展著
128. 1958 年 • John McCarthy 發明了 LISP 程式語言 https://zh.wikipedia.org/wiki/LISP
129. LISP • 比 λ Calculus 親切得多 是非常簡潔有力的程式語言
130. 如果你用 C 語言 • 實作 LISP 解譯器，只要幾百行
131. 像是 minilisp 專案 • 就用 996 行 C 語言實現了一個具體而微的 Lisp 解譯器 https://github.com/rui314/minilisp
132. 雖然目前 LISP 的使用者不算很多 • 但卻一直有非常死忠的熱愛者 • Common Lisp 是比較傳統的 LISP 版本 • Scheme 則是 LISP 的一種簡化方言 • Clojure 是現代化在 JVM 平台上跑的 LISP
133. λ-Calculus • 啟發了 LISP 的設計
134. 而 LISP • 又啟發了 Dylan/Julia/Haskell/ OCaml/Erlang/F#/Scala 等語言的設計 • 這類語言通常沒有迴圈，必須使用遞迴 的方式設計 • 被統稱為《函數式程式語言》 ...
135. 後來在 1970 年 • Dennis Ritchie 和 Ken Thompson 合作 發展出影響深遠的 C 語言和 UNIX 作業系統 • 讓 C 語言在數十年內成為工業影響力最強 的語言
136. 但是 • λ-Calculus 的理論 與 LISP 的簡潔優美 都對電腦與程式領域有深厚的影響
137. 雖然 • 當初希爾伯特想把數學機械化的夢想，被 – 哥德爾不完備定理 – Church 的不可解問題證明 – 圖靈的停止問題證明 所否決了！
138. 但是 • 這些理論的探索，仍然對資訊科學的發 展，有著重要的貢獻與長遠的影響 • 也導致了《函數式程式語言》的發明
139. 形成了一條 • 從數理邏輯到 λ-Calculus 再經圖靈機到現代電腦 的發展路徑 ...
140. 而這些知識 • 形成了計算理論的主要架構 串起了從數學經程式到機器的美妙世界
141. 這就是我們今天的 • 十分鐘系列
142. 希望你會喜歡
143. 我們下次見！ Good Bye !