你好，類型（二）：Lambda calculus

1. 匿名函數

現在很多種編程語言都支持匿名函數了，

例如，C# 3.0，C++ 11和Java 8中的lambda表達式，

又例如，Python 2.2.2中的lambda，ECMAScript 3的匿名函數，

ECMAScript 2015的箭頭函數（arrow function）等等。

更不論，Haskell，Lisp，Standard ML，這些函數式編程語言了。

越來越多的語言擁抱匿名函數，是因為在很多場景中，我們無需給函數事先指定一個名字，

並且結合詞法作用域和高階函數，會使某些問題用更直觀的方式得以解決。

從理論上來講，匿名函數具有和一般函數同樣的計算能力，

使用某些技術手段，可以讓匿名函數支持遞歸運算，從而完成任何圖靈可計算的任務。

然而，要想理解這一切，我們首先還得靜下心來，從基礎的 演算開始吧。

2. 自然數

演算聽起來是一個高大上的概念，實際上它只是一套「符號推導系統」。

人們首先定義某些合法的符號，然後再定義一些符號推導規則，

最後就可以計算了，從一堆合法的符號得到另一堆，

這種推導過程稱之為「演算」。

為了讓 演算更容易被接受，我們暫時先岔開話題，看看自然數是怎麼定義的。

2.1 Peano系統

1889年，皮亞諾（Peano）為了給出自然數的集合論定義，

他建立了一個包含5條公設的公理系統，後人稱之為Peano系統。

Peano系統是滿足以下公設的有序三元組 ，

其中 為一個集合， 是 到 的函數， 為首元素，

（1）

（2） 在 下是封閉的

（3） 不在 的值域中

（4） 是單射

（5）如果 的子集 滿足， ，且 在 下封閉，則 。

2.2 後繼

設 為一個集合，我們稱 為 的後繼，記作 ，

求集合後繼的操作，稱為後繼運算。

例如，

，

，

。

2.3 歸納集

設 為一個集合，若 滿足，

（1）

（2） ，

則稱 是歸納集。

例如， 是一個歸納集。

從歸納集的定義可知， 是所有歸納集的元素，

於是，可以將它們定義為自然數，自然數集記為 。

設 ，滿足 ，則稱 為後繼函數，

則可以證明 是一個Peano系統。

3. λ演算

λ演算，是1930年由邱奇（Alonzo Church）發明的一套形式系統，

它是從具體的函數定義，函數調用和函數複合中，抽象出來的數學概念。

3.1 語法

形式上， 演算由3種語法項（term）組成，

（1）一個變數 本身，是一個合法的 項，

（2） ，是一個合法的 項，稱為從項 中抽象出 ，

（3） ，是一個合法的 項，稱為將 應用於 。

例如， ， ， ，都是合法的 項。

為了簡化描述，我們通常會省略一些括弧，以上三個 項可以寫成，

， ， ，

對於形如 的 項來說，「 」後面會向右包含盡量多的內容。

現在我們有了一堆合法的字元串了。

可是，在給定推導規則之前，這些字元串之間都是沒有關聯的。

而且，我們也還沒有為這些符號指定語義，它們到底代表什麼也是不清楚的。

很顯然給這些符號指定不同的推導規則，會得到不同的公理系統，

在眾多 演算系統中，最簡單的是 系統，它指定了 和 兩種變換。

3.2 α變換

設 項 中包含了 ，

則我們可以把 中所有自由出現的 ，全都換成 ，即 ，

這種更名變換，稱為 變換。

其中，「自由出現」指的是 不被其他 抽象所綁定，

例如， 中， 是自由的，

而 就不是自由的，因為它被 綁定了。

如果 可以經過有限步 變換轉換為 ，就寫為 。

例如，

3.3 β變換

形如 的 項，可以經由 變換轉換為 ，

指的是，把 中所有自由出現的 都換成 。

如果 可以經過有限步 變換轉換為 ，就寫為 。

例如，

我們發現，某些 項，可以無限進行 變換。

而那些最終會終止的 變換的結果，稱為 範式（ normal form）。

3.4 邱奇編碼

現在我們有 公理系統了，就可以依照 或 變換，對任意合法的 項進行變換。

假設我們有一個 項， ，

還有另外一個 項， ，記為 ，

我們來計算， ，

可得， ，

我們再運用一次 ， 。

我們發現每次應用 ，都會給 中加一個 ，

最終我們可以得到以下這些 項，

如果我們記 ， ， ， ，

我們就得到了自然數的另一種表示方式，稱之為邱奇編碼。

可以看到邱奇編碼與歸納集之間有異曲同工之妙。

3.5 語義

到目前為止，我們並未談及 項到底表示什麼含義，

雖然 看起來像是函數定義， 看起來像是函數調用。

我們謹慎的使用公理化方法，從什麼是合法的 項出發，

定義 系統中的公理——合法的 項，

然後又指定了該系統中的推導規則—— 和 變換，

最終得到了一個形式化的公理系統（公理+推導規則）。

後文中，我們將談及 項的語義，然後再逐漸給它加上類型。

---

參考

離散數學教程

Lambda-Calculus and Combinators，an Introduction

Lecture Notes on the Lambda Calculus

---

下一篇：你好，類型（三）：Combinatory logic

推薦閱讀：