{%hackmd @YuRen-tw/article-theme %}
# 啥物是 Lambda Calculus

## 話頭

Lambda calculus 是數學家 Alonzo Church 發表出來的，是用替換規則來稽考函數的一个形式系統。
原底 lambda calculus 干焦是欲用來研究數學的基礎，毋過後來咱發現伊有真濟袂䆀的應用，所以佇這馬的計算機科學（computer science）、邏輯學甚至是語言學攏會使看著伊的身影。
尤其是這幾冬，有愈來愈濟寫程式的人認捌著講函數型程式設計（functional programming）的理路是誠有智慧，寫 FP 袂輸一件蓋奅的代誌，lambda calculus 嘛綴咧出現佇逐家的面頭前。

雖然伊名後壁的 calculus 佮微積分仝名，無過莫予伊嚇驚著。
lambda calculus 無啥物複雜的運算，嘛無啥物恐怖的符號，干焦一點仔替換規則。
咱佇這篇文內底會對數學函數的概念開始，簡單、直覺的紹介 lambda calculus。

## 函數

咱凡勢攏捌佇咧高中的數學課學著一點仔函數的概念：咱通共函數當做一个機器，予伊一个物件，經過機器運作了後變做另外一个物件予咱。
咱予函數的物件號做「自變數（independent variable）」，伊應轉來予咱的物件號做「應變數（dependent variable）」。
假使這个函數的名是 $f$，咱就用 $f(x)$ 來代表咱予伊 $x$ 了後的應變數，讀做「$f$ of $x$」。

比論講有一个函數號做 $g$，予伊 $3$ 伊就應 $30$、予伊 $12$ 伊就應 $120$。
就是隨在咱予 $g$ 啥物數字 $n$，伊攏應這个數字的 $10$ 倍。
咱就通寫做 \\[ g(n) = 10n \\] 讀做「$g$ of $n$ 平平 $10n$」。
佇數學文獻內底，咱嘛定定會共寫做 \\[ g\!: n \longmapsto 10n \\] 讀做「$g$ 共 $n$ 映到 $10n$」。
若共函數內底的對應關係像按呢共寫起來，欲知影這个函數會按怎應就簡單矣。
比論講欲知影 $g(23)$ 是偌濟，咱就共正手邊的 $n$ 換做 $23$，所以 $g(23)$ 就是 $10 \times 23$，平平 $230$。
咱佇這篇文內底共這款「共 $x$ 替換作 $a$」的操作寫做 $[a/x]$，那按呢拄才咧計算 $g(23)$ 的步數就會寫做 \\[ g(23) = 10n[23/n] = 10 \times 23 = 230. \\]

毋管是佗一種寫法，咱攏會用一个「抽象」的符號（親像頭前的 $n$）來代表自變數；若應變數內底有佮自變數對應的符號，欲來「應用」這个函數的時陣（親像頭前欲算 $g(23)$），咱就共彼寡符號攏「替換」做欲予伊的物件（親像頭前的 $[23/n]$）就好矣。
嘛是因為寫按呢了後，自變數的符號會含佇咧應變數內底，清國的數學家李善蘭就共應變數號做「函數」（「函」是「包含」的意思），隨著數學的發展，這个名慢慢仔嘛變做今仔日代表規个對應的用法。

> :::spoiler 李善蘭《代微積拾級》〈凡例〉
> 一、諸數字之旨各異。函數者，言其數中函元之加、減、乘、約、開方、自乘諸數也；長數者，言幾何漸增漸減之微數也；變數者，言其數或漸變大、或漸變小、非一定之數也；常數者，言其數一定不變也。
> :::

> :::spoiler 李善蘭《代微積拾級》〈卷十　微分一〉
> 凡此變數中函彼變數，則此為彼之函數。如直線之式為 $地 = 甲天 \mathop{丄} 乙$，則地為天之函數。又平圜之式為 $地 = \sqrt{味^二 \mathop{丅} 天^二}$、橢圜之式為……，皆地為天之函數也。
> |漢字|天|地|甲|乙|味|丄|丅|
> |:-:|:-:|:-:|:-:|:-:|:-:|:-:|:-:|
> |**意義**|`x`|`y`|`a`|`b`|`R`|`+`|`-`|
> :::

數學發展到這馬，會當叫做函數（function）的物件早就毋是干焦頭前寫的彼款爾矣。
佇今仔日的數學內底，任何的對應關係，只要伊袂一个應兩三个，按呢伊就通號做是函數，比論下跤的 $\psi$ 嘛是函數： \\[
\psi(x) = \begin{cases}
1, &\text{若是講 $x$ 是素數；} \\
0, &\text{若是講 $x$ 毋是素數。}\\
\end{cases}
\\]
這个 $\psi$ 就較僫寫做進前啥物應變數內底有自變數的彼款矣。
雖然按呢寫起來是真方便，毋過咱若欲看這个 $\psi$ 到底會按怎應，就無遐直接矣。
比論講，咱若欲知影 $\psi(2117)$ 是啥，就愛先去檢查講 $2117$ 敢是素數：$2117 = 29 \times 73$ 毋是素數，所以 $\psi(2117) = 0$。

就是講，若對「計算」的角度來看，咱較有法度來研究的，凡勢干焦上頭前彼種有明確的符號照步來予咱替換、運算的函數爾爾矣。
所以，為著欲單純研究彼款通替換的函數，美國數學家 Alonzo Church 就提出了 lambda calculus 這款系統，專門來操作「抽象」、「應用」、「替換」。
續落來咱就來看講啥物是 lambda calculus。

## 啥物是 Lambda？
### Lambda 的定義

咱這馬要緊的操作是「抽象」（abstraction）、「應用」（application）、「替換」（substitution）。
比論用進前的數學寫法，咱會當按呢表達定義佮使用一个函數：
\begin{align}
\text{抽象}\quad & f\!: x \longmapsto 3x+5\\
\text{應用}\quad & f(10)
\end{align}
Lambda 的寫法其實差無偌濟，會當講是換一个寫法爾爾。
比論講拄才的就寫做
\begin{align}
\text{抽象}\quad & f = \lambda x. 3x+5\\
\text{應用}\quad & f\ 10
\end{align}
就是講，應用是免括號的；啊抽象的時陣，代表自變數的符號囥佇 $\lambda$ 佮 $.$ 的中央，代表應變數的部分囥佇 $.$ 的後壁。
咱若無想欲共這个函數號名，$f\ 10$ 嘛會使直接寫做 $(\lambda x. 3x+5)\ 10$。

咱欲操作的這款物件號做「lambda 項」，伊是按呢定義：
- 【變數】咱有一堆符號 $\{x, y, \ldots\}$，內底的任何一个符號攏通算是一个 lambda 項；
- 【抽象】若講 $x$ 是咱的符號、$M$ 是一个 lambda 項，按呢 $\lambda x. M$ 嘛是一个 lambda 項；
- 【應用】若講 $N$ 佮 $M$ 攏是 lambda 項，按呢 $N\ M$ 嘛是一个 lambda 項；
- 若有需要，通添括號 $()$ 予咱的表達閣較清楚；
- 為著表達方便，會當共一寡物件當做 lambda 項罔用，比論講數字 $3$、運算 $x+y$。

照按呢定義，下跤的攏是合法的 lambda 項：
| $x$ | $x\ x$ | $\lambda x. x$ |
|:---|:---|:---|
| $x\ y$ | $(x\ y)\ z$ | $x\ (y\ z)$ |
| $\lambda x. y$ | $\lambda x. (\lambda y. x)$ | $\lambda x. (x\ y)$ |
| $(\lambda x. x)\ y$ | $x\ (\lambda y. y)$ | $(\lambda x. x)\ (\lambda y. y)$ |

為著方便咱寫，咱閣有一寡寫法的約定：
- 應用是「對倒爿結合（left-associative）」的，就是講 $L\ M\ N$ 是代表 $(L\ M)\ N$；
- 抽象的範圍是 $\lambda - .$ 後壁（佮伊仝一個括號內底的）規句，就是講
- $\lambda x. M\ N$ 代表 $\lambda x. (M\ N)$；
- $(\lambda x. M)\ N$ 的括號袂當省；
- $\lambda x. \lambda y. M$ 會當直接寫 $\lambda x\,y. M$。

### $\alpha$ 變換

函數內底的符號干焦是佇咱咧應用的時陣予咱參考的對象爾爾，符號是選 $x$ 抑是選 $y$ 根本無差別。
這代表講咱嘛會使改變 lambda 項的符號，只要改了袂影響伊的函數意義就好，比論講 $\lambda x. y\ x$ 會當改做 $\lambda z. y\ z$。
愛注意的是，咱逐擺改符號攏是改規組抽象結構 $(\lambda\cdots)$ 內底的符號。
這款改符號的變換其實嘛有嚴格的定義，號做「$\alpha$ 變換」，毋過彼攏是為著欲予這套 lambda calculus 系統閣較完整，毋免去依賴函數意義。
其實咱簡單對函數改參考符號的意義來理解就會用得矣。

### $\beta$ 簡化

欲算「應用」的時佮函數仝款，若欲算 $(\lambda x. M)\ N$，結果就是做「替換」 $M[N/x]$，共應變數 $M$ 內底佮自變數 $x$ 對應的符號替換做 $N$。
愛注意的是，咱袂使直接共所有仝款的符號替換掉，愛先檢查講伊敢真正有予自變數縛牢。
比論講 $(\lambda \color{red}{x}.(\lambda \color{green}{x}. \color{green}{x}+1)\ (\color{red}{x}+1))\ 3$ 欲算上外口應用 $3$ 的部分，是愛算做 $(\lambda x. x+1)\ 4$，毋通算做是 $(\lambda x. 4)\ 4$。
咱若欲避免無細膩替換毋著的狀況，會當先透過 $\alpha$ 變換共每一个 $\lambda$ 後壁的符號換作全部攏無仝了後才來算。
應用的時陣到底欲按怎替換嘛有嚴格的定義，號做「$\beta$ 簡化」，毋過仝款是為著欲予系統閣較完整爾爾，咱嘛會使直接對函數意義去理解。

凡勢有人看到遮就會問講，像頂頭的 $(\lambda \color{red}{x}.(\lambda \color{green}{x}. \color{green}{x}+1)\ (\color{red}{x}+1))\ 3$ 有兩个應用結構，按呢到底是愛先應用外口的 $(\lambda \color{red}{x}. \cdots)\ 3$ 抑是內底的 $(\lambda \color{green}{x}. \color{green}{x}+1)\ (\color{red}{x}+1)$ 才著？
其實，咱欲選佗一个代先算攏無要緊，Church–Rosser 定理共咱講選佗一个結果攏仝款。
\begin{align}
&(\lambda \color{red}{x}.(\lambda \color{green}{x}. \color{green}{x}+1)\ (\color{red}{x}+1))\ 3\\[4pt]
&\hspace{-2em}\text{共符號攏換無仝}\\[4pt]
&\ \equiv_\alpha\ %
(\lambda \color{red}{x}.(\lambda \color{green}{y}. \color{green}{y}+1)\ (\color{red}{x}+1))\ 3\\[7pt]
&\hspace{-2em}\text{若是外口的 $\color{red}{x}$ 先應用}\\[4pt]
&\ \xrightarrow{[3/\color{red}{x}]}_\beta\ %
(\lambda \color{green}{y}. \color{green}{y}+1)\ 4
\ \xrightarrow{[4/\color{green}{y}]}_\beta\ %
5\\[7pt]
&\hspace{-2em}\text{若是內底的 $\color{green}{y}$ 先應用}\\[4pt]
&\ \xrightarrow{[(\color{red}{x}+1)/\color{green}{y}]}_\beta\ %
(\lambda \color{red}{x}. \color{red}{x}+2)\ 3
\ \xrightarrow{[3/\color{red}{x}]}_\beta\ %
5
\end{align}

## 啥物攏是 Lambda

猶未寫完…