MDA之路

前言

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

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

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

接下來的三天，一直在學習lambda演算的相關內容，由于資料不全，學習的過程很是痛苦。國內的大學好像基本上不開設Functional Programming課程，因此FP的基礎知識lambda演算也講得很少。不過好歹在網上找到了一些資料，加上數理邏輯中的少量介紹，明白了一個大致。相關資料網址會列在最后。

Lamda演算簡介

Wikipedia（維基百科全書）中關于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演算是一個形式系統，它被設計出來用來研究函數定義，函數應用和遞歸。它是在二十世紀三十年代由Alonzo Church 和 Stephen Cole Kleene發明的。Church在1936年使用lambda演算來證明了判定問題是沒有答案的。Lambda演算可以用來清晰的定義什么是一個可計算的函數。兩個lambda演算表達式是否相等的問題不能夠被一個通用的算法解決，這是第一個問題，它甚至排在停機問題之前。為了證明停機問題是沒有答案的，不可判定性能夠被證明。Lambda演算對于函數式編程語言（例如lisp）有重大的影響。

同時，數理邏輯中對于lambda演算的介紹就簡單得多：

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

這里不由得想起一位我尊敬的老師的博士畢業論文就是關于π-演算的，可惜這位老師已經去別的學校了。

Lambda演算表達了兩個計算機計算中最基本的概念“代入”和“置換”。“代入”我們一般理解為函數調用，或者是用實參代替函數中的形參；“置換”我們一般理解為變量換名規則。后面會講到，“代入”就是用lambda演算中的β-歸約概念。而“替換”就是lambda演算中的α-變換。

Lambda演算系統的形式化定義

維基百科全書上面的對于lambda演算的定義不是很正規，但是說明性的文字較多。而數理邏輯中的定義很嚴密，不過沒有說明不容易理解。我盡可能把所有資料結合起來說明lambda演算系統的定義。

字母表

lambda演算系統中合法的字符如下：

1.         x1，x2，x3，…變元（變元的數量是無窮的，不能在有限步驟內窮舉，這個很重要，后面有定理是根據這一點證明的）

2.         à 歸約

3.         ＝ 等價

4.         λ，（，）  （輔助工具符號，一共有三個，λ和左括號右括號）

所有能夠在lambda演算系統中出現的合法符號只有以上四種，其他符號都是非法的。例如λx.x+2，如果沒有其他對于＋符號的說明，那么這就是一個非法的λ演算表達式。

λ-項

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

1.         任一個變元是一個項

2.         若M，N是項，則（MN）也是一個項  （function application，函數應用）

3.         若M是一個項，而x是一個變元，則（λx.M）也是一個項  （function abstraction，函數抽象）

4.         僅僅由以上規則歸納定義得到的符號串是項

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

說明2：(λx.M)這樣的λ-項被稱為函數抽象，原因是它常常就是一個函數的定義，函數的參數就是變量x，函數體就是M，而函數名稱則是匿名的。用一個不恰當的比喻來說，我們通常認為的函數f(x)=x+2，可以被表達為λx.x+2。因為＋是未定義的，所以這個比喻只是為了方便理解而已。

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

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

    上面是λ-項的形式化定義，有一些是可以與函數理論直觀聯系的，而另一些只是說明這個λ-項是合法的，不一定有直觀的字面意義。

公式

    若M，N是λ-項，則MàN，M=N是公式。

λ-項中的變量自由出現法則

在一個λ-項中，變量要么是自由出現的，要么是被一個λ符號綁定的。還是以函數的方式來理解變量的自由出現和綁定。例如f(x)=xy這個函數，我們知道x是和函數f相關的，因為它是f的形參，而y則是和f無關的。那么在λx.xy這個λ-項中，x就是被λ綁定的，而y則是自由出現的變量。

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

Lambda變量綁定規則：

1.         在表達式x中，如果x本身就是一個變量，那么x就是一個單獨的自由出現。

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

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

另一種關于變量的自由出現的規則也許更直接：

1.         free(x) = x

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

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

為什么要花大力氣來給出變量自由出現的規則，是因為后面的很多地方要用到變量的自由出現的概念。例如α-變換和β-歸約。

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

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

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

所以在A中f和x都是自由出現的，

所以E中x是綁定λ x

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

λ x的控制域

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

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

α-變換（α-conversion）

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

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

α-變換規則如下：

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

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

α-變換主要用來表達函數中的變量換名規則，需要注意的是被換名的只能是M（函數體）中變量的自由出現。

β-歸約

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

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

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

一些例子如下：

(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

需要多加練習才能習慣這種歸約。

η-變換（η-conversion）

η-變換表達了“外延性”（extensionality）的概念，在這種上下文中，兩個函數被認為是相等的“當且僅當”對于所有的參數，它們都給出同樣的結果。我理解為，對于所有的實參，通過β-歸約都能得到同樣的λ-項，或者使用α-變換進行換名后得到同樣的λ-項。

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

λ演算的公理和規則組成

這一段來自《數理邏輯與集合論》（第二版 清華大學出版社）。還修正了其中的一個錯誤。

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

2.         MàM

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

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。

范式

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

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

例子

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

例子

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

注意這個λx.(xx) λx.(xx)在λ演算的協調性研究中是一個比較經典的項。((λ x. x x) (λ x. x x))被稱為Ω, ((λ x. x x x) (λ x. x x x))被稱為 Ω2。

不動點理論

Λ表示所有的λ-項組成的集合。

定理：對于每一個F∈Λ，存在M∈Λ，使得λ├FM=M。

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

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

Church-Rosser定理及其等價定理

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

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

與之等價的定理如下，

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

后記

最后兩個定理的證明沒有怎么看懂，所以沒有在筆記中記下。另外，前天在網上訂購的《程序設計語言：概念和結構》第二版剛剛拿到手，其中有關于λ演算的一章。應該也對我大有幫助，待看完再說。

學習λ演算的初衷是了解一些程序設計的最基本原理，沒想到最后還是繞到形式系統和數理邏輯這兒來了。不過，形式化表達的λ演算更清晰。

國內大學雖然也開程序設計的課程，不過好像都是pascal，c/c++之類，關于程序設計的本質基礎的程序好像并不多。隨著大學擴招，中國有望在很短的時間內成為世界上程序員最多的國家，如果僅僅只學命令式和面向對象的程序設計，一定是不夠的。函數式和邏輯式程序設計語言也是要學學的啊。

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

參考文獻

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

這個大學的FP課程中的Lambda演算相關部分

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

wikipedia中lambda演算相關介紹

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

《數理邏輯與集合論》第二版 清華大學出版社