【逻辑与计算理论】Lambda 演算——开篇
原文來自Good Math/Bad Math的系列連載，全文分7章，本篇是第1章。中文博客負暄瑣話對這個系列的前6章做過翻譯，強迫癥表示忍受不了「下面沒有了」，于是自己動手做了全套。這里只對原文做了翻譯，而“負暄瑣話”的版本則加上了很多掌故，使得閱讀起來更有趣味性。
| Good Math, Bad Math | Lambda演算系列之七 |
（在這個帖子的原始版本里，我試圖用一個JavaScript工具來生成MathML。但不太順利：有幾個瀏覽器沒法正確的渲染，在RSS feed里也顯示的不好。所以我只好從頭開始，用簡單的文本格式重新寫一遍。）
?
我的最愛Lambda演算——開篇
計算機科學，尤其是編程語言，經常傾向于使用一種特定的演算：Lambda演算（Lambda Calculus）。這種演算也廣泛地被邏輯學家用于學習計算和離散數學的結構的本質。Lambda演算偉大的的原因有很多，其中包括：
- 非常簡單。
- 圖靈完備。
- 容易讀寫。
- 語義足夠強大，可以從它開始做（任意）推理。
- 它有一個很好的實體模型。
- 容易創建變種，以便我們探索各種構建計算或語義方式的屬性。
Lambda演算易于讀寫，這一點很重要。它導致人們開發了很多極為優秀的編程語言，他們在不同程度上都基于Lambda演算：LISP，ML和Haskell語言都極度依賴于Lambda演算。
Lambda演算建立在函數的概念的基礎上。純粹的Lambda演算中，一切都是函數，連值的概念都沒有。但是，我們可以用函數構建任何我們需要的東西。還記得在這個博客的初期，我談了一些關于如何建立數學的方法么？ 我們可以從無到有地用Lambda演算建立數學的整個結構。
閑話少說，讓我們深入的看一看LC（Lambda Calculus）。對于一個演算，需要定義兩個東西：語法，它描述了如何在演算中寫出合法的表達式；一組規則，讓你符號化地操縱表達式。
Lambda演算的語法
Lambda演算只有三類表達式：
柯里化
在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看起來是正確的，但在早期為它定義一個模型的嘗試，卻是失敗的。畢竟，請記住，如果沒有一個有效的模型，這意味著該系統的結果是毫無意義的！
?
阿隆佐.丘奇的天才之作——lambda演算中的數字
所以，現在，讓我們用lambda演算干點有趣的事。首先，為了方便起見，我將介紹些語法糖（syntactic sugar）來命名函數，以便下面遇到某些復雜的事情的時候方便我們閱讀。
引進「全局」函數（即在我寫的這些所有的關于lambda演算的介紹里都可以直接使用，而不用在每一個表達式中都聲明一次這個函數的辦法），我們將使用“let”表達式：
let square = lambda x . x ^ 2這條表達式聲明了一個名為“square”的函數，其定義是lambda x . x ^ 2。如果我們有“?square 4”，則上面的“let”表達式的等效表達式為：
(lambda square . square 4) (lambda x . x ^ 2)某些例子中，我使用了數字和算術運算。但數字并不真正存在于lambda演算中，我們有的只有函數！因此，我們需要發明某種使用函數來創建數字的方式。幸運的是，邱奇（Alonzo Church），這個發明了lambda演算的天才，找出了做到這一點的辦法。他的函數化的數字的版本被稱為丘奇數（Church Numerals）。
所有的丘奇數都是帶有兩個參數的函數：
- 0是“?lambda s z . z?“。
- 1是“?lambda s z . s z?“。
- 2是“?lambda s z . s (s z)
- 對于任何數“n”，它的丘奇數是將其第一個參數應用到第二個參數上“n”次的函數。
一個很好的理解辦法是將“z”作為是對于零值的命名，而“s”作為后繼函數的名稱。因此，0是一個僅返回“0”值的函數；1是將后繼函數運用到0上一次的函數；2則是將后繼函數應用到零的后繼上的函數，以此類推。
現在看好了，如果我們想要做加法，x + y，我們需要寫一個有四個參數的函數；兩個需要相加的數字；以及推導數字時用到的“s”和“z”：
let add = lambda s z x y . x s (y s z)讓我們將其柯里化，看看是怎么回事。首先，它接受兩個參數，這是我們需要做加法的兩個值；第二，它需要正則化（normalize）這兩個參數，以使它們都使用對0（z）和后繼值（s）的綁定（即，將參數都寫成s和z的組合的形式）。
let add = lambda x y . (lambda s z . (x s (y s z)))看下這個式子，它說的是，為了將x和y相加，先用參數“s”和“z”創建（正則化的）丘奇數“y”。然后應用x到丘奇數y上，這時候使用由“s”和“z”定義的丘奇數y。也就是說，我們得到的結果是一個函數，這個函數把自己加到另一個數字上。（要計算x + y，先計算?y?是?z?的幾號后繼，然后計算x?是?y的幾號后繼。）
讓我們再進一步看看2 + 3的運算過程：
add (lambda s z . s (s z)) (lambda s z . s (s (s z))) news newz為了更容易理解，對數字2和3做alpha變換，“2”用“s2”和“z2”代替，3用“s3”和“z3”代替：
add (lambda s2 z2 . s2 (s2 z2)) (lambda s3 z3 . s3 (s3 (s3 z3)))用add的定義做替換：
(lambda x y .(lambda s z. (x s y s z))) (lambda s2 z2 . s2 (s2 z2)) (lambda s3 z3 . s3 (s3 (s3 z3)))對add做beta規約：
lambda s z . (lambda s2 z2 . s2 (s2 z2)) s (lambda s3 z3 . s3 (s3 (s3 z3)) s z)然后beta規約丘奇數”3”。這步操作其實是“正則化”3：把數字3的定義里的后繼函數和零函數替換成add的參數列表里的后繼函數和零函數：
lambda s z . (lambda s2 z2 . s2 (s2 z2)) s (s (s (s z)))現在，到了最精妙的一步了。再對丘奇數”2”做beta規約。我們知道：2是一個函數，它接受兩個參數：一個后繼函數和0(函數)。于是，要相加2和3，我們用后繼函數應用到2的第一個參數；用3的運算結果應用到第二個參數（0函數）！
lambda s z . s (s (s (s (s z))))于是，我們的結果是：丘奇數”5”！
?
Lambda演算中的布爾值和選擇
現在，我們在lambda演算中引入了數字，只差兩件事情就可以表達任意計算了：一個是如何表達選擇（分支），另一個是如何表示重復。在這篇文章中，我將討論布爾值和選擇，下一篇將介紹重復和遞歸。
我們希望能夠寫出形如?if / then / else語句的表達式，就像我們在大多數編程語言做的那樣。繼像丘奇數那樣將數字表示為函數之后，我們也將true和false值表示為對其參數執行一個if-then-else操作的函數：
let TRUE = lambda x y . x let FALSE = lambda x y . y于是，現在我們可以寫一個“if”函數，它的第一個參數是一個條件表達式，第二個參數是如果條件為真時才進行運算的表達式，第三個參數則如果條件為假時要進行的運算。
let IfThenElse = lambda cond true_expr false_expr . cond true_expr false_expr此外我們還需要定義常用的邏輯運算：
let BoolAnd = lambda x y . x y FALSE let BoolOr = lambda x y. x TRUE y let BoolNot = lambda x . x FALSE TRUE現在，就讓我們過一遍這些定義。讓我們先看看BoolAnd：
- BoolAnd TRUE FALSE，展開TRUE和FALSE定義：BoolAnd (lambda x y . x) (lambda x y . y)
- alpha變換true和false：BoolAnd (lambda xt yt . xt) (lambda xf yf . yf)
- 現在，展開BoolAnd：(lambda x y. x y FALSE) (lambda xt yt . xt) (lambda xf yf . yf)
- beta規約：(lambda xt yt.xt) (lambda xf yf. yf) FALSE
- 再次beta規約：(lambda xf xf . yf)
于是我們得到結果：BoolAnd TRUE FALSE = FALSE。再讓我們來看看BoolAnd FALSE TRUE：
- BoolAnd (lambda x y . y) (lambda x y .x)
- alpha變換：BoolAnd (lambda xf yf . yf) (lambda xt yt . xt)
- 展開BoolAnd：?(lambda x y .x y FALSE) (lambda xf yf . yf) (lambda xt yt . xt)
- beta規約：(lambda xf yf . yf) (lambda xt yt . xt) FALSE
- 再beta規約：FALSE
所以，BoolAnd FALSE TRUE = FALSE
最后讓我們來算算，BoolAnd TRUE TRUE：
- 展開兩個TRUE：?BoolAnd (lambda x y . x) (lambda x y . x)
- alpha變換：?BoolAnd (lambda xa ya . xa) (lambda xb yb . xb)
- 展開BoolAnd：?(lambda x y . x y FALSE) (lambda xa ya . xa) (lambda xb yb . xb)
- beta規約：?(lambda xa ya . xa) (lambda xb yb . xb) FALSE
- beta規約：?(lambda xb yb .xb)
所以，BoolAnd TRUE TRUE = TRUE
總結
以上是生活随笔為你收集整理的【逻辑与计算理论】Lambda 演算——开篇的全部內容，希望文章能夠幫你解決所遇到的問題。
- 上一篇： 贪婪的送礼者（洛谷P1201题题解，Ja
- 下一篇： 【面向对象】面向对象程序设计测试题6-J