原文來自Good Math/Bad Math的系列連載，全文分7章，本篇是第1章。中文博客負(fù)暄瑣話對這個系列的前6章做過翻譯，強(qiáng)迫癥表示忍受不了「下面沒有了」，于是自己動手做了全套。這里只對原文做了翻譯，而“負(fù)暄瑣話”的版本則加上了很多掌故，使得閱讀起來更有趣味性。

Good Math, Bad Math

Lambda演算系列之七

（在這個帖子的原始版本里，我試圖用一個JavaScript工具來生成MathML。但不太順利：有幾個瀏覽器沒法正確的渲染，在RSS feed里也顯示的不好。所以我只好從頭開始，用簡單的文本格式重新寫一遍。）

?

我的最愛Lambda演算——開篇

計算機(jī)科學(xué)，尤其是編程語言，經(jīng)常傾向于使用一種特定的演算：Lambda演算（Lambda Calculus）。這種演算也廣泛地被邏輯學(xué)家用于學(xué)習(xí)計算和離散數(shù)學(xué)的結(jié)構(gòu)的本質(zhì)。Lambda演算偉大的的原因有很多，其中包括：

• 非常簡單。
• 圖靈完備。
• 容易讀寫。
• 語義足夠強(qiáng)大，可以從它開始做（任意）推理。
• 它有一個很好的實體模型。
• 容易創(chuàng)建變種，以便我們探索各種構(gòu)建計算或語義方式的屬性。

Lambda演算易于讀寫，這一點很重要。它導(dǎo)致人們開發(fā)了很多極為優(yōu)秀的編程語言，他們在不同程度上都基于Lambda演算：LISP，ML和Haskell語言都極度依賴于Lambda演算。

Lambda演算建立在函數(shù)的概念的基礎(chǔ)上。純粹的Lambda演算中，一切都是函數(shù)，連值的概念都沒有。但是，我們可以用函數(shù)構(gòu)建任何我們需要的東西。還記得在這個博客的初期，我談了一些關(guān)于如何建立數(shù)學(xué)的方法么？ 我們可以從無到有地用Lambda演算建立數(shù)學(xué)的整個結(jié)構(gòu)。

閑話少說，讓我們深入的看一看LC（Lambda Calculus）。對于一個演算，需要定義兩個東西：語法，它描述了如何在演算中寫出合法的表達(dá)式；一組規(guī)則，讓你符號化地操縱表達(dá)式。

Lambda演算的語法

Lambda演算只有三類表達(dá)式：

函數(shù)定義：Lambda演算中的函數(shù)是一個表達(dá)式，寫成：lambda x . body，表示“一個參數(shù)參數(shù)為x的函數(shù)，它的返回值為body的計算結(jié)果。” 這時我們說：Lambda表達(dá)式綁定了參數(shù)x。

標(biāo)識符引用（Identifier reference）：標(biāo)識符引用就是一個名字，這個名字用于匹配函數(shù)表達(dá)式中的某個參數(shù)名。

函數(shù)應(yīng)用（Function application）：函數(shù)應(yīng)用寫成把函數(shù)值放到它的參數(shù)前面的形式，如(lambda x . plus x x) y。

柯里化

在Lambda演算中有一個技巧：如果你看一下上面的定義，你會發(fā)現(xiàn)一個函數(shù)（Lambda表達(dá)式）只接受一個參數(shù)。這似乎是一個很大的局限 —— 你怎么能在只有一個參數(shù)的情況下實現(xiàn)加法？

這一點問題都沒有，因為函數(shù)就是值。你可以寫只有一個參數(shù)的函數(shù)，而這個函數(shù)返回一個帶一個參數(shù)的函數(shù)，這樣就可以實現(xiàn)寫兩個參數(shù)的函數(shù)了——本質(zhì)上兩者是一樣的。這就是所謂的柯里化（Currying），以偉大的邏輯學(xué)家Haskell Curry命名。

例如我們想寫一個函數(shù)來實現(xiàn)x + y。我們比較習(xí)慣寫成類似：lambda x y . plus x y之類的東西。而采用單個參數(shù)函數(shù)的寫法是：我們寫一個只有一個參數(shù)的函數(shù)，讓它返回另一個只有一個參數(shù)的函數(shù)。于是x + y就變成一個單參數(shù)x的函數(shù)，它返回另一個函數(shù)，這個函數(shù)將x加到它自己的參數(shù)上：

lambda x. ( lambda y. plus x y )

現(xiàn)在我們知道，添加多個參數(shù)的函數(shù)并沒有真正添加任何東西，只不過簡化了語法，所以下面繼續(xù)介紹的時候，我會在方便的時候用到多參數(shù)函數(shù)。

自由標(biāo)識符 vs. 綁定標(biāo)識符

有一個重要的語法問題我還沒有提到：閉包（closure）或者叫完全綁定（complete binding）。在對一個Lambda演算表達(dá)式進(jìn)行求值的時候，不能引用任何未綁定的標(biāo)識符。如果一個標(biāo)識符是一個閉合Lambda表達(dá)式的參數(shù)，我們則稱這個標(biāo)識符是（被）綁定的；如果一個標(biāo)識符在任何封閉上下文中都沒有綁定，那么它被稱為自由變量。

• lambda x . plus x y：在這個表達(dá)式中，y和plus是自由的，因為他們不是任何閉合的Lambda表達(dá)式的參數(shù)；而x是綁定的，因為它是函數(shù)定義的閉合表達(dá)式plus x y的參數(shù)。
• lambda x y . y x?：在這個表達(dá)式中x和y都是被綁定的，因為它們都是函數(shù)定義中的參數(shù)。
• lambda y . (lambda x . plus x y)：在內(nèi)層演算lambda x . plus x y中，y和plus是自由的，x是綁定的。在完整表達(dá)中，x和y是綁定的：x受內(nèi)層綁定，而y由剩下的演算綁定。plus仍然是自由的。

我們會經(jīng)常使用free(x)來表示在表達(dá)式x中自由的標(biāo)識符。

一個Lambda演算表達(dá)式只有在其所有變量都是綁定的時候才完全合法。但是，當(dāng)我們脫開上下文，關(guān)注于一個復(fù)雜表達(dá)式的子表達(dá)式時，自由變量是允許存在的——這時候搞清楚子表達(dá)式中的哪些變量是自由的就顯得非常重要了。

Lambda演算運(yùn)算法則

Lambda演算只有兩條真正的法則：稱為Alpha和Beta。Alpha也被稱為「轉(zhuǎn)換」，Beta也被稱為「規(guī)約」。

Alpha轉(zhuǎn)換

Alpha是一個重命名操作; 基本上就是說，變量的名稱是不重要的：給定Lambda演算中的任意表達(dá)式，我們可以修改函數(shù)參數(shù)的名稱，只要我們同時修改函數(shù)體內(nèi)所有對它的自由引用。

所以 —— 例如，如果有這樣一個表達(dá)式：

lambda x . if (= x 0) then 1 else x ^ 2

我們可以用Alpha轉(zhuǎn)換，將x變成y（寫作alpha[x / y]），于是我們有：

lambda y . if (= y 0) then 1 else y ^ 2

這樣絲毫不會改變表達(dá)式的含義。但是，正如我們將在后面看到的，這一點很重要，因為它使得我們可以實現(xiàn)比如遞歸之類的事情。

Beta規(guī)約

Beta規(guī)約才是精彩的地方：這條規(guī)則使得Lambda演算能夠執(zhí)行任何可以由機(jī)器來完成的計算。

Beta基本上是說，如果你有一個函數(shù)應(yīng)用，你可以對這個函數(shù)體中和對應(yīng)函數(shù)標(biāo)識符相關(guān)的部分做替換，替換方法是把標(biāo)識符用參數(shù)值替換。這聽起來很費(fèi)解，但是它用起來卻很容易。

假設(shè)我們有一個函數(shù)應(yīng)用表達(dá)式：“?(lambda x . x + 1) 3?“。所謂Beta規(guī)約就是，我們可以通過替換函數(shù)體（即“x + 1”）來實現(xiàn)函數(shù)應(yīng)用，用數(shù)值“3”取代引用的參數(shù)“x”。于是Beta規(guī)約的結(jié)果就是“3 + 1”。

一個稍微復(fù)雜的例子：(lambda y . (lambda x . x + y)) q。 這是一個挺有意思的表達(dá)式，因為應(yīng)用這個Lambda表達(dá)式的結(jié)果是另一個Lambda表達(dá)式：也就是說，它是一個創(chuàng)建函數(shù)的函數(shù)。這時候的Beta規(guī)約，需要用標(biāo)識符“q”替換所有的引用參數(shù)“y”。所以，其結(jié)果是“?lambda x . x + q?“。

再給一個讓你更不爽的例子：“?(lambda x y. x y) (lambda z . z * z) 3?“。這是一個有兩個參數(shù)的函數(shù)，它(的功能是)把第一個參數(shù)應(yīng)用到第二個參數(shù)上。當(dāng)我們運(yùn)算時，我們替換第一個函數(shù)體中的參數(shù)“x”為“l(fā)ambda z . z * z?“；然后我們用“3”替換參數(shù)“y”，得到：“?(lambda z . z * z) 3?“。 再執(zhí)行Beta規(guī)約，有“3 * 3”。

Beta規(guī)則的形式化寫法為：

lambda x . B e = B[x := e] if free(e) subset free(B[x := e])

最后的條件“if free(e) subset free(B[x := e])”說明了為什么我們需要Alpha轉(zhuǎn)換：我們只有在不引起綁定標(biāo)識符和自由標(biāo)識符之間的任何沖突的情況下，才可以做Beta規(guī)約：如果標(biāo)識符“z”在“e”中是自由的，那么我們就需要確保，Beta規(guī)約不會導(dǎo)致“z”變成綁定的。如果在“B”中綁定的變量和“e”中的自由變量產(chǎn)生命名沖突，我們就需要用Alpha轉(zhuǎn)換來更改標(biāo)識符名稱，使之不同。

例子更能明確這一點：假設(shè)我們有一個函數(shù)表達(dá)式，“?lambda z . (lambda x . x + z)?“，現(xiàn)在，假設(shè)我們要應(yīng)用它：

(lambda z . (lambda x . x + z)) (x + 2)

參數(shù)“(x + 2)”中，x是自由的。現(xiàn)在，假設(shè)我們不遵守規(guī)則直接做Beta規(guī)約。我們會得到：

lambda x . x + x + 2

原先在“x + 2”中自由的的變量現(xiàn)在被綁定了。再假設(shè)我們應(yīng)用該函數(shù)：

(lambda x . x + x + 2) 3

通過Beta規(guī)約，我們會得到“3 + 3 + 2”。

如果我們按照應(yīng)有的方式先采用Alpha轉(zhuǎn)換，又該如何？

• 由?alpha[x/y]?有:?(lambda z . (lambda y . y + z)) (x + 2)
• 由Beta規(guī)約：?(lambda y . y + x + 2) 3
• 再由Beta規(guī)約：?3 + x + 2?。

“3 + x + 2”和“3 + 3 + 2”是非常不同的結(jié)果！

規(guī)則差不多就是這些。還有另外一個規(guī)則，你可以選擇性地加一條被稱為Eta-規(guī)約的規(guī)則，不過我們將跳過它。 我在這里描述了一個圖靈完備 —— 完整有效的計算系統(tǒng)。 要讓它變得有用，或看它如何用來做些有實際意義的事情，我們還需要定義一堆能讓我們做數(shù)學(xué)計算的基本函數(shù)，條件測試，遞歸等，我將在下一篇文章討論這些。

我們也還沒有定義Lambda-演算的模型呢。（原作者在這里和這里討論了模型的概念。）模型實際上是非常重要的！邏輯學(xué)家們在擺弄了LC好幾年之后，才為其想出一個完整的模型，這是件非常重要的事情，因為雖然LC看起來是正確的，但在早期為它定義一個模型的嘗試，卻是失敗的。畢竟，請記住，如果沒有一個有效的模型，這意味著該系統(tǒng)的結(jié)果是毫無意義的！
?

阿隆佐.丘奇的天才之作——lambda演算中的數(shù)字

所以，現(xiàn)在，讓我們用lambda演算干點有趣的事。首先，為了方便起見，我將介紹些語法糖（syntactic sugar）來命名函數(shù)，以便下面遇到某些復(fù)雜的事情的時候方便我們閱讀。

引進(jìn)「全局」函數(shù)（即在我寫的這些所有的關(guān)于lambda演算的介紹里都可以直接使用，而不用在每一個表達(dá)式中都聲明一次這個函數(shù)的辦法），我們將使用“l(fā)et”表達(dá)式：

let square = lambda x . x ^ 2

這條表達(dá)式聲明了一個名為“square”的函數(shù)，其定義是lambda x . x ^ 2。如果我們有“?square 4”，則上面的“l(fā)et”表達(dá)式的等效表達(dá)式為：

(lambda square . square 4) (lambda x . x ^ 2)

某些例子中，我使用了數(shù)字和算術(shù)運(yùn)算。但數(shù)字并不真正存在于lambda演算中，我們有的只有函數(shù)！因此，我們需要發(fā)明某種使用函數(shù)來創(chuàng)建數(shù)字的方式。幸運(yùn)的是，邱奇（Alonzo Church），這個發(fā)明了lambda演算的天才，找出了做到這一點的辦法。他的函數(shù)化的數(shù)字的版本被稱為丘奇數(shù)（Church Numerals）。

所有的丘奇數(shù)都是帶有兩個參數(shù)的函數(shù)：

• 0是“?lambda s z . z?“。
• 1是“?lambda s z . s z?“。
• 2是“?lambda s z . s (s z)
• 對于任何數(shù)“n”，它的丘奇數(shù)是將其第一個參數(shù)應(yīng)用到第二個參數(shù)上“n”次的函數(shù)。

一個很好的理解辦法是將“z”作為是對于零值的命名，而“s”作為后繼函數(shù)的名稱。因此，0是一個僅返回“0”值的函數(shù)；1是將后繼函數(shù)運(yùn)用到0上一次的函數(shù)；2則是將后繼函數(shù)應(yīng)用到零的后繼上的函數(shù)，以此類推。

現(xiàn)在看好了，如果我們想要做加法，x + y，我們需要寫一個有四個參數(shù)的函數(shù)；兩個需要相加的數(shù)字；以及推導(dǎo)數(shù)字時用到的“s”和“z”：

let add = lambda s z x y . x s (y s z)

讓我們將其柯里化，看看是怎么回事。首先，它接受兩個參數(shù)，這是我們需要做加法的兩個值；第二，它需要正則化（normalize）這兩個參數(shù)，以使它們都使用對0（z）和后繼值（s）的綁定（即，將參數(shù)都寫成s和z的組合的形式）。

let add = lambda x y . (lambda s z . (x s (y s z)))

看下這個式子，它說的是，為了將x和y相加，先用參數(shù)“s”和“z”創(chuàng)建（正則化的）丘奇數(shù)“y”。然后應(yīng)用x到丘奇數(shù)y上，這時候使用由“s”和“z”定義的丘奇數(shù)y。也就是說，我們得到的結(jié)果是一個函數(shù)，這個函數(shù)把自己加到另一個數(shù)字上。（要計算x + y，先計算?y?是?z?的幾號后繼，然后計算x?是?y的幾號后繼。）

讓我們再進(jìn)一步看看2 + 3的運(yùn)算過程：

add (lambda s z . s (s z)) (lambda s z . s (s (s z))) news newz

為了更容易理解，對數(shù)字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規(guī)約：

lambda s z . (lambda s2 z2 . s2 (s2 z2)) s (lambda s3 z3 . s3 (s3 (s3 z3)) s z)

然后beta規(guī)約丘奇數(shù)”3”。這步操作其實是“正則化”3：把數(shù)字3的定義里的后繼函數(shù)和零函數(shù)替換成add的參數(shù)列表里的后繼函數(shù)和零函數(shù)：

lambda s z . (lambda s2 z2 . s2 (s2 z2)) s (s (s (s z)))

現(xiàn)在，到了最精妙的一步了。再對丘奇數(shù)”2”做beta規(guī)約。我們知道：2是一個函數(shù)，它接受兩個參數(shù)：一個后繼函數(shù)和0(函數(shù))。于是，要相加2和3，我們用后繼函數(shù)應(yīng)用到2的第一個參數(shù)；用3的運(yùn)算結(jié)果應(yīng)用到第二個參數(shù)（0函數(shù)）！

lambda s z . s (s (s (s (s z))))

于是，我們的結(jié)果是：丘奇數(shù)”5”！

?

Lambda演算中的布爾值和選擇

現(xiàn)在，我們在lambda演算中引入了數(shù)字，只差兩件事情就可以表達(dá)任意計算了：一個是如何表達(dá)選擇（分支），另一個是如何表示重復(fù)。在這篇文章中，我將討論布爾值和選擇，下一篇將介紹重復(fù)和遞歸。

我們希望能夠?qū)懗鲂稳?if / then / else語句的表達(dá)式，就像我們在大多數(shù)編程語言做的那樣。繼像丘奇數(shù)那樣將數(shù)字表示為函數(shù)之后，我們也將true和false值表示為對其參數(shù)執(zhí)行一個if-then-else操作的函數(shù)：

let TRUE = lambda x y . x let FALSE = lambda x y . y

于是，現(xiàn)在我們可以寫一個“if”函數(shù)，它的第一個參數(shù)是一個條件表達(dá)式，第二個參數(shù)是如果條件為真時才進(jìn)行運(yùn)算的表達(dá)式，第三個參數(shù)則如果條件為假時要進(jìn)行的運(yùn)算。

let IfThenElse = lambda cond true_expr false_expr . cond true_expr false_expr

此外我們還需要定義常用的邏輯運(yùn)算：

let BoolAnd = lambda x y . x y FALSE let BoolOr = lambda x y. x TRUE y let BoolNot = lambda x . x FALSE TRUE

現(xiàn)在，就讓我們過一遍這些定義。讓我們先看看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)
• 現(xiàn)在，展開BoolAnd：(lambda x y. x y FALSE) (lambda xt yt . xt) (lambda xf yf . yf)
• beta規(guī)約：(lambda xt yt.xt) (lambda xf yf. yf) FALSE
• 再次beta規(guī)約：(lambda xf xf . yf)

于是我們得到結(jié)果：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規(guī)約：(lambda xf yf . yf) (lambda xt yt . xt) FALSE
• 再beta規(guī)約：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規(guī)約：?(lambda xa ya . xa) (lambda xb yb . xb) FALSE
• beta規(guī)約：?(lambda xb yb .xb)

所以，BoolAnd TRUE TRUE = TRUE

總結(jié)

以上是生活随笔為你收集整理的【逻辑与计算理论】Lambda 演算——开篇的全部內(nèi)容，希望文章能夠幫你解決所遇到的問題。

如果覺得生活随笔網(wǎng)站內(nèi)容還不錯，歡迎將生活随笔推薦給好友。