（在這個帖子的原始版本里，我試圖用一個JavaScript工具來生成MathML。但不太順利：有幾個瀏覽器沒法正確的渲染，在RSS feed里也顯示的不好。所以我只好從頭開始，用簡單的文本格式重新寫一遍。）
計算機科學，尤其是編程語言，經常傾向於使用一種特定的演算：Lambda演算（Lambda Calculus）。這種演算也廣泛地被邏輯學家用於學習計算和離散數學的結構的本質。Lambda演算偉大的的原因有很多，其中包括：
- 非常簡單。
- 圖靈完備。
- 容易讀寫。
- 語義足夠強大，可以從它開始做（任意）推理。
- 它有一個很好的實體模型。
- 容易創建變種，以便我們探索各種構建計算或語義方式的屬性。
Lambda演算易於讀寫，這一點很重要。它導致人們開發了很多極為優秀的編程語言，他們在不同程度上都基於Lambda演算：LISP，ML和Haskell語言都極度依賴於Lambda演算。
Lambda演算建立在函數的概念的基礎上。純粹的Lambda演算中，一切都是函數，連值的概念都沒有。但是，我們可以用函數構建任何我們需要的東西。還記得在這個博客的初期，我談了一些關於如何建立數學的方法么？ 我們可以從無到有地用Lambda演算建立數學的整個結構。
閑話少說，讓我們深入的看一看LC（Lambda Calculus）。對於一個演算，需要定義兩個東西：語法，它描述了如何在演算中寫出合法的表達式；一組規則，讓你符號化地操縱表達式。
Lambda演算的語法
Lambda演算只有三類表達式：
- 函數定義：Lambda演算中的函數是一個表達式，寫成：
lambda x . body，表示“一個參數參數為x的函數，它的返回值為body的計算結果。” 這時我們說：Lambda表達式綁定了參數x。 - 標識符引用（Identifier reference）：標識符引用就是一個名字，這個名字用於匹配函數表達式中的某個參數名。
- 函數應用（Function application）：函數應用寫成把函數值放到它的參數前面的形式，如
(lambda x . plus x x) y。
柯里化
在Lambda演算中有一個技巧：如果你看一下上面的定義，你會發現一個函數（Lambda表達式）只接受一個參數。這似乎是一個很大的局限 —— 你怎么能在只有一個參數的情況下實現加法？
這一點問題都沒有，因為函數就是值。你可以寫只有一個參數的函數，而這個函數返回一個帶一個參數的函數，這樣就可以實現寫兩個參數的函數了——本質上兩者是一樣的。這就是所謂的柯里化（Currying），以偉大的邏輯學家Haskell Curry命名。
例如我們想寫一個函數來實現x + y。我們比較習慣寫成類似：lambda x y . plus x y之類的東西。而采用單個參數函數的寫法是：我們寫一個只有一個參數的函數，讓它返回另一個只有一個參數的函數。於是x + y就變成一個單參數x的函數，它返回另一個函數，這個函數將x加到它自己的參數上：
lambda x. ( lambda y. plus x y )
現在我們知道，添加多個參數的函數並沒有真正添加任何東西，只不過簡化了語法，所以下面繼續介紹的時候，我會在方便的時候用到多參數函數。
自由標識符 vs. 綁定標識符
有一個重要的語法問題我還沒有提到：閉包（closure）或者叫完全綁定（complete binding）。在對一個Lambda演算表達式進行求值的時候，不能引用任何未綁定的標識符。如果一個標識符是一個閉合Lambda表達式的參數，我們則稱這個標識符是（被）綁定的；如果一個標識符在任何封閉上下文中都沒有綁定，那么它被稱為自由變量。
lambda x . plus x y：在這個表達式中，y和plus是自由的，因為他們不是任何閉合的Lambda表達式的參數；而x是綁定的，因為它是函數定義的閉合表達式plus x y的參數。lambda x y . y x：在這個表達式中x和y都是被綁定的，因為它們都是函數定義中的參數。lambda y . (lambda x . plus x y)：在內層演算lambda x . plus x y中，y和plus是自由的，x是綁定的。在完整表達中，x和y是綁定的：x受內層綁定，而y由剩下的演算綁定。plus仍然是自由的。
我們會經常使用free(x)來表示在表達式x中自由的標識符。
一個Lambda演算表達式只有在其所有變量都是綁定的時候才完全合法。但是，當我們脫開上下文，關注於一個復雜表達式的子表達式時，自由變量是允許存在的——這時候搞清楚子表達式中的哪些變量是自由的就顯得非常重要了。
Lambda演算運算法則
Lambda演算只有兩條真正的法則：稱為Alpha和Beta。Alpha也被稱為「轉換」，Beta也被稱為「規約」。
Alpha轉換
Alpha是一個重命名操作; 基本上就是說，變量的名稱是不重要的：給定Lambda演算中的任意表達式，我們可以修改函數參數的名稱，只要我們同時修改函數體內所有對它的自由引用。
所以 —— 例如，如果有這樣一個表達式：
lambda x . if (= x 0) then 1 else x ^ 2
我們可以用Alpha轉換，將x變成y（寫作alpha[x / y]），於是我們有：
lambda y . if (= y 0) then 1 else y ^ 2
這樣絲毫不會改變表達式的含義。但是，正如我們將在后面看到的，這一點很重要，因為它使得我們可以實現比如遞歸之類的事情。
Beta規約
Beta規約才是精彩的地方：這條規則使得Lambda演算能夠執行任何可以由機器來完成的計算。
Beta基本上是說，如果你有一個函數應用，你可以對這個函數體中和對應函數標識符相關的部分做替換，替換方法是把標識符用參數值替換。這聽起來很費解，但是它用起來卻很容易。
假設我們有一個函數應用表達式：“ (lambda x . x + 1) 3 “。所謂Beta規約就是，我們可以通過替換函數體（即“x + 1”）來實現函數應用，用數值“3”取代引用的參數“x”。於是Beta規約的結果就是“3 + 1”。
一個稍微復雜的例子：(lambda y . (lambda x . x + y)) q。 這是一個挺有意思的表達式，因為應用這個Lambda表達式的結果是另一個Lambda表達式：也就是說，它是一個創建函數的函數。這時候的Beta規約，需要用標識符“q”替換所有的引用參數“y”。所以，其結果是“ lambda x . x + q “。
再給一個讓你更不爽的例子：“ (lambda x y. x y) (lambda z . z * z) 3 “。這是一個有兩個參數的函數，它(的功能是)把第一個參數應用到第二個參數上。當我們運算時，我們替換第一個函數體中的參數“x”為“lambda z . z * z “；然后我們用“3”替換參數“y”，得到：“ (lambda z . z * z) 3 “。 再執行Beta規約，有“3 * 3”。
Beta規則的形式化寫法為：
lambda x . B e = B[x := e] if free(e) subset free(B[x := e])
最后的條件“if free(e) subset free(B[x := e])”說明了為什么我們需要Alpha轉換：我們只有在不引起綁定標識符和自由標識符之間的任何沖突的情況下，才可以做Beta規約：如果標識符“z”在“e”中是自由的，那么我們就需要確保，Beta規約不會導致“z”變成綁定的。如果在“B”中綁定的變量和“e”中的自由變量產生命名沖突，我們就需要用Alpha轉換來更改標識符名稱，使之不同。
例子更能明確這一點：假設我們有一個函數表達式，“ lambda z . (lambda x . x + z) “，現在，假設我們要應用它：
(lambda z . (lambda x . x + z)) (x + 2)
參數“(x + 2)”中，x是自由的。現在，假設我們不遵守規則直接做Beta規約。我們會得到：
lambda x . x + x + 2
原先在“x + 2”中自由的的變量現在被綁定了。再假設我們應用該函數：
(lambda x . x + x + 2) 3
通過Beta規約，我們會得到“3 + 3 + 2”。
如果我們按照應有的方式先采用Alpha轉換，又該如何？
- 由
alpha[x/y]有:(lambda z . (lambda y . y + z)) (x + 2) - 由Beta規約：
(lambda y . y + x + 2) 3 - 再由Beta規約：
3 + x + 2。
“3 + x + 2”和“3 + 3 + 2”是非常不同的結果！
規則差不多就是這些。還有另外一個規則，你可以選擇性地加一條被稱為Eta-規約的規則，不過我們將跳過它。 我在這里描述了一個圖靈完備 —— 完整有效的計算系統。 要讓它變得有用，或看它如何用來做些有實際意義的事情，我們還需要定義一堆能讓我們做數學計算的基本函數，條件測試，遞歸等，我將在下一篇文章討論這些。
我們也還沒有定義Lambda-演算的模型呢。（原作者在這里和這里討論了模型的概念。）模型實際上是非常重要的！邏輯學家們在擺弄了LC好幾年之后，才為其想出一個完整的模型，這是件非常重要的事情，因為雖然LC看起來是正確的，但在早期為它定義一個模型的嘗試，卻是失敗的。畢竟，請記住，如果沒有一個有效的模型，這意味着該系統的結果是毫無意義的！
http://cgnail.github.io/academic/lambda-1/