最近比較閑，打算整理一下之前學習的關於程序語言的知識。主要的內容其實就是一邊設計程序語言一邊寫解釋器實現它。這些知識基本上來自Programming Languages and Lambda Calculi和Essentials of Programming Languages這兩本書。
我還記得高中奧數競賽培訓時的老師這樣說過：“解題時一定要抓住定義。” 編程和解題一樣，也要抓住定義。 所以在寫解釋器前，得先定義好這門要解釋的程序語言。 這門程序語言基於Lambda演算。
從\(\lambda\)演算講起
真不想講\(\lambda\)演算……算了，還是簡要說明一下。\(\lambda\)演算之於程序語言中的地位好比集合論之於數學。正如每一本數學教材，都要從集合論開始； 每一本程序語言教材，也要從\(\lambda\)演算講起。 不過話說回來，追根溯源\(\lambda\)演算也是從集合論搭起來。 咱就不走那么遠了，又累又沒什么意思……
\(\lambda\)演算中的基本類型只有變量和函數兩種。 變量用大寫字母\(X\)表示。 像\(a,b,x,y,abc,...\)都是變量。 一個函數包含兩個元素： 一個是函數參數（形參），它是一個變量； 另一個元素是函數體，它是一個\(\lambda\)演算表達式（這里是遞歸定義）。 用(lambda X M)表示一個函數， 其中X是一個變量，M是一個\(\lambda\)演算表達式（ 別吐槽參數X那里少了個括號。 ）。 為了描述的簡潔，也用\(\lambda X.M\)表示一個函數。
舉個例子，\(\lambda x.x\)是一個恆等函數\(f(x) = x\)。 在數學上一般用\(f(a)\)表示函數調用，\(a\)是實參。 在\(\lambda\)演算中把函數也放入括號，記為\((\lambda x.x \; a)\)。 函數調用的計算方法是在函數體中用實參替換形參。 在這個例子里\((\lambda x.x \; a) = a\)。 這個計算過程稱為歸約。
\(\lambda\)演算的函數都只包含一個參數。 如果要使用多參函數，可以用多個函數嵌套。 下面是一個例子： \[ \lambda x.\lambda y.(x \; y) \] 這種技巧被稱作currying。
從上面的討論看出，\(\lambda\)演算只包含三種表達式。 形式化地定義\(\lambda\)演算的語法如下： \begin{eqnarray*} M, N, L &=& X \\ &|& \lambda X.M \\ &|& (M \; N) \end{eqnarray*} 這里用大寫字母\(M\)、\(N\)和\(L\)代表\(\lambda\)演算的表達式， 這是個遞歸定義，第二行、第三行出現了\(M\)和\(N\)。 第三行表達式是一個函數調用，一般要求處於函數位置的\(M\)應該要能歸約成一個函數，否則歸約就沒法進行下去啦。
下面給出幾個\(\lambda\)演算的表達式的例子： \begin{eqnarray*} & x \\ & \lambda x.x \\ & (\lambda x.x \; y) \\ & (\lambda x.(x \; x) \; \lambda x.x) \\ & (\lambda x.(x \; x) \; \lambda x.(x \; x)) \end{eqnarray*}
\(\lambda\)演算的歸約依賴於替換操作。 在介紹替換操作之前還得先介紹自由變量。
自由變量
考察一個表達式：\((\lambda x.(\lambda x.x \; x) \; a)\)。 這個表達式歸約到\((\lambda x.x \; a)\)。 可以看到，在\(\lambda x.(\lambda x.x \; x)\)函數體\((\lambda x.x \; x)\)中參數位置的變量\(x\)和\(\lambda x.x\)中點后面的\(x\)是不一樣的。 參數位置中的\(x\)被替換成\(a\)，而\(\lambda x.x\)中點后面的\(x\)沒有被替換。 被替換的\(x\)稱為表達式\((\lambda x.x \; x)\)的自由變量。 在函數調用的替換過程中只有自由變量會被替換。
自由變量指一個表達式中沒有受到約束的變量。 約束指這個變量不是作為某個函數的參數而存在。 如表達式\(\lambda x.(f x)\)中\(f\)是自由變量，\(x\)不是自由變量。 用\(FV(M)\)表示表達式\(M\)中的所有自由變量的集合。
從這里開始，描述和\(\lambda\)演算有關的一些定義和算法將遵循\(\lambda\)演算的語法定義。 所以計算\(FV(M)\)的算法（也是\(FV(M)\)的精確定義）應該分成變量、函數和函數調用三種情況討論： \begin{eqnarray*} FV(X) &=& \{X\} \\ FV(\lambda X.M) &=& FV(M) \backslash \{X\} \\ FV((M \; N)) &=& FV(M) \cup FV(N) \end{eqnarray*}
替換
用記號\(M[X \leftarrow N]\)表示在表達式\(M\)中將自由變量\(X\)（如果有出現這個自由變量）替換成表達式\(N\)。 更准確的定義如以下公式： \begin{eqnarray*} X_1[X_1 \leftarrow N] &=& N \\ X_2[X_1 \leftarrow N] &=& X_2 \\ &&其中X_1 \neq X_2 \\ (\lambda X_1.M)[X_1 \leftarrow N] &=& (\lambda X_1.M) \\ (\lambda X_1.M)[X_2 \leftarrow N] &=& (\lambda X_3.M[X_1 \leftarrow X_3][X_2 \leftarrow N]) \\ &&其中X_1 \neq X_2, X_3 \notin FV(N), X_3 \notin FV(M)\backslash\{X_1\} \\ (M_1 \; M_2)[X \leftarrow N] &=& (M_1[X \leftarrow N] \; M_2[X \leftarrow N]) \end{eqnarray*} 第四個公式看着比較復雜，其實是為了避免\(N\)中有自由變量\(X_1\)這種情況。 舉個例子，\(\lambda x.y[y \leftarrow (x x)]\)應該替換為\(\lambda z.(x x)\)。 如果替換成\(\lambda x.(x x)\)就不對了。
如果\(N\)中沒有自由變量\(X_1\)，那么這個公式可以簡化成： \begin{eqnarray*} (\lambda X_1.M)[X_2 \leftarrow N] = (\lambda X_1.M[X_2 \leftarrow N]) \end{eqnarray*}
歸約
所謂歸約，可以理解成求值，或者表達式化簡（初中好像有學過代數表達式化簡）。 \(\lambda\)演算有三種歸約方法。 三種歸約分別稱為\(\alpha\)歸約，\(\beta\)歸約和\(\eta\)歸約。 名字看着很滲人，不表示這三種歸約難以理解，只說明命名的人沒有一顆愛玩的心。
- \(\alpha\)歸約的意思是，函數參數變量的變量名是什么無關緊要。 比如\(\lambda x.x\)和\(\lambda y.y\)表示的同一個函數。 這個歸約很基本，但是幾乎上不會被用到就是的了。 \[ \lambda X_1.M \rightarrow_\alpha \lambda X_2.M[X_1 \leftarrow X_2] \quad \text{其中}X_2 \notin FV(M)\]
- \(\beta\)歸約表示了函數調用過程，是最常用的歸約。 \(\beta\)歸約用函數調用的輸入參數（實參）替換函數體中出現的參數變量（形參）： \[ (\lambda X.M \; N) \rightarrow_\beta M[X \leftarrow N] \]
- \(\eta\)歸約指： \[ \lambda X.(M \; X) \rightarrow_\eta M \quad \text{其中}X \notin FV(M)\] 這個有點怪，但仔細想想不難理解。
一個解釋器的作用是輸入一個表達式，輸出該表達式歸約到最簡（不能再\(\beta\)歸約）的形式。 一般我們是希望這個最簡形式能夠是一個變量（\(X\)）或者一個函數（\(\lambda X.M\)），因為函數調用是用來讓人進行\(\beta\)歸約的。 變量，或者函數，被稱為“值”。 但是也有些壞掉了的表達式像\((x \; x)\)，由於\(x\)是個變量而非函數，這個表達式沒法再歸約。 通常這種表達式被認為非法的表達式。 如果輸出這種結果就表示輸入程序有誤，程序崩潰。 另外有些表達式不能歸約到某種最簡形式，也就是無限循環（可憐的西西弗斯）。 無限循環的一個經典例子是這個輸入：\((\lambda x.(x \; x) \; \lambda x.(x \; x))\)。
一個解釋器，給它一個輸入，它會有以下三種情況：
- 輸出一個值:-)
- 崩潰XD
- 無限循環@_@
呼！總算寫完。