跳轉到

1.3 λ演算、遞迴函數與Church-Turing論題#

前言：為什麼需要多種計算模型？#

圖靈機是從「機械動作」的角度刻劃計算，直觀且貼近實際計算設備。然而在 1936 年前後，另一條路線也在同步發展：從函數與遞迴（recursion）的數學性質來定義「可計算函數」。

阿隆佐·丘奇（Alonzo Church）提出了λ演算（λ-calculus），旨在建立一套純粹的函數形式系統，用以研究函數應用與抽象的邏輯基礎。與此同時，哥德爾（Kurt Gödel）與克林（Stephen Kleene）系統化了一般遞迴函數（general recursive functions），將「有效計算」歸結為從初始函數出發、經由有限次原始遞迴與 \(\mu\) -遞迴所構造的函數。

三種模型的來源截然不同：

  • 圖靈機（Turing）：模擬人類計算者的紙筆操作（動作導向）
  • λ演算（Church）：研究函數定義、應用與綁定的純粹代數（函數導向）
  • 遞迴函數（Gödel–Kleene）：從算術函數的遞迴定義抽象出「機械可構造」的函數類（算術導向）

儘管出發點迥異，最終卻證明三者在計算能力上完全等價。這種跨領域的收斂，正是促成 Church–Turing 論題 的關鍵。

λ演算：一切皆函數#

基本觀念#

λ演算最根本的洞見是：函數本身也可以作為參數傳遞、也可以作為結果回傳。這種「一級函數（first-class functions）」的思維，遠遠超前於當時的數學傳統，卻成為現代程式語言（尤其是函數式語言）的靈魂。

λ演算僅有三種構造式：

  1. 變數（Variable）： \(x, y, z, \ldots\)
  2. 抽象（Abstraction）： \(\lambda x. M\) ，表示「參數為 \(x\) ，回傳 \(M\) 」的匿名函數
  3. 應用（Application）： \((M\ N)\) ，表示將函數 \(M\) 應用於引數 \(N\)

舉例來說，恆等函數寫作 \(\lambda x. x\) ；常數函數 \(\lambda x. \lambda y. x\) （忽略第二個參數，回傳第一個）；函數合成的精神也能用純 λ 項表達。

β-歸約與計算規則#

λ演算的「計算」僅僅是替換（substitution）：

\[ (\lambda x. M)\, N \to_\beta M[x := N] \]

意即：將 \(M\) 中所有自由出現的 \(x\) 替換為 \(N\) 。這個看似極簡的規則，已足夠表達邏輯、算術、遞迴等一切可計算概念。

例如，計算 \((\lambda x. x + 1)\, 2 \to_\beta 2 + 1 = 3\) 。在純 λ 演算中，我們甚至能用丘奇編碼（Church encoding）定義自然數、布林值、配對、列表等資料結構。

\(\alpha\) -轉換與自由變數#

為了避免變數名稱衝突，λ演算引入 \(\alpha\) -轉換： \(\lambda x. M \equiv_\alpha \lambda y. M[x:=y]\) （僅在 \(y\) 不自由出現於 \(M\) 時）。這種對「綁定」與「作用域」的形式化，直接影響了後來程式語言的變數範疇（lexical scope）設計。

不可判定性與正規化#

一個 λ 項是否有β-正規形（β-normal form）（無法再進行 β-歸約的形式）？這本身就是不可判定的。這與圖靈機的停機問題等價： \((M\ N)\) 停機（歸約至正規形） \(\Leftrightarrow\) 對應的圖靈機在輸入下停機。

遞迴函數：從算術到機械計算#

初始函數#

克林（Stephen Kleene）基於哥德爾的原始遞迴函數理論，定義初始函數（initial functions）：

  1. 零函數 \(Z(n)=0\)
  2. 後繼函數 \(S(n)=n+1\)
  3. 投影函數 \(P_i^k(x_1,\ldots,x_k)=x_i\)

這三類函數極為簡單，卻構成了整個自然數算術的胚胎。

組合運算#

從初始函數出發，可透過以下運算生成新的函數：

  • 複合（composition）： \(f(\vec{x}) = h(g_1(\vec{x}), \ldots, g_m(\vec{x}))\)
  • 原始遞迴（primitive recursion）：定義 \(f(0,\vec{x}) = g(\vec{x})\) ， \(f(n+1,\vec{x}) = h(f(n,\vec{x}), n, \vec{x})\)

由此得到的函數類稱為原始遞迴函數（primitive recursive functions）。加法、乘法、指數、階乘等幾乎日常用到的算術函數皆屬此類。

\(\mu\) -遞迴與一般遞迴函數#

然而，原始遞迴函數仍有其極限。考慮阿克曼函數（Ackermann function） \(A(m,n)\) ：它定義簡潔卻增長極快，且可證明不是原始遞迴的。為了涵蓋所有「有效可計算」的函數，克林引入最小化運算（ \(\mu\) -operator）：

\[ f(\vec{x}) = \mu y\,[ g(\vec{x}, y)=0 ] \]

表示「找出最小的 \(y \ge 0\) 使得 \(g(\vec{x},y)=0\) 」。若對給定 \(\vec{x}\) 不存在這樣的 \(y\) ，則 \(f(\vec{x})\) 無定義（部分函數）。

允許有限次應用初始函數、複合、原始遞迴與 \(\mu\) -運算所得到的函數，稱為一般遞迴函數（general recursive functions），又稱** \(\mu\) -遞迴函數**。

部分函數的重要性#

值得注意：圖靈機允許輸入不停止（loop），對應到部分函數。一般遞迴函數也允許 \(\mu\) -運算找不到零點而無定義。這種「部分性」正是刻劃不可判定性邊界的關鍵：全函數的可判定性與部分函數的可辨識性必須分開討論。

三大模型的等價性#

1936 年的論戰與收斂堪稱計算理論史上的奇觀。丘奇首先證明：** \(\lambda\) 可定義函數 = 一般遞迴函數。圖靈隨後證明：圖靈可計算函數 = \(\lambda\) 可定義函數**。

更具體地，可以建立雙向模擬：

  • 圖靈機 \(\mapsto\) λ項：將紙帶、狀態、轉移編碼為 λ 項，模擬機器步驟
  • λ項 \(\mapsto\) 圖靈機：用圖靈機實作 β-歸約策略（例如最左歸約）
  • 遞迴函數 \(\mapsto\) 圖靈機：用圖靈機實作遞迴呼叫與 \(\mu\) -搜尋
  • 圖靈機 \(\mapsto\) 遞迴函數：將機器配置編號為自然數，定義「下一配置」函數 \(next(c)=c'\)

這些模擬證明了：對於任何一個模型定義的「有效計算」，都能在另一個模型中重現。計算能力在邏輯上達成了完全一致。

Church–Turing 論題#

基於上述等價性，丘奇於 1936 年提出「丘奇論題」（Church's Thesis），圖靈則獨立地表達了類似看法。後人統稱為 Church–Turing 論題：

Church–Turing 論題（Church–Turing Thesis）：一個函數是有效可計算（effectively computable）的，當且僅當它是圖靈可計算的。

論題 vs 定理#

必須清楚區分兩者：

  • 定理（Theorem）：在已給定的形式定義下，可由邏輯推演證明。
  • 論題（Thesis）：關於「直覺概念」與「形式模型」之間的對應關係，無法用純形式手段證明。

「有效可計算」是一個直覺性概念：指任何人類只憑有限的規則、紙筆、時間即可完成的計算程序。圖靈機、λ演算、遞迴函數則是形式化模型。Church–Turing 論題斷言：這個直覺概念的外延，恰好就是這三個形式模型的共同外延。

論據與說服力#

支持此論題的理由主要有：

  1. 三模型等價：截然不同的起點卻殊途同歸，極不可能全都錯失「真正的有效計算」。
  2. 圖靈的分析（Turing's analysis）：圖靮機的設計直接源自對「人類計算者」認知與行為的哲學分析（有限狀態的大腦、有限符號感知、逐步書寫），最能說服非形式背景的觀察者。
  3. 經驗收斂：歷來提出的所有計算模型（Post 系統、暫存器機、RAM 機、While 程式語言等）都被證明等價於圖靈機。
  4. 工程實際：通用圖靮機預示了現代電腦的能力範圍。事實上，任何實際可執行的演算法，都能在圖靮機上模擬。

超圖靈計算（Hypercomputation）的思考#

有少數研究者探討所謂「超圖靈計算」（hypercomputation），試圖超越 Church–Turing 邊界（例如利用實數物理、黑洞、無限加速機器等）。但至今多數觀點認為：這些構想要嘛違反物理定律（因果律、能量有限等），要嘛將「預言」與「計算」混淆。Church–Turing 論題在理論計算機科學的標準框架中仍被普遍接受。

理論與實務的互相驅動#

Church–Turing 論題的統一，對後世影響極為深遠：

  • 程式語言設計：λ演算催生了 LISP（1958），其影響貫穿至 ML、Scheme、Haskell 等語言。函數抽象、閉包（closure）、柯里化（currying）等概念皆源自 λ 理論。
  • 編譯器理論：λ演算的 \(\beta\) -歸約與求值策略（call-by-value vs call-by-name）直接對應到實際編譯與直譯器的設計選擇。
  • 型別系統：簡單型別 λ 演算（Curry–Howard 對應的起點）發展出 Hindley–Milner 型別推導（ML family），影響了 TypeScript、Rust 等現代語言的型別思維。
  • 計算複雜性理論：以圖靈機為標準模型度量時間與空間，建立 P、NP、EXPTIME 等複雜度類別。變體模型（多帶圖靮機、非確定圖靮機）則用來刻劃資源約束。
  • 自動定理證明：λ演算與型別理論是 Coq、Agda 等證明輔助器的邏輯基礎（Curry–Howard 同構：命題即型別，證明即程式）。
  • 形式語義：操作語義（small-step/big-step）、指稱語義、公理語義等，無不建立在 λ 演算與遞迴函數的形式框架上。

特別值得強調：理論上的等價性並不意味工程上的等價。λ演算鼓勵「函數組合」的宣告式思維，圖靈機則揭示了「狀態轉移」的命令式本質。現代程式語言正是嘗試在這兩種思維之間取得平衡。

小結#

λ演算、遞迴函數與圖靈機從三個完全不同的角度回答了同一個問題：「什麼是有效可計算？」三者等價的事實，讓我們有充分理由相信 Church–Turing 論題的正確性。

這個統一具有劃時代意義：它不僅終結了 1930年代關於「可計算性」定義的爭論，更確立了計算邊界的普適性。從此，理論計算機科學獲得了堅實的形式地基。

下一章，我們將從計算能力的邊界轉向計算模型的分類：有限自動機如何刻劃正則語言？Kleene 定理如何建立正則表達式與自動機之間的等價？這些較為「受限」的計算模型，反而在編譯器、字串處理、網路協定等實務中最為常用。