无类型lambda演算

**λ 演算**（英語：lambda calculus，λ-calculus）是一套從數學邏輯中發展，以變數綁定和替換的規則，來研究函式如何抽象化定義、函式如何被應用以及遞迴的形式系統。它由數學家阿隆佐・邱奇在 20 世紀 30 年代首次發表。lambda 演算作為一種廣泛用途的計算模型，可以清晰地定義什麼是一個可計算函式，而任何可計算函式都能以這種形式表達和求值，它能類比單一磁帶圖靈機的計算過程；儘管如此，lambda 演算強調的是變換規則的運用，而非實現它們的具體機器。

lambda 演算可比擬是最根本的程式語言，它包括了一條變換規則（變數替換）和一條將函式抽象化定義的方式。因此普遍公認是一種更接近軟體而非硬體的方式。對函數式程式語言造成很大影響，比如 Lisp、ML 語言和 Haskell 語言。在 1936 年邱奇利用 λ 演算給出了對於判定性問題（Entscheidungsproblem）的否定：關於兩個 lambda 運算式是否等價的命題，無法由一個「通用的演算法」判斷，這是不可判定效能夠證明的頭一個問題，甚至還在停機問題之先。

lambda 演算包括了建構 lambda 項，和對 lambda 項執行歸約的操作。在最簡單的 lambda 演算中，只使用以下的規則來建構 lambda 項：

產生了諸如：(λx.λy.(λz.(λx.zx)(λy.zy))(x y)) 的表達式。如果表達式是明確而沒有歧義的，則括號可以省略。對於某些應用，其中可能包括了邏輯和數學的常數以及相關操作。

本文討論的是邱奇的「無類型 lambda 演算」，此後，已經研究出來了一些有類型 lambda 演算。

## 解釋與應用

λ 演算是圖靈完備的，也就是說，這是一個可以用於類比任何圖靈機的通用模型。 λ 也被用在 **λ 表達式**和 **λ 項**中，用來表示將一個變數繫結在一個函式上。

λ 演算可以是**有類型**或者**無類型**的，在有類型 λ 演算中（上文所述是無類型的），函式只能在參數類型和輸入類型符合時被應用。有類型 λ 演算比無類型 λ 演算要弱 —— 後者是這個條目的主要部分 —— 因為有類型的 λ 運算能表達的比無類型 λ 演算少；與此同時，前者使得更多定理能被證明。例如，在簡單類型 λ 演算中，運算總是能夠停止，然而無類型 λ 演算中這是不一定的（因為停機問題）。目前有許多種有類型 λ 演算的一個原因是它們被期望能做到更多（做到某些以前的有類型 λ 演算做不到的）的同時又希望能用以證明更多定理。

λ 演算在數學、哲學、語言學和電腦科學中都有許多應用。它在程式語言理論中占有重要地位，函式語言程式設計實現了 λ 演算支援。λ 演算在範疇論中也是一個研究熱點。

## 歷史

作為對數學基礎研究的一部分，數學家阿隆佐・邱奇在 20 世紀 30 年代提出了 λ 演算。 但最初的 λ 演算系統被證明是邏輯上不自洽的 —— 在 1935 年史蒂芬・科爾・克萊尼和 J. B. Rosser 舉出了 Kleene-Rosser 悖論。

隨後，在 1936 年邱奇把那個版本的關於計算的部分抽出獨立發表 — 現在這被稱為無類型 λ 演算。 在 1940 年，他創立了一個計算能力更弱但是邏輯上自洽的系統，這被稱為簡單類型 λ 演算。

直到 1960 年，λ 演算與程式語言的關係被確立了；在這之前它只是一個範式。由於理察・蒙塔古和其他語言學家將 λ 演算應用於自然語言語法的研究，λ 演算已經開始在語言學和電腦科學學界擁有一席之地。

至於為何邱奇選擇 λ 作為符號，連他本人的解釋也互相矛盾：最初是在 1964 年的一封信中，他明確解釋稱這是來源於《數學原理》一書中的類抽象符號（脫字元），為了方便閱讀，他首先將其換成邏輯與符號（ $\land $ ）作為區分，然後又改成形狀類似的 λ。他在 1984 年又重申了這一點，但再後來他又表示選擇 λ 純粹是偶然。

## 非形式化的直覺描述

在 λ 演算中，每個表達式都代表一個函式，這個函式有一個參數，並且會返回一個值。不論是參數和返回值，也都是一個單參的函式。可以這麼說，λ 演算中只有一種「類型」，那就是這種一元函式。函式是通過 λ 表達式匿名地定義的，這個表達式說明了此函式將對其參數進行什麼操作。

例如，「加 2」函式 f (x)= x + 2 可以用 lambda 演算表示為 λx.x + 2（或者 λy.y + 2，參數的取名無關緊要），而 f (3) 的值可以寫作 (λx.x + 2) 3。函式的應用（application）是左結合的：f x y =(f x) y。

考慮這麼一個函式：它把一個函式作為參數，這個函式將被作用在 3 上：λf.f 3。如果把這個（用函式作參數的）函式作用於我們先前的「加 2」函式上：(λf.f 3)(λx.x+2)，則明顯地，下述三個表達式：

　
: (λf.f 3)(λx.x+2) 與 (λx.x + 2) 3 與 3 + 2

是等價的。有兩個參數的函式可以通過 lambda 演算這樣表達：一個單一參數的函式，它的返回值又是一個單一參數的函式（參見柯里化）。例如，函式 f (x, y) = x - y 可以寫作 λx.λy.x - y。下述三個表達式：

　
: (λx.λy.x - y) 7 2 與 (λy.7 - y) 2 與 7 - 2

也是等價的。然而這種 lambda 表達式之間的等價性，無法找到某個通用的函式來判定。

並非所有的 lambda 表達式都能被歸約至上述那樣的確定值，考慮

　
: (λx.x x)(λx.x x)

或

　
: (λx.x x x)(λx.x x x)

然後試圖把第一個函式作用在它的參數上。(λx.x x) 被稱為 ω 組合子，((λx.x x)(λx.x x)) 被稱為 Ω，而 ((λx.x x x) (λx.x x x)) 被稱為 Ω2，以此類推。若僅形式化函式作用的概念而不允許 lambda 表達式，就得到了組合子邏輯。

### 動機

在數學和計算機科學中，「可計算的」函式是基礎觀念。對於所謂的可計算性，λ- 演算提供了一個簡單明確的語義，使計算的性質可以被形式化研究。λ- 演算結合了兩種簡化方式，使得這個語義變得簡單。第一種簡化是不給予函式一個確定名稱，而「匿名」地對待它們。例如，兩數的平方和函式

　
: $\operatorname {square\_sum} (x,y)=x^{2}+y^{2}$

可以用匿名的形式重新寫為：

　
: $(x,y)\mapsto x^{2}+y^{2}$ （理解成一包含 x 和 y 的數組被對映到 $x^{2}+y^{2}$ ）

同樣地，

　
: $\operatorname {id} (x)=x$

可以用匿名的形式重新寫為：

　
: $x\mapsto x$ （即輸入是直接對應到它本身。）

第二個簡化是 λ 演算只使用單一個參數輸入的函式。如果普通函式需要兩個參數，例如 $\operatorname {square\_sum} $ 函式，可轉成接受單一參數，傳給另一個函式中介，而中介函式也只接受一個參數，最後輸出結果。例如，

　
: $(x,y)\mapsto x^{2}+y^{2}$

可以重新寫成：

　
: $x\mapsto (y\mapsto x^{2}+y^{2})$

這是稱為柯里化的方法，將多參數的函式轉換成為多個中介函式的複合鏈，每個中介函式都只接受一個參數。
將 $\operatorname {square\_sum} $ 函式應用於參數 (5,2)，直接產生結果

　
: $((x,y)\mapsto x^{2}+y^{2})(5,2)$

　
: $=5^{2}+2^{2}$

　
: $=29$ ,

而對於柯里化轉換版的評估，需要再多一步：

　
: ${\Bigl (}{\bigl (}x\mapsto (y\mapsto x^{2}+y^{2}){\bigr )}(5){\Bigr )}(2)$

　
: $=(y\mapsto 5^{2}+y^{2})(2)$ // 在內層表達式中 $x$ 的定義為 $5$ ，這就像 β- 歸約一樣。

　
: $=5^{2}+2^{2}$ // $y$ 的定義為 $2$ ，再次如同 β- 歸約。

　
: $=29$

得出相同結果。

### lambda 演算

lambda 演算是由特定形式語法所組成的一種語言，一組轉換規則可操作其中的 lambda 項。這些轉換規則被看作是一個等式理論或者一個操作定義。如上節所述，lambda 演算中的所有函式都是匿名的，它們沒有名稱，它們只接受一個輸入變數，柯里化用於實現有多個輸入變數的函式。

#### lambda 項

lambda 演算的語法將一些表達式定義為有效的 lambda 演算式，而某一些表達式無效，就像 C 程式語言中有些字串有效，有些則不是。有效的 lambda 演算式稱為「lambda 項」。

以下三個規則給出了語法上有效的 lambda 項，如何建構的歸納定義：

* 變數 $x$ 本身就是一個有效的 lambda 項
* 如果 $t$ 是一個 lambda 項，而 $x$ 是一個變數，則 $(\lambda x.t)$ 是一個 lambda 項（稱為 **lambda 抽象**）；
* 如果 $t$ 和 $s$ 是 lambda 項，那麼 $(ts)$ 是一個 lambda 項（稱為**應用**）。

其它的都不是 lambda 項。因此，lambda 項若且唯若可重複應用這三個規則取得時，才是有效的。一些括號根據某些規則可以省略。例如，最外面的括號通常不會寫入。

「lambda 抽象」是指一個匿名函式的定義，它將單一輸入的 $\lambda x.t$ 替換成 $t$ 的表達式，所以產生了一個匿名函式，它採用 $x$ 的值並返回 $t$ 。例如， $\lambda x.x^{2}+2$ 是表示使用函式 $f(x)=x^{2}+2$ 作為 $t$ 項的一個 lambda 抽象。lambda 抽象只是先「設定」了函式定義，還沒使用它。這個抽象在 $t$ 項中綁定了變數 $x$ 。一個**應用** $ts$ 表示將函式 $t$ 應用在輸入 $s$ ，亦即對輸入 $s$ 使用函式 $t$ 產生 $t(s)$ 。

lambda 演算中並沒有變數聲明的概念。如 $\lambda x.x+y$ （即 $f(x)=x+y$ ）的定義中，lambda 演算將 $y$ 當作尚未定義的變數。lambda 抽象 $\lambda x.x+y$ 在語法上是有效的，並表示將其輸入添加到未知 $y$ 的函式。

可用圓括弧對來消除歧義。例如， $\lambda x.((\lambda x.x)x)$ 和 $(\lambda x.(\lambda x.x))x$ 表示不同的項（儘管它們剛好化簡到相同值）。這裡第一個例子定義了一個包含子函式的抽象，並將子函式應用於 x（先應用後傳回）的結果；而第二個例子定義了一個傳回任何輸入的函式，然後在應用過程中傳回對輸入為 x 的應用（返回函式然後應用）。

#### 操作函式的函式

在 lambda 演算中，函式被認為是**頭等物件**，因此函式可以當作輸入，或作為其它函式的輸出返回。

例如， $\lambda x.x$ 表示對映到本身的函式， $x\mapsto x$ 和 $(\lambda x.x)y$ 表示將這個函式應用於 $y$ 。此外， $(\lambda x.y)$ 則表示無論輸入為何，始終返回 $y$ 值的**常數函式** $x\mapsto y$ 。lambda 演算中的函式應用是左結合的，因此 $stx$ 表示 $(st)x$ 。

有幾個「等價」和「化簡」的概念，允許將各個 lambda 項「縮減」為「相同」的 lambda 項。

####  $\alpha $ - 等價

對於 lambda 項，等價的基本形式定義，是 $\alpha $ - 等價。它捕捉了直覺概念，在 lambda 抽象中一個綁定變數的特別選擇（通常）並不重要。
比如， $\lambda x.x$ 和 $\lambda y.y$ 是 $\alpha $ - 等價的 lambda 項，它們都表示相同的函式（自對映函式）；但如 $x$ 和 $y$ 項則不是 $\alpha $ - 等價的，因為它們並非以 lambda 抽象方式綁定的。
在許多演示中，通常會確定 $\alpha $ - 等價的 lambda 項。

為了能夠定義 $\beta $ - 歸約，需要以下定義：

#### 自由變數

所謂的**自由變數**是那些在 lambda 抽象不受到綁定的變數。表達式中的一組自由變數定義歸納如下：

 * $x$ 的自由變數就只是 $x$
* $\lambda x.t$ 的自由變數集合，是在 $t$ 中移除了 $x$ 的自由變數集合。
* $ts$ 的自由變數是 $t$ 的一組自由變數，與 $s$ 的一組自由變數，這兩項變數的並集。

例如，代表對映自身的 $\lambda x.x$ ，其中的 lambda 項沒有自由變數，但是在函式 $\lambda x.yx$ 中的 lambda 項，有一個自由變數 $y$ 。

#### 避免捕獲的替換記法

假設 $t$ ， $s$ 和 $r$ 是 lambda 項，而 $x$ 和 $y$ 是變數。如果寫成 $t[x:=r]$ 是一種_避免被捕獲_的記法方式，表示在 $t$ 這個 lambda 項中，以 $r$ 來替換 $x$ 變數的值。這定義為：

 * $x[x:=r]=r$ ；
* $y[x:=r]=y$ ，如果 $x\neq y$ ；
* $(ts)[x:=r]=(t[x:=r])(s[x:=r])$ ；
* $(\lambda x.t)[x:=r]=\lambda x.t$ ；
* 如果 $x\neq y$ 而且 $y$ 不在 lambda 項 $r$ 的自由變數中，則 $(\lambda y.t)[x:=r]=\lambda y.(t[x:=r])$ 。對於 lambda 項 $r$ ，變數 $y$ 被稱為是「新鮮」的。

例如， $(\lambda x.x)[y:=y]=\lambda x.(x[y:=y])=\lambda x.x$ 和 $((\lambda x.y)x)[x:=y]=((\lambda x.y)[x:=y])(x[x:=y])=(\lambda x.y)y$ 。

新鮮度條件（要求 $y$ 不在 lambda 項 $r$ 中的自由變數中）對於確保替換不會改變函式的意義很重要。例如，忽視新鮮度條件的替代： $(\lambda x.y)[y:=x]=\lambda x.(y[y:=x])=\lambda x.x$ 。此替換會將原本意義為常數函式的 $\lambda x.y$ ，轉換成意義為對映自身函式的 $\lambda x.x$ 。

一般來說，在無法滿足新鮮度條件的情況，可利用 $\alpha $ - 重新命名使用一個合適的新變數來補救，切換回正確的替換概念；比如在 $(\lambda x.y)[y:=x]$ 中，使用一個新變數 $z$ 重新命名這個 lambda 抽象，獲取 $(\lambda z.y)[y:=x]=\lambda z.(y[y:=x])=\lambda z.x$ ，則替換就能保留原本函式的義涵。

####  $\beta $ - 歸約

β- 歸約規定了形式如 $(\lambda x.t)s$ 的應用，可以化簡成 $t[x:=s]$ 項。符號記法 $(\lambda x.t)s\to t[x:=s]$ 用於表示 $(\lambda x.t)s$ 經過 β- 歸約轉換為 $t[x:=s]$ 。例如，對於每個 $s$ ，可轉換為 $(\lambda x.x)s\to x[x:=s]=s$ 。這表明 $\lambda x.x$ 實際上的應用是對映自身函式。同樣地， $(\lambda x.y)s\to y[x:=s]=y$ ，表明了 $\lambda x.y$ 是一個常數函式。

lambda 演算可視為函數式程式語言的理想化版本，如 Haskell 或 ML 語言。在這種觀點下，β- 歸約對應於一組計算步驟。
這個步驟重複應用 β- 轉換，一直到沒有東西能再被化簡。在無型別 lambda 演算中，如本文所述，這個歸約過程可能無法終止，
比如 $\Omega =(\lambda x.xx)(\lambda x.xx)$ ，是個特殊的 lambda 項。這裡 $(\lambda x.xx)(\lambda x.xx)\to (xx)[x:=\lambda x.xx]=(x[x:=\lambda x.xx])(x[x:=\lambda x.xx])=(\lambda x.xx)(\lambda x.xx)$ 也就是說，該 lambda 項在一次 β- 歸約中化簡到本身，因此歸約過程將永遠不會終止。

無型別 lambda 演算的另一方面是它並不區分不同種類的資料。例如，需要編寫只針對數字操作的功能。然而，在無型別的 lambda 演算中，沒有辦法避免函式被應用於真值、字串或其它非數字物件。

## 形式化定義

形式化地，我們從一個識別碼（identifier）的可數無窮集合開始，比如 {a, b, c, ..., x, y, z, x1, x2, ...}，則所有的 lambda 表達式可以通過下述以 BNF 範式表達的上下文無關文法描述：

1. <表達式> ::= <識別碼>
2. <表達式> ::= (λ< 識別碼>.<表達式>)
3. <表達式> ::= (<表達式> <表達式>)

頭兩條規則用來生成函式，而第三條描述了函式是如何作用在參數上的。通常，lambda 抽象（規則 2）和函式作用（規則 3）中的括弧在不會產生歧義的情況下可以省略。如下假定保證了不會產生歧義：（1）函式的作用是左結合的，和（2）lambda 運算子被繫結到它後面的整個表達式。例如，表達式 (λx.x x)(λy.y) 可以簡寫成 λ(x.x x) λy.y 。

類似 λx.(x y) 這樣的 lambda 表達式並未定義一個函式，因為變數 y 的出現是自由的，即它並沒有被繫結到表達式中的任何一個 λ 上。一個 lambda 表達式的自由變數的集合是通過下述規則（基於 lambda 表達式的結構歸納地）定義的：

1. 在表達式 V 中，V 是變數，則這個表達式里自由變數的集合只有 V。
2. 在表達式 λV .E 中（V 是變數，E 是另一個表達式），自由變數的集合是 E 中自由變數的集合減去變數 V。因而，E 中那些 V 被稱為繫結在 λ 上。
3. 在表達式 (E E') 中，自由變數的集合是 E 和 E' 中自由變數集合的併集。

例，對於表達式 λx.x（我們將第一個 x 視作變數，第二個 x 視作表達式），其中表達式 x 中，由 1，它的自由變數集合是 x，又由 2，表達式 λx.x 的自由變數的集合是表達式 x 的自由變數集合減去變數 x。所以對於表達式 λx.x，它的自由變數集合是空。 
例，對於表達式 λx.x x 由形式化描述的第 3 點，我們把它看作 ((λx.x)(x))，(λx.x) 和 (x) 分別為表達式，由上一例知道 (λx.x) 的自由變數集合為空，表達式 (x) 的變數集合為變數 x，所以對於 λx.x x，它的自由變數集合為 x 與空的並，即 x。

在 lambda 表達式的集合上定義了一個等價關係 (在此用 == 標註)，「兩個表達式其實表示的是同一個函式」這樣的直覺性判斷即由此表述，這種等價關係是通過所謂的「alpha - 變換規則」和「beta - 歸約規則」。

## 歸約

歸約的操作包括：

### α- 變換

Alpha - 變換規則表達的是，被繫結變數的名稱是不重要的。比如說 λx.x 和 λy.y 是同一個函式。儘管如此，這條規則並非像它看起來這麼簡單，關於被繫結的變數能否由另一個替換有一系列的限制。

Alpha - 變換規則陳述的是，若 V 與 W 均為變數，E 是一個 lambda 表達式，同時 E [V:=W] 是指把表達式 E 中的所有的 V 的自由出現都替換為 W，那麼在 W 不是
E 中的一個自由出現，且如果 W 替換了 V，W 不會被 E 中的 λ 繫結的情況下，有

　
: λV.E == λW.E[V:=W]

這條規則告訴我們，例如 λx.(λx.x) x 這樣的表達式和 λy.(λx.x) y 是一樣的。

### β- 歸約

Beta - 歸約規則表達的是函式作用的概念。它陳述了若所有的 E' 的自由出現在 E [V:=E'] 中仍然是自由的情況下，有

　
: ((λV.E) E') == E [V:=E']

成立。

== 關係被定義為滿足上述兩條規則的最小等價關係（即在這個等價關係中減去任何一個對映，它將不再是一個等價關係）。

對上述等價關係的一個更具操作性的定義可以這樣獲得：只允許從左至右來應用規則。不允許任何 beta 歸約的 lambda 表達式被稱為 **Beta 範式**。並非所有的 lambda 表達式都存在與之等價的範式，若存在，則對於相同的形式參數命名而言是唯一的。此外，有一個演算法使用者計算範式，不斷地把最左邊的形式參數替換為實際參數，直到無法再作任何可能的規約為止。這個演算法若且唯若 lambda 表達式存在一個範式時才會停止。Church-Rosser 定理說明了，若且唯若兩個表達式等價時，它們會在形式參數換名後得到同一個範式。

### η- 變換

前兩條規則之後，還可以加入第三條規則，eta - 變換，來形成一個新的等價關係。Eta - 變換表達的是外延性的概念，在這裡外延性指的是，對於任一給定的參數，若且唯若兩個函式得到的結果都一致，則它們將被視同為一個函式。Eta - 變換可以令 $\lambda x.fx$ 和 $f$ 相互轉換，只要 $x$ 不是 $f$ 中的自由變數。下面說明了為何這條規則和外延性是等價的：

若 $f$ 與 $g$ 外延地等價，即， $fa==ga$ 對所有的 $\lambda $ 表達式 $a$ 成立，則當取 $a$ 為在 $f$ 中不是自由出現的變數 $x$ 時，我們有 $f(x)==g(x)$ ，因此 $\lambda x.fx==\lambda x.gx$ ，由 eta - 變換 f == g。所以只要 eta - 變換是有效的，會得到外延性也是有效的。

相反地，若外延性是有效的，則由 beta - 歸約，對所有的 y 有 (λx .f x) y == f y，可得 λx .f x == f，即 eta - 變換也是有效的。

## 資料類型的編碼

基本的 lambda 演算法可用於建構布林值，算術，資料結構和遞迴的模型，如以下各小節所述。

### lambda 演算中的算術

在 lambda 演算中有許多方式都可以定義自然數，但最常見的還是邱奇數，下面是它們的定義：

```
0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))
```

以此類推。直觀地說，lambda 演算中的數字 n 就是一個把函式 f 作為參數並以 f 的 n 次冪為返回值的函式。換句話說，邱奇整數是一個高階函式 -- 以單一參數函式 f 為參數，返回另一個單一參數的函式。

(注意在邱奇原來的 lambda 演算中，lambda 表達式的形式參數在函式體中至少出現一次，這使得我們無法像上面那樣定義 0) 在邱奇整數定義的基礎上，我們可以定義一個後繼函式，它以 n 為參數，返回 n + 1：

```
SUCC = λn.λf.λx.f(n f x)
```

加法是這樣定義的：

```
PLUS = λm.λn.λf.λx.m f (n f x)
```

PLUS 可以被看作以兩個自然數為參數的函式，它返回的也是一個自然數。你可以試試驗證

```
PLUS 2 3 
```

與 5 是否等價。乘法可以這樣定義：

```
MULT = λm.λn.m (PLUS n) 0,
```

即 m 乘以 n 等於在零的基礎上 m 次加 n。另一種方式是

```
MULT = λm.λn.λf.m (n f)
```

正整數 n 的前驅元（predecessesor）PRED n = n - 1 要複雜一些：

```
PRED = λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)
```

或者

```
PRED = λn.n(λg.λk.(g 1) (λu.PLUS(g k) 1) k) (λl.0) 0
```

注意 `(g 1)(λu.PLUS(g k) 1) k` 表示的是，當 `g(1)` 是零時，表達式的值是 `k`，否則是 `g(k)+ 1`。

### 邏輯與謂詞

習慣上，下述兩個定義（稱為邱奇布林值）被用作 TRUE 和 FALSE 這樣的布林值：

　
: TRUE := λx.λy.x

　
: FALSE := λx.λy.y

　
: (注意 FALSE 等價於前面定義邱奇數零)

接著，通過這兩個 λ- 項，我們可以定義一些邏輯運算：

　
: AND := λp q.p q FALSE

　
: OR := λp q.p TRUE q

　
: NOT := λp.p FALSE TRUE

　
: IFTHENELSE := λp x y.p x y

我們現在可以計算一些邏輯函式，比如：

　
: AND TRUE FALSE

　
: ≡(λp q.p q FALSE) TRUE FALSE →β TRUE FALSE FALSE

　
: ≡(λx y.x) FALSE FALSE →β FALSE

我們見到 AND TRUE FALSE 等價於 FALSE。

「謂詞」是指返回布林值的函式。最基本的一個謂詞是 ISZERO，若且唯若其參數為零時返回真，否則返回假：

　
: ISZERO := λn.n (λx.FALSE) TRUE

運用謂詞與上述 TRUE 和 FALSE 的定義，使得 "if-then-else" 這類語句很容易用 lambda 演算寫出。

### 有序對

有序對（2 - 元組）資料類型可以用 TRUE、FALSE 和 IF 來定義。

　
: CONS := λx y.λp.IF p x y

　
: CAR := λx.x TRUE

　
: CDR := λx.x FALSE

連結串列資料類型可以定義為，要麼是為空串列保留的值（e.g.FALSE），要麼是 CONS 一個元素和一個更小的列表。

## 附加的編程技術

lambda 演算出現在相當大量的編程習慣用法中，其中許多程式語言最初以 lambda 演算作為語義基礎，在此背景下開發的；有效地利用 lambda 演算作為基底。因為幾個程式語言部份含括了 lambda 演算（或者非常相似的東西），所以這些技術也可以在實際的編程中見到，但有可能被認為是模糊或外來的。

### 命名常數

在 lambda 演算中，函式庫將採用預先定義好的函式集合，其中 lambda 項僅僅是特定的常數。純粹的 lambda 演算法並不具有命名常數的概念，因為所有的原子 λ 項都是變數；但是在程式主體中，我們可將一個變數當成常數的名稱，利用 lambda 抽象把這個變數綁定，並將該 lambda 抽象應用於預期的定義，來類比命名常數的作法。因此在 _N_（「主程式」的另一個 lambda 項）中，要以 _f_ 來表示 _M_（一些明確的 lambda 項），則寫成如下：

　
: (λ_f_._N_) _M_

作者經常引入類似如 let 的語法糖，允許以更直觀的次序撰寫上述內容：

　
: let _f_ = _M_ in _N_

通過等號鏈結這個命名常數，即可將 lambda 演算「編程」的一個 lambda 項，寫為零或多個函式的定義，而使用構成程式主體的那些函式。這個 let 顯著的限制，是在 _M_ 中並沒有定義 _f_ 名稱，因為 _M_ 不在綁定 _f_ 的 lambda 抽象範疇之內；這意味著遞迴函式定義不能以 let 來使用 _M_。更進步的 letrec 語法糖允許以直覺的方式編寫遞迴函式定義，而不需用到不動點組合子。

### 遞迴與不動點

遞迴是使用函式自身的函式定義；在表面上，lambda 演算不允許這樣。但是這種印象是誤解。考慮個例子，階乘函式 f(n) 遞迴的定義為

　
: f(n):= if n = 0 then 1 else n·f(n-1)。

在 lambda 演算中，你不能定義包含自身的函式。要避免這樣，你可以開始於定義一個函式，這裡叫 g，它接受一個函式 f 作為參數並返回接受 n 作為參數的另一個函式：

　
: g := λf n.(if n = 0 then 1 else n·f(n-1))。

函式 g 返回要麼常數 1，要麼函式 f 對 n-1 的 n 次應用。使用 ISZERO 謂詞，和上面描述的布林和代數定義，函式 g 可以用 lambda 演算來定義。

但是，g 自身仍然不是遞迴的；為了使用 g 來建立遞迴函式，作為參數傳遞給 g 的 f 函式必須有特殊的性質。也就是說，作為參數傳遞的 f 函式必須展開為呼叫帶有一個參數的函式 g -- 並且這個參數必須再次 f 函式！

換句話說，f 必須展開為 g(f)。這個到 g 的呼叫將接著展開為上面的階乘函式並計算下至另一層遞迴。在這個展開中函式 f 將再次出現，並將被再次展開為 g(f) 並繼續遞迴。這種函式，這裡的 f = g(f)，叫做 g 的不動點，並且它可以在 lambda 演算中使用叫做**悖論算子**或**不動點算子**來實現，它被表示為 Y -- Y 組合子：

　
: Y = λg.(λx.g(x x))(λx.g(x x))

在 lambda 演算中，Y g 是 g 的不動點，因為它展開為 g(Y g)。現在，要完成我們對階乘函式的遞迴呼叫，我們可以簡單的呼叫 g(Y g)n，這裡的 n 是我們要計算它的階乘的數。

比如假定 n = 5，它展開為：

　
: (λn.(if n = 0 then 1 else n·((Y g)(n-1)))) 5

　
: if 5 = 0 then 1 else 5·(g(Y g，5-1))

　
: 5·(g(Y g)4)

　
: 5·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 4)

　
: 5·(if 4 = 0 then 1 else 4·(g(Y g，4-1)))

　
: 5·(4·(g(Y g)3))

　
: 5·(4·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 3))

　
: 5·(4·(if 3 = 0 then 1 else 3·(g(Y g，3-1))))

　
: 5·(4·(3·(g(Y g)2)))

　
: ...

等等，遞迴的求值演算法的結構。所有遞迴定義的函式都可以看作某個其他適當的函式的不動點，因此，使用 Y 所有遞迴定義的函式都可以表達為 lambda 表達式。特別是，我們現在可以明晰的遞迴定義自然數的減法、乘法和比較謂詞。

### 標準化的組合子名稱

某一些 lambda 項有普遍接受的名稱：

　
: **I** := λ_x_._x_

　
: **K** := λ_x_.λ_y_._x_

　
: **S** := λ_x_.λ_y_.λ_z_._x_ _z_ (_y_ _z_)

　
: **B** := λ_x_.λ_y_.λ_z_._x_ (_y_ _z_)

　
: **C** := λ_x_.λ_y_.λ_z_._x_ _z_ _y_

　
: **W** := λ_x_.λ_y_._x_ _y_ _y_

　
: **U** := λ_x_.λ_y_._y_ (_x_ _x_ _y_)

　
: **ω** := λ_x_._x_ _x_

　
: **Ω** := **ω** **ω**

　
: **Y** := λ_g_.(λ_x_._g_ (_x_ _x_)) (λ_x_._g_ (_x_ _x_))

其中有幾個在「消除 lambda 抽象」中有直接的應用，將 lambda 項變為組合演算的術語。

### 消除 lambda 抽象

如果 _N_ 是一個沒有 λ- 抽象的 lambda 項，但可能包含了命名常數（組合子），則存在一個 lambda 項 _T_(_x_,_N_)，這相同於一個缺少 λ- 抽象（除了作為命名常數的一部份，如果這些被認為是非原子的）的 λ_x_._N_；也可以被視為匿名變數，就如同 _T_(_x_,_N_) 從 _N_ 之中刪除所有出現的 _x_，同時仍然允許在 _N_ 包含 _x_ 的位置替換參數值。

轉換函式 _T_ 可由下式定義：

　
: _T_(_x_, _x_) := **I**

　
: _T_(_x_, _N_) := **K** _N_ if _x_ is not free in _N_.

　
: _T_(_x_, _M_ _N_) := **S** _T_(_x_, _M_) _T_(_x_, _N_)

在這兩種情況下，形式 _T_(_x_,_N_)_P_ 可藉由使初始的組合子 **I**，**K** 或 **S** 獲取參數 _P_ 而化簡，
就像 (λ_x_._N_) _P_ 經過 β- 歸約一樣。**I** 返回那個參數。**K** 則將參數拋棄，就像 (λ_x_._N_)，如果 _x_ 在 _N_ 中不是以自由變數出現。**S** 將參數傳遞給應用程式的兩個子句，然後將第一個結果應用到第二個的結果之上。

組合子 **B** 和 **C** 類似於 **S**，但把參數傳遞給應用的一個子項（**B** 傳給「參數」子項，而 **C** 傳給「函式」子項），如果子項中沒有出現 _x_，則儲存後續的 **K**。與 **B** 和 **C** 相比，**S** 組合子實際上混合了兩個功能：
重新排列參數，並複製一個參數，以便它可以在兩個地方使用。**W** 組合子只做後者，產生了 SKI 組合子演算的 B，C，K，W 系統。

## 可計算函式和 lambda 演算

自然數的函式 F: **N** → **N** 是可計算函式，若且唯若存在著一個 lambda 表達式 f，使得對於 **N** 中的每對 x, y 都有 F(x) = y 若且唯若 f x == y，這裡的 x 和 y 分別是對應於 x 和 y 的邱奇數。這是定義可計算性的多種方式之一；關於其他方式和它們的等價者的討論請參見邱奇 - 圖靈論題。

## lambda 演算與程式語言

### 匿名函式

比如計算平方的函式 square 在 Lisp 中可以表示為如下的 lambda 表達式

符號 lambda 建立一個匿名函式，給定參數列 (x) ，以及一個作為函式體的表達式 (\* x x)。 匿名函式有時稱為 lambda 表達式。

很多命令式語言都有函式指標或者類似的機制。但是函式指標並不是類型中的一等公民，函式是一等公民若且唯若函式可以在執行時建立。 下面一些語言支援函式的執行時建立： Smalltalk、 JavaScript、 Kotlin、 Scala、 Python3、 C# ("delegates")、 C++11 等。

### 化簡策略

### 關於複雜度的註釋

### 並行與並發

## 參見

* 邱奇 - 圖靈論題
* 遞迴函式
* 可計算函式
* 柯里化

## 參考文獻

## 外部連結

* L.Allison, Some executable λ-calculus examples （頁面存檔備份，存於網際網路檔案館）
* Georg P.Loczewski, The Lambda Calculus and A++ （頁面存檔備份，存於網際網路檔案館）
* To Dissect a Mockingbird: A Graphical Notation for the Lambda Calculus with Animated Reduction
* 人物介紹
* 神奇的 λ 演算 （頁面存檔備份，存於網際網路檔案館）
* (譯) The Y combinator (Slight Return)
* Λ 運算︰淵源介紹 （頁面存檔備份，存於網際網路檔案館）