[Functional Programming] 初探 lambda calculus

前言#

去年鐵人賽寫了 functional programming 主題，在 Day 30 的時候列了一些待讀清單，當時也有大大有推薦讀物，這陣子決定先從《Haskell Programming From First Principles》開始，一樣想依據書中章節順序，撰寫文章說明相關概念，作為我的讀書筆記。按照慣例(?，文章內容會以書中敘述為主，輔以相關資料，部分內容可能是書中沒有、而是我另外補充的資訊，範例程式碼也不一定會和書中相同，示意圖有些是我按照自己的理解重繪的，也不一定和書中圖完全相同，想了解完整書籍內容一樣歡迎大家去買書看。

因為還有其他事情要忙，讀書筆記就讀到哪寫到哪囉，內容若有任何錯誤歡迎大家回覆告訴我～

此篇敘述的是第一章 All You Need is Lambda。

另外補充，有些英文詞彙我不確定中文怎麼翻比較好，所以文章會有中英夾雜的狀況，還請見諒><

什麼是 lambda?#

lambda calculus (λ 演算) 是 1930 年代由 Alonzo Church 提出的計算模型。calculus 又是什麼呢? calculus 是一種計算或推理的方法，而 lambda calculus 則是一種將計算方式形式化的方法。

補充：λ 讀作 lambda

lambda calculus 將計算方式形式化，以界定哪些問題或問題類型是可被解決的。而 Haskell 本質上就是一個 lambda calculus 的語言。那什麼叫做「將計算方式形式化」?簡單來說，就是把「怎麼計算」這件事，用非常精確的規則寫下來。

什麼是 functional programming?#

Functional programming is a computer programming paradigm that relies on functions modeled on mathematical functions.

functional programming 是一種電腦程式設計範式，它依賴以數學函數為模型的函數。

在 functional programming 中，程式的核心是「表達式（expressions）」，所謂的表達式包含幾個要素：

具體值（concrete values）
變數（variables）
函數（functions）

那 function 又是什麼? function 是「應用在某個參數（argument/input）上」的表達式，一旦被應用，就能被「化簡（reduced）」或「求值（evaluated）」

function 在 functional programming 和 Haskell 中是作為 first-class function 的，也就是我在 [Day 08] First-Class Functions 和 Higher-Order Functions (1)：簡介與 forEach 提到的，first-class function 可以…

當成值使用
當作參數傳入其他函數
作為其他函數的輸出

為什麼學 functional programming 要先認識 lambda 呢?

因為所有函數式語言都以 lambda calculus 為基礎（雖然有些語言會加入 lambda calculus 無法直接表達的特性）。不過 Haskell 是純函數式語言（pure functional language），因為它沒有加入那些無法翻成 λ 表達式的語法。

什麼是「純」函數式語言？#

當我們說這是一個純函數式語言時，到底是什麼意思? 更準確來說，「purity(純)」其實是指「referential transparency (參照透明)」，引用透明在 [Day04] Pure Function 是什麼？有提到，簡單來說 referential transparency 就是同一個函數在給定相同的輸入時，總是會傳回相同的結果，就像在數學中的運算一樣。

純函數的基礎可以為 Haskell 帶來兩個特性：

抽象性
- 抽象性讓我們能將重複的結構抽取成通用的程式碼，提高重用性能讓程式更精簡
可組合性
- Haskell 程式由獨立、分離的函數組成，就像樂高積木一樣，函數可以任意搭配

什麼是 function?#

A function is a relation between a set of possible inputs and a set of possible outputs.

function 定義並代表一種關係，它代表一組可能的輸入與一組可能的輸出之間的關係，舉例來說，將「加法」函數應用到兩個輸入，就是把那兩個輸入對應到一個輸出（它們的和）。

function 的對應舉例#

假設一個函數 𝑓 定義如下，定義了輸入與輸出的關係：

$𝑓(1) = A$
$𝑓(2) = B$
$𝑓(3) = C$

在這定義關係中，輸入的集合（domain）是 ${1, 2, 3}$ ，輸出的集合（codomain）是 ${A, B, C}$ ，此關係中，若輸入是 1，輸出一定是 A。

補充

domain（輸入集合）：所有可能輸入的集合
codomain（輸出集合）：所有可能輸出的集合
domains 與 codomains 都由「不重複的值」組成
image：codomain 中真正「會被函數產生」的輸出子集合
domain → image 或 domain → codomain 的映射不必是 1 對 1
多個輸入可對應到同一輸出（例如不同輸入都對應到 true / false）
一個輸入不得對應到多個不同輸出

無效的 function 例子#

假設一個函數 𝑓 定義如下，那它會是一個無效的 function：

$𝑓(1) = X$
$𝑓(1) = Y$
$𝑓(2) = Z$

原因是同一個輸入 1 對應到兩個不同的輸出（X、Y）。

這兩個例子的關鍵差異是 referential transparency，referential transparency 要求同樣的輸入必須得到可預測且一致的輸出。

有效的 function 例子：多個輸入對應同一輸出#

假設一個函數 𝑓 定義如下，它是有效的 function，因為多個輸入對應同一輸出是合法的，符合 referential transparency。

$𝑓(1) = A$
$𝑓(2) = B$
$𝑓(3) = C$

一個判斷正整數是否小於 20 的 function，就是一個多個輸入對應相同輸出的 function：

小於 20 的所有輸入，都會輸出 true
其他輸入，則都輸出 false

有效的 function 例子：定義對應關係#

假設有個函數 𝑓 定義如下：

$𝑓(𝑥) = 𝑥 + 1$

f 接受一個參數 x，且函數本體描述輸入與輸出的關係，這關係就是輸入 x 時，會回傳輸出 x + 1。

接著我們可以將函數應用到一個值上面(apply function to a value)，假設我們將輸入 1 代入 x：

$𝑓(1) = 1 + 1$

下一步可以求出實際輸出值，也就是 2：

$𝑓(1) = 2$

lambda expression 的結構#

lambda calculus 有三個基本的元素，或稱之為三個 lambda terms：

Expressions（表達式）
Variables（變數）
Abstractions（抽象/函數）

expressions（表達式）#

表達式是上述所有項目的 superset(超集合)，換句話說它可以是：

變數名稱
抽象（abstraction）
兩者的組合

最簡單的 expression 就是單一變數，變數在這裡沒有特別的意義或值，只是函數可能的輸入名稱。

abstraction（抽象/函數）#

abstraction 等於 function(函數)，abstraction 分為兩部分：

head（函數頭）
body（函數本體）
- body 可被應用於（applied to）一個參數（argument）。這裡說的參數（argument）指的是輸入值（input value）。

abstraction/function 結構說明#

head 就是 λ + 一個變數名稱
body 則是另一個表達式

舉例來說，這是一個 abstraction： $λx.x$

變數綁定（binding）#

head 中的變數等於參數，此參數會綁定（bind）在 body 中相同名稱的所有變數。

以 $λx.x$ 這 function 來說，當這 function 被應用到一個 argument 時，body 中所有 x 會被取代為該 argument 的值。

Application（應用）#

將 lambda function 應用到一個 argument 的行為，稱為 application，application 是 lambda calculus 的核心機制。

具名與匿名函數#

我們前面舉例提到的 function 𝑓 屬於具名函數；而 $λx.x$ 是沒有名字的 function，屬於匿名函數，兩者差異在於具名函數可以被其他函數用名稱呼叫，反之匿名函數無法以名稱被呼叫。

$λx.x$ 的結構解析#

進一步看一下 $λx.x$ 中每個元素的意思。

首先 $λx$ 是 head 的範圍。

$λ$ 後面的 $x$ 是 function 的單一參數(parameter)，用來綁定 body 中名稱相同的變數。

中間的點. 用來分隔參數與 body，. 後面的 $x$ 是 function 的 body，這是 function 在應用時會回傳的表達式。這裡的 $x$ 是被 head 中的參數綁定的 bound variable。

Abstraction 為什麼叫 abstraction?#

前面有說 abstraction 就等於 function 的意思，那為什麼不直接稱作 function 而要叫作 abstraction?

稱作 abstraction，是因為它是從具體問題的實例抽象而來，引入具體的名稱就可以實現抽象，當 abstraction 被應用到 arguments 時，名稱就會被值替換，變得具體。我的理解是，abstraction 有點像是一個抽象化的建築藍圖，只有實際實作、實際開始蓋房子的時候，才會變得具體。

Alpha Equivalence#

在 lambda calculus 中，x 這個變數名稱本身沒有語意意義，不代表特定意思，因此以下 lambda 表達式都是等價的：

$λx.x$
$λa.a$
$λc.c$

上述三者在原則上表示相同的函數，這種等價關係稱為 alpha equivalence。

Beta reduction#

Beta Reduction 是什麼?#

當我們將函數應用到一個參數（argument）時，會執行以下步驟：

將該參數取代 abstraction body 中所有綁定變數（bound variables）的實例
同時刪除 abstraction 的 head（因為 head 只負責綁定變數）

而這過程就稱為 beta reduction（β 簡化）。

範例： $λx.x$ （identity function）#

假設現在有個 $λx.x$ function，將它應用到數字 2 上，會長這樣： $(λx.x) 2$ ，接著將 body 的 x 帶入 2，同時去除 head 的 λx，就會得到 $2$ 。在這 function 中，唯一的 bound variable 是 x，綁定後得出的結果為 2。

另外， $λx.x$ 這個 function 又稱為 identity function（恆等函數），identity function 會接收一個參數然後回傳該參數。

補充

λ calculus 本身可以「用純 lambda 抽象定義數字」（即 Church numerals），而不需用我們習慣的數字符號，但寫起來會較難閱讀。
$λx.x$ 與數學中的 $f(x) = x$ 是同一種恆等關係。 $f(x) = x$ 是「命名一個叫 f 的函數」，屬於具名函數； $λx.x$ 是「直接寫出函數本身」，屬於匿名函數。

帶運算的範例#

如果有個 lambda $(λx. x + 1)$ ，當它應用到 2 時，結果會是什麼?

試走一次 beta reduction 的應用過程：

應用 lambda term 到一個 argument（參數）
- 也就是將 $(λx. x + 1)$ 應用到 2，會長這樣： $(λx. x + 1)2$
用 argument 取代 body 內所有 bound variables
- 也就是用 $2$ 取代 $x+1$ 這 body 內的所有 $x$ ，變成 $2+1$ ，得到 $3$
移除 head $λx$ $λ x$ ，移除 head 表示 function 已經被成功應用(applied)
- 最後會得到 $3$

應用 $λx.x$ 到另一個 lambda abstraction#

$(λx.x)(λy.y)$ 的意思是將 $λx.x$ 應用到 $(λy.y)$ 這參數上，會用 $(λy.y)$ 這整個 abstraction 來取代 $x$ 。

語法 $[𝑥 := 𝑧]$ 表示 𝑧 會取代所有出現的 𝑥，在這裡 $(λy.y)$ 會取代所有的 $x$ ，所以是 $[𝑥 := (λy.y)]$ 。

整個 Beta Reduction 過程如下：

$(λx.x)(λy.y)$
$[x := (λy.y)]$
$λy.y$

最後的結果是 identity function，因為沒有 argument 可以繼續應用，reduction 結束。

再加入另一個 argument#

lambda calculus 的應用預設為左結合（left associative），符合左結合律，除非括號另有說明。如果以左結合律來看 $(λx.x)(λy.y) z$ ， $(λx.x)(λy.y) z$ 會等於 $((λx.x)(λy.y)) z$ ，會先從左邊兩個括號開始看。

試走一次 Beta Reduction 過程如下：

$((λx.x)(λy.y)) z$
$[x := (λy.y)]$
$(λy.y) z$
$[y := z]$
$z$

最後結果會得到 $z$ ，因為對 $z$ 毫無資訊，不能再簡化。

Beta Reduction 的停止條件#

遇到以下任一條件時，beta reduction 就會停止：

沒有尚未求值的函數應用
head 已全部消除
沒有 arguments 可再應用

以上面 $((λx.x)(λy.y)) z$ 的 Beta Reduction 來說，因為最後得到的 $z$ 符合這三種條件，因此 Beta Reduction 就停止了。

Free variables#

在 lambda calculus 中有分兩種 variables，Bound Variables 與 Free Variables。 Bound Variables 與 Free Variables 和 lambda calculus 的 head 有關，head 的目的是指出 body 中哪些變數應被替換（綁定），Bound variable 就是指出現在 head 的變數；而 Free Variables 就是未在 head 中命名的變數。

以 $λ𝑥.𝑥𝑦$ 為例，x 出現在 head，是 bound variable，而 y 沒出現在 head，是 free variable。如果要應用函數到 argument 時，x 會被替換，y 則保持不變(irreducible)。

應用包含 free variable 的 abstraction#

試跑一次 $(λ𝑥.𝑥𝑦)𝑧$ 的 beta reduction 流程。

將 lambda 應用到 argument $z$

(λ𝑥.𝑥𝑦)𝑧

替換 bound variable，body 出現的所有 $x$ 都會變成 $z$ ，然後移除 head

(λ[𝑥 ∶= 𝑧].𝑥𝑦)

替換後得到 $𝑧𝑦$ ，沒有其他 head 或 bound variable，不可再簡化，其中 y 是 free variable，保持不變

Alpha equivalence 與 free variable#

Alpha equivalence 不適用於 free variable，舉例來說， $λx.xz$ 和 $λx.xy$ ，因為 z 和 y 是 free variable，可能代表不同東西，兩者不等價。

可以等價的情況例如：

都是 bound variable，只有 bound variable 名稱改變，屬於 alpha equivalence。以下兩者等價。

$λxy.yx$
$λab.ba$

free variable（z）保持不動，只有 bound variable 名稱改變，屬於 alpha equivalence。以下兩者等價。

$λx.xz$
$λy.yz$

多個參數#

每個 lambda 只能綁定一個參數#

一個 lambda abstraction 只能綁定一個參數，且只能接受一個 argument。 如果需要多參數的函數，需使用「多層巢狀的 lambda heads」。

語法上的「連寫」只是巢狀 lambda 的簡寫#

$λxy.xy$ 並不是一次應用多參數的意思， $λxy.xy$ 等價於巢狀形式，一個 lambda 針對一個 argument，也就是 $λx.(λy.xy)$ 。

$λx.(λy.xy)$ 可以理解成，先定義一個函數，接收一個參數 $x$ ，這函數會回傳另一個函數，回傳的函數接收一個參數 $y$ ，然後在 body 裡做 $xy$ 。

Currying（柯里化）#

以上述 $λxy.xy$ 為例， $λx.(λy.xy)$ 逐層應用 argument 的流程如下：

應用第一個 argument $(λy.xy)$
綁定 x
移除外層 lambda，得到 $(λy.xy)$
接著第二個 lambda $(λy.xy)$ 再等待下一個 argument 應用

這種逐層應用的方式，在 1920s Moses Schönfinkel 首次提出，後來 Haskell Curry 推廣並以他命名，也就是我們常聽到的 Currying（柯里化），也因此嚴格的 Currying 函數一次只能傳入一個參數，只有寬鬆版的才能一次傳入多個。關於 Currying 介紹可參考 [Day 10] Currying（柯里化）簡介。

多參數 Beta Reduction 範例#

以 $λxy.xy$ 為例來說明 beta reduction 流程。

$λxy.xy$
$(λxy.xy)(λz.a) 1$ $(λ x y . x y) (λ z . a) 1$
- $λxy.xy$ 收到兩個參數，第一個參數是一個 lambda $(λ𝑧.𝑎)$
$(λx.(λy.xy))(λz.a) 1$ $(λ x . (λ y . x y)) (λ z . a) 1$
- 取出最左側 $λx$ 作為目前的 head，準備應用第一個參數 $(λ𝑧.𝑎)$
$[𝑥 ∶= (λ𝑧.𝑎)]$ $[x ∶ = (λ z . a)]$
- $λ𝑦.𝑥𝑦$ 這 body 內的 $x$ 都綁定 $(λ𝑧.𝑎)$
$(λ𝑦.(λ𝑧.𝑎)𝑦) 1$ $(λ y . (λ z . a) y) 1$
- 取出最左側 $λ𝑦$ 作為目前的 head，準備應用參數 $1$
$[𝑦 ∶= 1]$ $[y ∶ = 1]$
- $(λ𝑧.𝑎)𝑦$ 這 body 內的 $y$ 都綁定 $1$
$(λ𝑧.𝑎) 1$ $(λ z . a) 1$
- $λ𝑧$ 這 head 準備應用參數 1
$[𝑧 ∶= 1]$ $[z ∶ = 1]$
- $a$ 這 body 內的 $z$ 都綁定 1
$𝑎$ $a$
- 因為 $a$ 這 body 裡沒有 $z$ ，所以直接去除 head $λ𝑧$ ，回傳 $a$

使用抽象變數的範例#

補充一下，因為 alpha equivalence，有時會看到 $(λ𝑥𝑦.𝑥𝑥𝑦)(λ𝑥.𝑥𝑦)(λ𝑥.𝑥𝑧)$ 這種表達式，每個變數都綁定不同 head，在替換過程可能產生混亂，為了方便理解，此書範例會使用不同變數，但變數名/字母沒有任何特殊意義。

接下來以 $(λ𝑥𝑦𝑧.𝑥𝑧(𝑦𝑧))(λ𝑚𝑛.𝑚)(λ𝑝.𝑝)$ 為例說明 beta reduction 流程。

$(λ𝑥𝑦𝑧.𝑥𝑧(𝑦𝑧))(λ𝑚𝑛.𝑚)(λ𝑝.𝑝)$
$(λ𝑥.λ𝑦.λ𝑧.𝑥𝑧(𝑦𝑧))(λ𝑚.λ𝑛.𝑚)(λ𝑝.𝑝)$ $(λ x . λ y . λ z . x z (yz)) (λm . λn . m) (λ p . p)$
- 這步驟只是讓 currying 變得明顯，將每一個 head 獨立出來
$(λ𝑦.λ𝑧.(λ𝑚.λ𝑛.𝑚)𝑧(𝑦𝑧))(λ𝑝.𝑝)$ $(λ y . λ z . (λm . λn . m) z (yz)) (λ p . p)$
- $(λ𝑥 .λ𝑦.λ𝑧.𝑥𝑧(𝑦𝑧)) (λ𝑚.λ𝑛.𝑚) (λ𝑝.𝑝)$
  - 取出最左側 $λ𝑥$ 作為目前的 head，應用 $(λ𝑚.λ𝑛.𝑚)$ 參數
- $(λ𝑥. λ𝑦.λ𝑧.𝑥𝑧(𝑦𝑧))(λ𝑚.λ𝑛.𝑚)(λ𝑝.𝑝)$
  - $λ𝑦.λ𝑧.𝑥𝑧(𝑦𝑧)$ 這 body 內的所有 $x$ 都綁定為 $(λ𝑚.λ𝑛.𝑚)$ ，然後去除 head λ𝑥
- $λ𝑦.λ𝑧.𝑥𝑧(𝑦𝑧)$ 中的 $x$ 應用 $(λ𝑚.λ𝑛.𝑚)$ 後，變為 $λ𝑦.λ𝑧.(λ𝑚.λ𝑛.𝑚)𝑧(𝑦𝑧)$
$λ𝑧.(λ𝑚.λ𝑛.𝑚)(𝑧)((λ𝑝.𝑝)𝑧)$ $λ z . (λm . λn . m) (z) ((λ p . p) z)$
- $(λ𝑦 .λ𝑧.(λ𝑚.λ𝑛.𝑚)𝑧(𝑦𝑧)) (λ𝑝.𝑝)$
  - 取出最左側的 $λ𝑦$ 作為目前的 head，應用 $(λ𝑝.𝑝)$ 參數
- $(λ𝑦. λ𝑧.(λ𝑚.λ𝑛.𝑚)𝑧(𝑦𝑧))(λ𝑝.𝑝)$
  - $λ𝑧.(λ𝑚.λ𝑛.𝑚)𝑧(𝑦𝑧)$ 這 body 內的所有 $y$ 都應用 $(λ𝑝.𝑝)$ ，變成 $λ𝑧.(λ𝑚.λ𝑛.𝑚)𝑧((λ𝑝.𝑝)𝑧)$
- 現在最外層的 $z$ 沒有參數可應用，已經是 irreducible，因此往內一層找是否還有可 reduce 的
- 發現可將 $λ𝑚$ 綁定參數 𝑧， $λ𝑛.𝑚$ 內的 $m$ 變成 $z$ ，變成 $(λ𝑛.𝑧)$
$λ𝑧.(λ𝑛.𝑧)((λ𝑝.𝑝)𝑧)$ $λ z . (λn . z) ((λ p . p) z)$
- 可將 $λ𝑛$ 綁定參數 $((λ𝑝.𝑝)𝑧)$
$λ𝑧.𝑧$ $λ z . z$
- 因為 $(λ𝑛.𝑧)$ 的 body $z$ 中沒有變數 $n$ ，所以應用參數 $((λ𝑝.𝑝)𝑧)$ 的結果就是 body $z$ 本身，而參數會被丟棄。因此整個表達式簡化為 $λ𝑧.𝑧$

Evaluation is simplification#

Beta Normal Form#

在 lambda calculus 中有多種 normal forms，此書提到的 normal forms，是指 beta normal form。

beta normal form 的定義是指「表達式中再也不能進行 beta reduction」，也就是不能再 apply lambdas to arguments，可想成「完全求值完畢」，在程式語言中可理解為「程式已完全執行完成」。

用一般數學表達式理解 normal form#

可以用一般的數學式來理解 normal form 是什麼意思，舉例來說，在 $2000/1000$ 這表達式中，/ 已被應用到兩個參數，但還沒有簡化， $2000/1000$ 經過簡化(求值)後會得到 $2$ ，因此 $2000/1000$ 的 normal form 是 $2$ ，因為 $2$ 已經是無法再簡化的值。

換句話說，如果一個函數（如 /）已吃到所有參數（saturated），但沒有化簡成最終結果，那它是「已應用（applied）」，但「未完全求值（not fully evaluated）」。

舉另一個例子 $(10 + 2) * 100 / 2$ ， $(10 + 2) * 100 / 2$ 這數學表達式化簡後會得到 $600$ ， $600$ 已無法再簡化，因此這就是 normal form。

lambda calculus 中的 normal form#

剛剛看了數學表達式的 normal form，來看一下 lambda calculus 中的 normal form。

Identity function $λx.x$ 沒有被應用到任何參數，已經是 normal form。而 $(λx.x)z$ 這就不是 normal form，因為可以進行 beta reduction， $(λx.x)z$ 簡化的下一步是 $[x := z]$ ，最後得到 $z$ ，因此 $(λx.x)z$ 最終 normal form 是 z。

Combinators#

什麼是 Combinator？#

Combinator 指的是沒有自由變數（free variables）的 lambda term，也就是 body 中用到的所有變數都必須在 head 中出現。 Combinator 的用途是用來組合傳入的 arguments，並且它不會引入新的值或外部資料，而這也是「combinator（組合子）」名字的由來。

Combinator 的例子#

以下皆為 combinators，因為 body 中所有變數都被 head 綁定。

$λx.x$
- x 是唯一使用的變數，也在 head 中被綁定，因此無 free variables
$λxy.x$
- body 中只有 x，x 也在 head 裡，符合定義
$λxyz.xz(yz)$
- 變數 x、y、z 全部都在 head 出現，符合定義

非 Combinator 的例子#

以下不是 combinators，因為包含 free variables。

$λy.x$
- y 是 bound variable，但 x 沒有在 head 出現，x 是 free variable，因此這不是 combinator
$λx.xz$
- x 是 bound variable，但 z 沒有在 head 出現，z 是 free variable，因此這不是 combinator

簡單來說，Combinators 是 lambda calculus 中一個特殊類別的表達式，它只使用被提供的 arguments，不依賴外部資料。

Divergence#

不是所有可簡化的 lambda terms 都能得到 normal form#

上面看了很多可以逐步 beta reduction 到 normal form 的範例，但不是所有可簡化的 lambda terms 都能得到 normal form，有些 lambda terms 永遠無法完成 beta reduction，因此無法得到 normal form，這些「永遠無法完成 beta reduction」的 lambda terms 是具有 divergence(發散性) 的。

Divergence（發散）#

Divergence 的意思是 beta reduction 的過程永遠不會終止，也因此不會收斂到 beta normal form。

補充：Convergence 與 Divergence

Convergence（收斂）：最終得到 normal form
Divergence（發散）：永無止境的 reduction

omega：典型發散的 lambda term#

omega 是一個典型發散的 lambda term，Omega 的定義是 $(λx.xx)(λx.xx)$ ，來試跑一次 reduction 流程：

初始表達式為 $(λx.xx)(λx.xx)$
將第一個 $λ$ 的 $x$ 替換為 $(λx.xx)$ ，也就是 $([𝑥 ∶= (λ𝑥.𝑥𝑥)]𝑥𝑥)$
替換完成後得到 $(λx.xx)(λx.xx)$

可發現替換後又回到第一步驟的原點，因此這是無限循環，reduction 過程無法終止，這時就可說此 lambda term 發散（diverges）。

為什麼發散很重要?#

在程式語言中，發散的 terms 等於：

不會產生結果
不會回傳有意義的值

因此理解哪些 lambda 表達式會終止，等於理解哪些程式會真正「做完工作」並回傳答案。

Summary#

簡單列下第一章的 summary 如下。

Functional programming 是基於表達式（expressions）的，包含：
- 變數（variables）
- 常數（constant values）
- 表達式（expressions）之間的組合
- 函數（functions）
函數（Functions）
- Function 由 head 與 body 組成
- Function 是一種可「應用（apply）」到參數並可「簡化（reduce）」到最終結果的表達式
變數（Variables）
- 變數可被函數的 head 綁定（bound）
- 在 body 中，只要是 bound variable，每一次出現都代表相同的值
Function 的統一特徵
- 所有 Function 只接受一個參數，只回傳一個結果
- Function 是「輸入集合 → 輸出集合」的映射(mapping)
  - 同樣的輸入，永遠得到同樣的輸出
與 Haskell 的關係
- 上述規則同樣適用於 Haskell
- 語義上，Haskell 就是一個 lambda calculus
- 實際上，Haskell 是 typed lambda calculus（有型別的 lambda calculus），核心語義仍與 lambda calculus 相同
Haskell 程式的意義
- Haskell 程式的意義來自求值 expressions（evaluating expressions），而不是像命令式語言那樣執行指令（雖然 Haskell 也有機制來執行指令）

最後書中有列一些進階讀物，也一併列上來提供大家參考~

Raul Rojas. A Tutorial Introduction to the Lambda Calculus.
- http://www.inf.fu-berlin.de/lehre/WS03/alpi/lambda.pdf
Henk Barendregt and Erik Barendsen. Introduction to Lambda Calculus.
- http://www.cse.chalmers.se/research/group/logic/TypesSS05/Extra/geuvers.pdf
Jean-Yves Girard, P. Taylor, and Yves Lafon. Proofs and Types.
- http://www.paultaylor.eu/stable/prot.pdf

如有任何問題歡迎聯絡、不吝指教✍️