此系列文章是我學(xué)習(xí)lambda演算過程的總結(jié)與復(fù)習(xí)榆浓，著重于探討“為什么(Why)”與“怎么做(How)”，也希望能對(duì)看到它的人學(xué)習(xí)了解這個(gè)形式系統(tǒng)有些微幫助弱贼。由于之前看了不少wiki蒸苇、tutorial、introduction之流吮旅，絕大多數(shù)讀過之后僅知其然而不知其所以然溪烤，我不知道為什么它們都不解釋為什么要這么做，為什么要有這些東西庇勃，這些東西是怎么得來的檬嘀，但這個(gè)事實(shí)讓我非常苦惱责嚷，因此才有了這個(gè)系列鸳兽。我試圖將自己的淺薄理解稍作闡釋梳理，知之尚淺罕拂，如有錯(cuò)漏不妥之處請(qǐng)不吝指出揍异，歡迎交流討論批評(píng)建議。

部分參考：
Wikipedia
SEP(Stanford Encyclopedia of Philosophy)
Brilliant
Cornell Recitation Course
一個(gè)有翻譯的tutorial：[翻譯] [原文]
一個(gè)完全how to的introduction

NOTE: 在lambda演算中聂受，函數(shù)是一等公民蒿秦。即對(duì)函數(shù)做一般的基本操作都是合法的，比如把函數(shù)作為參數(shù)傳入或返回蛋济，賦給一個(gè)變量等等棍鳖。

lambda | λ 定義

要描述一個(gè)形式系統(tǒng)，我們首先需要約定用到的基本符號(hào)，對(duì)于本系列所介紹的lambda演算渡处，其符號(hào)集包括λ . ()和變量名(x, y, z, etc.)镜悉。

1. λ 表達(dá)式/項(xiàng)

在lambda演算中只有三種合法表達(dá)式（也可以稱之為項(xiàng)：λ-expression or λ-term）存在：

• 變量(Variable)
  形式：x
  變量名可能是一個(gè)字符或字符串，它表示一個(gè)參數(shù)（形參）或者一個(gè)值（實(shí)參）医瘫。
  e.g. z var
• 抽象(Abstraction)
  形式：λx.M
  它表示獲取一個(gè)參數(shù)x并返回M的lambda函數(shù)侣肄，M是一個(gè)合法lambda表達(dá)式，且符號(hào)λ和.表示綁定變量x于該函數(shù)抽象的函數(shù)體M醇份。簡(jiǎn)單來說就是表示一個(gè)形參為x的函數(shù)M稼锅。
  e.g. λx.y λx.(λy.xy)
  前者表示一個(gè)常量函數(shù)(constant function)，輸出恒為y與輸入無關(guān)僚纷；后者的輸出是一個(gè)函數(shù)抽象λy.xy矩距，輸入可以是任意的lambda表達(dá)式。
  注意：一個(gè)lambda函數(shù)的輸入和輸出也可以是函數(shù)怖竭。
• 應(yīng)用(Application)
  形式：M N
  它表示將函數(shù)M應(yīng)用于參數(shù)N锥债，其中M、N均為合法lambda表達(dá)式痊臭。簡(jiǎn)單來說就是給函數(shù)M輸入實(shí)參N哮肚。
  e.g. (λx.x) y, (λx.x) (λx.x)
  前者表示將函數(shù)λx.x應(yīng)用于變量y，得到y广匙；后者表示將函數(shù)λx.x應(yīng)用于λx.x允趟，得到λx.x。函數(shù)λx.x是一個(gè)恒等函數(shù)(identity function)鸦致，即輸入恒等于輸出拼窥，它可以用 I 來表示。

這時(shí)候可能就有人納悶兒了蹋凝，(λx.x) y意義很明確，但λy.xy為什么代表函數(shù)抽象而不是將函數(shù)λy.x應(yīng)用于y的函數(shù)應(yīng)用呢总棵？為了消除類似的表達(dá)式歧義鳍寂，可以多使用小括號(hào)，也有以下幾個(gè)消歧約定可以參考：

• 一個(gè)函數(shù)抽象的函數(shù)體將盡最大可能向右擴(kuò)展情龄，即：λx.M N代表的是一個(gè)函數(shù)抽象λx.(M N)而非函數(shù)應(yīng)用(λx.M) N迄汛。
• 函數(shù)應(yīng)用是左結(jié)合的，即：M N P意為(M N) P而非M (N P)骤视。

2. 自由變量和綁定變量

前面提到在函數(shù)抽象中鞍爱，形參綁定于函數(shù)體，即形參是綁定變量专酗，相對(duì)應(yīng)地睹逃，不是綁定變量的自然就是自由變量。咱們來通過幾個(gè)例子來理解這個(gè)關(guān)系：

• λx.xy：其中x是綁定變量，y是自由變量沉填；
• (λy.y)(λx.xy)：這個(gè)表達(dá)式可以按括號(hào)劃分為兩個(gè)子表達(dá)式M和N疗隶，M的y是綁定變量，無自由變量翼闹，N的x是綁定變量斑鼻，y是自由變量且與M無關(guān)；
• λx.(λy.xyz)：這個(gè)表達(dá)式中的x綁定于外部表達(dá)式猎荠，y綁定于內(nèi)部表達(dá)式坚弱，z是自由變量。

由于每個(gè)lambda函數(shù)都只有一個(gè)參數(shù)关摇，因此也只有一個(gè)綁定變量荒叶，這個(gè)綁定變量隨著形參的變化而變化。
我們用FV來表示一個(gè)lambda表達(dá)式中所有自由變量的集合拒垃，如：

FV(λx.xy) = {y}
FV((λy.y)(λx.xy)) = FV(λy.y) ∪ FV(λx.xy) = {y}
FV(λx.(λy.xyz)) = FV(λy.xyz) \ x = {x,z} \ x = {z}

3. 柯里化(Currying)

有時(shí)候我們的函數(shù)需要有多個(gè)參數(shù)停撞，這太正常不過了，但是lambda函數(shù)只能有一個(gè)參數(shù)怎么辦悼瓮？解決這個(gè)問題的方法就是柯里化(Currying)戈毒。
柯里化是用于處理多參數(shù)輸入情況的方法，我們已經(jīng)知道一個(gè)lambda函數(shù)的輸入和輸出也可以是函數(shù)横堡，那么基于它埋市，可以把多參數(shù)函數(shù)和單參數(shù)函數(shù)做以下轉(zhuǎn)換：
currying: λx y.xy = λx.(λy.xy)
外層函數(shù)接受一個(gè)參數(shù)x返回一個(gè)函數(shù)λy.xy，這個(gè)返回函數(shù)（內(nèi)層函數(shù)）又接受一個(gè)參數(shù)y返回xy命贴，x綁定于外層函數(shù)道宅，y綁定于內(nèi)層函數(shù)，這樣我們就在滿足lambda函數(shù)只接受一個(gè)參數(shù)的約束下實(shí)現(xiàn)了多參數(shù)函數(shù)的功能胸蛛，這就是柯里化污茵，而λx y.xy稱為λx.(λy.xy)的縮寫，為了方便表達(dá)葬项，后續(xù)會(huì)常常出現(xiàn)λx y.xy這樣的書寫方式泞当，需要謹(jǐn)記它只是縮寫寫法。

lambda | λ 歸約

我們已經(jīng)知道了lambda表達(dá)式的基本定義與語法民珍，下面將介紹如何對(duì)一個(gè)lambda表達(dá)式進(jìn)行歸約(reduction)襟士。

1. beta | β 歸約

對(duì)于一個(gè)函數(shù)應(yīng)用(λx.x) y，它意為將函數(shù)應(yīng)用λx.x應(yīng)用于y嚷量，等價(jià)于x[x:=y]陋桂，即結(jié)果是y。在這個(gè)過程中蝶溶，(λx.x) y ≡ x[x:=y]一步就叫做beta歸約嗜历，x[x:=y] ≡ y一步稱作替換(substitution)，[x:=y]意為將表達(dá)式中的自由變量x替換為y。

• 替換
  形式：E[V := R]
  意為將表達(dá)式E中的所有 “自由變量” V替換為表達(dá)式R秸脱。對(duì)于變量x,y和lambda表達(dá)式M,N落包，有以下規(guī)則：

x[x := N]       ≡ N
y[x := N]       ≡ y //注意 x ≠ y
(M1 M2)[x := N] ≡ (M1[x := N]) (M2[x := N])
(λx.M)[x := N]  ≡ λx.M //注意 x 是綁定變量無法替換
(λy.M)[x := N]  ≡ λy.(M[x := N]) //注意 x ≠ y, 且表達(dá)式N的自由變量中不包含 y 即 y ? FV(N)

• beta歸約
  形式：β: ((λV.E) E′) ≡ E[V := E′]
  其實(shí)就是用實(shí)參替換函數(shù)體中的形參，也就是函數(shù)抽象應(yīng)用(apply)于參數(shù)的過程啦摊唇，只不過這個(gè)參數(shù)除了是一個(gè)變量還可能是一個(gè)表達(dá)式咐蝇。

細(xì)心的話可以注意到，替換規(guī)則中特別標(biāo)注了一些x ≠ y或者y ? FV(N)等約束條件巷查，它們的意義在于防止lambda表達(dá)式的歸約過程中出現(xiàn)歧義有序。
比如以下過程：

(λx.(λy.xy)) y
= (λy.xy)[x:=y] //beta歸約：注意 y ∈ FV(y) 不滿足替換的約束條件
= λy.yy //替換：綁定變量y與自由變量y同名出現(xiàn)了沖突

可以看出在不滿足約束條件的情況強(qiáng)行替換造成了錯(cuò)誤的結(jié)果，那么對(duì)于這種情況該如何處理呢岛请？那就需要alpha轉(zhuǎn)換啦旭寿。

2. alpha | α 轉(zhuǎn)換

這條規(guī)則就是說，一個(gè)lambda函數(shù)抽象在更名綁定變量前后是等價(jià)的崇败，即：
α: λx.x ≡ λy.y
其作用就是解決綁定變量與自由變量間的同名沖突問題盅称。
那么對(duì)于上面的那個(gè)錯(cuò)誤歸約過程就可以糾正一下了：

(λx.(λy.xy))y
= (λy.xy)[x:=y] //beta歸約：注意 y ∈ FV(y) 不滿足替換的約束條件
= (λz.xz)[x:=y] //alpha轉(zhuǎn)換：因?yàn)榻壎ㄗ兞縴將與自由變量x（將被替換為y）沖突，所以更名為z
= λz.yz

Perfect后室！這樣對(duì)于lambda演算最基礎(chǔ)的定義與歸約規(guī)則已經(jīng)介紹完畢了缩膝，雖然內(nèi)容很簡(jiǎn)單，但是卻很容易眼高手低岸霹，要試著練習(xí)喔疾层。

3. eta | η 歸約

靈活運(yùn)用alpha和beta已經(jīng)可以解決所有的lambda表達(dá)式歸約問題，但是考慮這樣一個(gè)表達(dá)式：

λx.M x

將它應(yīng)用于任意一個(gè)參數(shù)上贡避，比如(λx.M x) N痛黎，進(jìn)行beta歸約和替換后會(huì)發(fā)現(xiàn)它等價(jià)于M N，這豈不是意味著

λx.M x ≡ M

沒錯(cuò)刮吧，對(duì)于形如λx.M x湖饱，其中表達(dá)式M不包含綁定變量x的函數(shù)抽象，它是冗余的杀捻，等價(jià)于M琉历，而這就是eta歸約，它一般用于清除lambda表達(dá)式中存在的冗余函數(shù)抽象水醋。

To be continued...