MDA之路

前言

blog好久沒有更新了，上次更新還是4月28號(hào)。這段時(shí)間實(shí)在是很忙，4月的最后一周為了趕一篇論文，累死累活，最后在tom的幫助下總算在4月30號(hào)截稿之前完成了。4月29號(hào)的晚上一直改到了第二天凌晨3點(diǎn)才睡。

4月30號(hào)下午回家，可是沒有料到長(zhǎng)沙的八一路修路，路上堵車。打的從學(xué)校到火車站花了40分鐘，平時(shí)只要15分鐘的。于是在最后10分鐘一路狂奔，終于在開車前1分鐘上車了。

五一長(zhǎng)假的第一天去了雙峰山，云霧繚繞之中真的頗有幾分氣勢(shì)，可惜數(shù)碼照片全部都拍得很模糊，早知道我就自己動(dòng)手好了。五一歸來馬上開始整理軟件工程相關(guān)資料，一共花了3天時(shí)間，還剩軟件標(biāo)準(zhǔn)化的部分沒有整理完畢。

接下來的三天，一直在學(xué)習(xí)lambda演算的相關(guān)內(nèi)容，由于資料不全，學(xué)習(xí)的過程很是痛苦。國(guó)內(nèi)的大學(xué)好像基本上不開設(shè)Functional Programming課程，因此FP的基礎(chǔ)知識(shí)lambda演算也講得很少。不過好歹在網(wǎng)上找到了一些資料，加上數(shù)理邏輯中的少量介紹，明白了一個(gè)大致。相關(guān)資料網(wǎng)址會(huì)列在最后。

Lamda演算簡(jiǎn)介

Wikipedia（維基百科全書）中關(guān)于lambda演算的解釋如下：

The lambda calculus is a formal system designed to investigate function definition, function application, and recursion. It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s; Church used the lambda calculus in 1936 to give a negative answer to the Entscheidungsproblem. The calculus can be used to cleanly define what a computable function is. The question of whether two lambda calculus expressions are equivalent cannot be solved by a general algorithm, and this was the first question, even before the halting problem, for which undecidability could be proved. Lambda calculus has greatly influenced functional programming languages, especially Lisp.

Lambda演算是一個(gè)形式系統(tǒng)，它被設(shè)計(jì)出來用來研究函數(shù)定義，函數(shù)應(yīng)用和遞歸。它是在二十世紀(jì)三十年代由Alonzo Church 和 Stephen Cole Kleene發(fā)明的。Church在1936年使用lambda演算來證明了判定問題是沒有答案的。Lambda演算可以用來清晰的定義什么是一個(gè)可計(jì)算的函數(shù)。兩個(gè)lambda演算表達(dá)式是否相等的問題不能夠被一個(gè)通用的算法解決，這是第一個(gè)問題，它甚至排在停機(jī)問題之前。為了證明停機(jī)問題是沒有答案的，不可判定性能夠被證明。Lambda演算對(duì)于函數(shù)式編程語(yǔ)言（例如lisp）有重大的影響。

同時(shí)，數(shù)理邏輯中對(duì)于lambda演算的介紹就簡(jiǎn)單得多：

λ-演算可以說是最簡(jiǎn)單、最小的一個(gè)形式系統(tǒng)。它是在二十世紀(jì)三十年代由Alonzo Church 和 Stephen Cole Kleene發(fā)明的。至今，在歐洲得到了廣泛的發(fā)展。可以說，歐洲的計(jì)算機(jī)科學(xué)是從λ-演算開始的，而現(xiàn)在仍然是歐洲計(jì)算機(jī)科學(xué)的基礎(chǔ)，首先它是函數(shù)式程序理論的基礎(chǔ)，而后，在λ-演算的基礎(chǔ)上，發(fā)展起來的π-演算、χ-演算，成為近年來的并發(fā)程序的理論工具之一，許多經(jīng)典的并發(fā)程序模型就是以π-演算為框架的。

這里不由得想起一位我尊敬的老師的博士畢業(yè)論文就是關(guān)于π-演算的，可惜這位老師已經(jīng)去別的學(xué)校了。

Lambda演算表達(dá)了兩個(gè)計(jì)算機(jī)計(jì)算中最基本的概念“代入”和“置換”。“代入”我們一般理解為函數(shù)調(diào)用，或者是用實(shí)參代替函數(shù)中的形參；“置換”我們一般理解為變量換名規(guī)則。后面會(huì)講到，“代入”就是用lambda演算中的β-歸約概念。而“替換”就是lambda演算中的α-變換。

Lambda演算系統(tǒng)的形式化定義

維基百科全書上面的對(duì)于lambda演算的定義不是很正規(guī)，但是說明性的文字較多。而數(shù)理邏輯中的定義很嚴(yán)密，不過沒有說明不容易理解。我盡可能把所有資料結(jié)合起來說明lambda演算系統(tǒng)的定義。

字母表

lambda演算系統(tǒng)中合法的字符如下：

1.         x1，x2，x3，…變?cè)ㄗ冊(cè)臄?shù)量是無窮的，不能在有限步驟內(nèi)窮舉，這個(gè)很重要，后面有定理是根據(jù)這一點(diǎn)證明的）

2.         à 歸約

3.         ＝ 等價(jià)

4.         λ，（，）  （輔助工具符號(hào)，一共有三個(gè)，λ和左括號(hào)右括號(hào)）

所有能夠在lambda演算系統(tǒng)中出現(xiàn)的合法符號(hào)只有以上四種，其他符號(hào)都是非法的。例如λx.x+2，如果沒有其他對(duì)于＋符號(hào)的說明，那么這就是一個(gè)非法的λ演算表達(dá)式。

λ-項(xiàng)

λ-項(xiàng)在一些文章中也稱為λ表達(dá)式（lambda expression），它是由上面字母表中的合法字符組成的表達(dá)式，合法的表達(dá)式組成規(guī)則如下：

1.         任一個(gè)變?cè)且粋€(gè)項(xiàng)

2.         若M，N是項(xiàng)，則（MN）也是一個(gè)項(xiàng)  （function application，函數(shù)應(yīng)用）

3.         若M是一個(gè)項(xiàng)，而x是一個(gè)變?cè)瑒t（λx.M）也是一個(gè)項(xiàng)  （function abstraction，函數(shù)抽象）

4.         僅僅由以上規(guī)則歸納定義得到的符號(hào)串是項(xiàng)

說明1：λ-項(xiàng)是左結(jié)合的，意思就是若f x y都是λ-項(xiàng)，那么f x y＝(f x) y

說明2：(λx.M)這樣的λ-項(xiàng)被稱為函數(shù)抽象，原因是它常常就是一個(gè)函數(shù)的定義，函數(shù)的參數(shù)就是變量x，函數(shù)體就是M，而函數(shù)名稱則是匿名的。用一個(gè)不恰當(dāng)?shù)谋扔鱽碚f，我們通常認(rèn)為的函數(shù)f(x)=x+2，可以被表達(dá)為λx.x+2。因?yàn)椋俏炊x的，所以這個(gè)比喻只是為了方便理解而已。

說明3：MN這樣的λ-項(xiàng)被稱為函數(shù)應(yīng)用，原因是它表達(dá)了將M這個(gè)函數(shù)應(yīng)用到N這個(gè)概念。沿用上面的例子f(x)=x+2，那么f(2)=2+2；同樣的λx.x+2表達(dá)了f(x)的概念，那么（λx.x+2）2表達(dá)了f(2)的概念。其中M＝λx.x+2，N＝2，所以MN＝（λx.x+2）2。

說明4：注意說明3只是為了方便理解，但是還存在很多與直觀理解不符合的地方。例如xy也是一個(gè)合法的λ-項(xiàng)，它們也是MN形式的，不過x和y都僅僅是一個(gè)變量而已，談不上函數(shù)代入。

    上面是λ-項(xiàng)的形式化定義，有一些是可以與函數(shù)理論直觀聯(lián)系的，而另一些只是說明這個(gè)λ-項(xiàng)是合法的，不一定有直觀的字面意義。

公式

    若M，N是λ-項(xiàng)，則MàN，M=N是公式。

λ-項(xiàng)中的變量自由出現(xiàn)法則

在一個(gè)λ-項(xiàng)中，變量要么是自由出現(xiàn)的，要么是被一個(gè)λ符號(hào)綁定的。還是以函數(shù)的方式來理解變量的自由出現(xiàn)和綁定。例如f(x)=xy這個(gè)函數(shù)，我們知道x是和函數(shù)f相關(guān)的，因?yàn)樗?/SPAN>f的形參，而y則是和f無關(guān)的。那么在λx.xy這個(gè)λ-項(xiàng)中，x就是被λ綁定的，而y則是自由出現(xiàn)的變量。

直觀的理解，被綁定的變量就是作為某個(gè)函數(shù)形參的變量，而自由變量則是不作為任何函數(shù)形參的變量。

Lambda變量綁定規(guī)則：

1.         在表達(dá)式x中，如果x本身就是一個(gè)變量，那么x就是一個(gè)單獨(dú)的自由出現(xiàn)。

2.         在表達(dá)式λ x. E中，自由出現(xiàn)就是E中所有的除了x的自由出現(xiàn)。這種情況下在E中所有x的出現(xiàn)都稱為被表達(dá)式中x前面的那個(gè)λ所綁定。

3.         在表達(dá)式(MN )中，變量的自由出現(xiàn)就是M和N中所有變量的自由出現(xiàn)。

另一種關(guān)于變量的自由出現(xiàn)的規(guī)則也許更直接：

1.         free(x) = x

2.         free(MN) = free(M) è free(N)

3.         free(lx ? M) = free(M) – {x}

為什么要花大力氣來給出變量自由出現(xiàn)的規(guī)則，是因?yàn)楹竺娴暮芏嗟胤揭玫阶兞康淖杂沙霈F(xiàn)的概念。例如α-變換和β-歸約。

例子：分析λf.λx.fx中變量的自由出現(xiàn)和綁定狀況。

λf.λx.fx =λf.E, E=λx.fx

E=λx.A, A=A1A2, A1=f, A2=x

所以在A中f和x都是自由出現(xiàn)的，

所以E中x是綁定λ x

所以整個(gè)公式中f是綁定第一個(gè)λ f的。

λ x的控制域

來看兩個(gè)λ-項(xiàng)，λx.xx和λx.(xx)有何不同？根據(jù)左結(jié)合的法則，λx.xx＝(λx.x)x，其中第一個(gè)x是被λ綁定的，而第二個(gè)x則是自由出現(xiàn)的。而λx.(xx)中兩個(gè)x都是被λ綁定的。這表明了兩個(gè)λ-項(xiàng)中λx的控制域是不同的。

我們知道謂詞演算中量詞也是有控制域的，λx的控制域與它們類似，這里就不給出詳細(xì)的定義了。其實(shí)也很直觀。

α-變換（α-conversion）

α-變換規(guī)則試圖解釋這樣一個(gè)概念，λ演算中約束變量的名稱是不重要的，例如λx.x和λy.y是相同的函數(shù)。因此，將某個(gè)函數(shù)中的所有約束變量全部換名是可以的。但是，換名需要遵循一些約束。

首先是一個(gè)說明：如果M，N是λ-項(xiàng)，x在M中有自由出現(xiàn)，若以N置換M中所有x的自由出現(xiàn)（M中可能含有x的約束出現(xiàn)），我們得到另一個(gè)λ-項(xiàng)，記為M[x/N]。

α-變換規(guī)則如下：

λx.M=λy.M[x/y]  如果y沒有在M中自由出現(xiàn)，并且只要y替換M中的x，都不會(huì)被M中的一個(gè)λ綁定。

例子：λx.( λx.x)x = λy(λx.x)y

α-變換主要用來表達(dá)函數(shù)中的變量換名規(guī)則，需要注意的是被換名的只能是M（函數(shù)體）中變量的自由出現(xiàn)。

β-歸約

β-歸約表達(dá)的是函數(shù)應(yīng)用或者函數(shù)代入的概念。前面提到MN是合法的λ-項(xiàng)，那么MN的含義是將M應(yīng)用到N，通俗的說是將N作為實(shí)參代替M中的約束變量，也就是形參。β-歸約的規(guī)則如下：

(λx.M)N à M[x/N] 如果N中所有變量的自由出現(xiàn)都在M[x/N]中保持自由出現(xiàn)

β-歸約是λ演算中最重要的概念和規(guī)則，它是函數(shù)代入這個(gè)概念的形式化表示。

一些例子如下：

(lx.ly.y x)(lz.u) ? ly.y(lz.u)

(lx. x x)(lz.u) ? (lz.u) (lz.u)

(ly.y a)((lx. x)(lz.(lu.u) z)) ? (ly.y a)(lz.(lu.u) z)

(ly.y a)((lx. x)(lz.(lu.u) z)) ? (ly.y a)((lx. x)(lz. z))

(ly.y a)((lx. x)(lz.(lu.u) z)) ? ((lx. x)(lz.(lu.u) z)) a

需要多加練習(xí)才能習(xí)慣這種歸約。

η-變換（η-conversion）

η-變換表達(dá)了“外延性”（extensionality）的概念，在這種上下文中，兩個(gè)函數(shù)被認(rèn)為是相等的“當(dāng)且僅當(dāng)”對(duì)于所有的參數(shù)，它們都給出同樣的結(jié)果。我理解為，對(duì)于所有的實(shí)參，通過β-歸約都能得到同樣的λ-項(xiàng)，或者使用α-變換進(jìn)行換名后得到同樣的λ-項(xiàng)。

例如λx.fx與f相等，如果x沒有在f中自由出現(xiàn)。

λ演算的公理和規(guī)則組成

這一段來自《數(shù)理邏輯與集合論》（第二版 清華大學(xué)出版社）。還修正了其中的一個(gè)錯(cuò)誤。

1.         (λx.M)N à M[x/N] 如果N中所有變量的自由出現(xiàn)都在M[x/N]中保持自由出現(xiàn)

2.         MàM

3.         MàN, NàL => MàL  （原書中此處錯(cuò)誤）

4.         MàM’=>ZMàZM’

5.         MàM’=>MZàM’Z

6.         MàM’=>λx. M àλx. M’

7.         MàM’=>M=M’

8.         M=M’=>M’=M

9.         M=N,N=L=>M=L

10.     M=M’ => ZM = ZM’

11.     M=M’ => MZ = M’Z

12.     M=M’ =>λx. M =λx. M’

如果某一公式MàN或者M=N可以用以上的公理推出，則記為λ├MàN和λ├M＝N。

范式

如果一個(gè)λ-項(xiàng)M中不含有任何形為((λx.N1)N2)的子項(xiàng)，則稱M是一個(gè)范式，簡(jiǎn)記為n.f.。如果一個(gè)λ-項(xiàng)M通過有窮步β-歸約后，得到一個(gè)范式，則稱M有n.f.，沒有n.f.的λ-項(xiàng)稱為n.n.f.。

    通俗的說法是，將一個(gè)λ-項(xiàng)進(jìn)行β-歸約，也就是進(jìn)行實(shí)參代入形參的過程，如果通過有窮步代入，可以得到一個(gè)不能夠再進(jìn)行代入的λ-項(xiàng)，那么這就是它的范式。如果無論怎樣代入，總存在可以繼續(xù)代入的子項(xiàng)，那么它就沒有范式。

例子

M = λx.(x((λy.y)x))y，則Mà y((λy.y)y) à yy。M有一個(gè)n.f.。

例子

M =λx.(xx) λx.(xx)，則Màλx.(xx) λx.(xx)=M。注意到M的歸約只有唯一的一個(gè)可能路徑，所以M不可能歸約到n.f.。所以M是n.n.f.。

注意這個(gè)λx.(xx) λx.(xx)在λ演算的協(xié)調(diào)性研究中是一個(gè)比較經(jīng)典的項(xiàng)。((λ x. x x) (λ x. x x))被稱為Ω, ((λ x. x x x) (λ x. x x x))被稱為 Ω2。

不動(dòng)點(diǎn)理論

Λ表示所有的λ-項(xiàng)組成的集合。

定理：對(duì)于每一個(gè)F∈Λ，存在M∈Λ，使得λ├FM=M。

證明：定義w＝λx.F(xx)，又令M＝ww，則有λ├M＝ww＝(λx.F(xx))w＝F(ww)=FM。

證明是非常巧妙的，對(duì)于每個(gè)F，構(gòu)造出的這個(gè)ww剛好是可以通過一次β-歸約得到F(ww)＝FM，如果再歸約一次就得到F(FM)，這樣可以無限次的歸約下去得到F(F(F(F…(FM)…)))。

Church-Rosser定理及其等價(jià)定理

這兩個(gè)定理告訴我們這樣一個(gè)事實(shí)：如果M有一個(gè)n.f.，則這個(gè)n.f.是唯一的，任何β-歸約的路徑都將終止，并且終止到這個(gè)n.f.。

Church-Rosser定理：如果λ├M=N，則對(duì)某一個(gè)Z，λ├MàZ并且λ├NàZ。

與之等價(jià)的定理如下，

Diamond Property定理：如果MàN1,MàN2，則存在某一Z，使得N1àZ，N2àZ。

后記

最后兩個(gè)定理的證明沒有怎么看懂，所以沒有在筆記中記下。另外，前天在網(wǎng)上訂購(gòu)的《程序設(shè)計(jì)語(yǔ)言：概念和結(jié)構(gòu)》第二版剛剛拿到手，其中有關(guān)于λ演算的一章。應(yīng)該也對(duì)我大有幫助，待看完再說。

學(xué)習(xí)λ演算的初衷是了解一些程序設(shè)計(jì)的最基本原理，沒想到最后還是繞到形式系統(tǒng)和數(shù)理邏輯這兒來了。不過，形式化表達(dá)的λ演算更清晰。

國(guó)內(nèi)大學(xué)雖然也開程序設(shè)計(jì)的課程，不過好像都是pascal，c/c++之類，關(guān)于程序設(shè)計(jì)的本質(zhì)基礎(chǔ)的程序好像并不多。隨著大學(xué)擴(kuò)招，中國(guó)有望在很短的時(shí)間內(nèi)成為世界上程序員最多的國(guó)家，如果僅僅只學(xué)命令式和面向?qū)ο蟮某绦蛟O(shè)計(jì)，一定是不夠的。函數(shù)式和邏輯式程序設(shè)計(jì)語(yǔ)言也是要學(xué)學(xué)的啊。

文中肯定有很多錯(cuò)漏，希望看出來的人給我留言。

參考文獻(xiàn)

School of Computer Science and Software Engineering, Faculty of Information Technology, Monash University, Australia 3800

這個(gè)大學(xué)的FP課程中的Lambda演算相關(guān)部分

http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Ch/

wikipedia中lambda演算相關(guān)介紹

http://en.wikipedia.org/wiki/Lambda_calculus

《數(shù)理邏輯與集合論》第二版 清華大學(xué)出版社