目錄 1 歷史 2 非形式化的描述 3 形式化的定義 3.1字母表 3.2 λ-項 3.3 公式 3.4 λ-項中的變量自由出現(xiàn)法則 3.5 λ x的控制域 4 變換與等價關(guān)系 4.1 α-變換 4.2 β-歸約 4.3 等價關(guān)系 4.4 η-變換 5 λ演算的操作語義 6 λ演算的公理化和定理 6.1 λ演算的公理 6.2 不動點理論 6.3 Church-Rosser定理及其等價定理 7 lambda 演算中的程序設(shè)計 7.1 自然數(shù)與運算 7.2 邏輯與斷言 7.3 遞歸 8 參考文獻(xiàn)和外部鏈接

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

 

4 變換與等價關(guān)系

4.1 α-變換

α-變換規(guī)則表達(dá)的是，被綁定變量的名稱是不重要的。比如說 λx.x 和 λy.y 是同一個函數(shù)。因此，將某個函數(shù)中的所有約束變量全部換名是可以的。盡管如此，這條規(guī)則并非像它看起來這么簡單，關(guān)于被綁定的變量能否由另一個替換有一系列的限制需要遵循。

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

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

λx.M≌λy.M[x/y]  如果y沒有在M中自由出現(xiàn)，并且只要y替換M中的x，都不會被M中的一個λ綁定。即：替換的變元不能在M中自由出現(xiàn)，并且也只替換M中的自由變元

這條規(guī)則告訴我們，例如 λ x. (λ x. x) x 這樣的表達(dá)式和 λ y. (λ x. x) y 是一樣的。

注意：M[x/N]定義出來只是一種記號，它不等于α-變換。既M！≌ M[x/y]

例子：λx.( λx.x)x≌λy.(λx.x)y  但是 ( λx.x)x！≌(λx.x)y

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

4.2 β-歸約

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

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

注意： (lx. ly.(y x))y ?ly.(y y)是錯的，應(yīng)為y在ly.(y x)中不自由出現(xiàn)，這時要歸約就應(yīng)該先用α-變換把ly.(y x)中的y換成其他變元

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

一些例子如下：

(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í)慣這種歸約。

4.3 等價關(guān)系

在 lambda 表達(dá)式的集合上定義了一個等價關(guān)系 (在此用  標(biāo)注)，“兩個表達(dá)式其實表示的是同一個函數(shù)”這樣的直覺性判斷即由此表述，這種等價關(guān)系是通過所謂的“alpha-變換規(guī)則”和“beta-歸約規(guī)則”得到的。

f g:當(dāng)且僅當(dāng)（1）g≌f ;(2)g甪 or f甮 ;(3)存在h，f h且h g之一成立。

 關(guān)系被定義為滿足上述規(guī)則的最小等價關(guān)系 (即在這個等價關(guān)系中減去任何一個映射，它將不再是一個等價關(guān)系)。

4.4 η-變換

前兩條規(guī)則之后，還可以加入第三條規(guī)則，η-變換，來形成一個新的等價關(guān)系。η-變換表達(dá)的是外延性的概念，在這里外延性指的是，兩個函數(shù)對于所有的參數(shù)得到的結(jié)果都一致，當(dāng)且僅當(dāng)它們是同一個函數(shù)。

η-變換：λ x . f x  f，只要 x 不是 f 中的自由出現(xiàn)。

f 與 g 外延的等價：對任意lambda 表達(dá)式 a，如果有f a  g a成立，則f  g也成立。

下面說明了為何這條規(guī)則和外延性是等價的：（即由η-變換可以證明外延等價，相反由外延等價也可以證明η-變換）

f a  g a 對所有的 lambda 表達(dá)式 a 成立，則當(dāng)取 a 為在 f 中不是自由出現(xiàn)的變量 x 時，我們有 f x  g x，因此 λ x . f x  λ x . g x，由 η-變換 f  g。所以只要 η-變換是有效的，會得到外延性也是有效的。

相反地，若外延性是有效的，則由β-歸約，對所有的 y 有 (λ x . f x) y  f y，可得 λ x . f x  f，即 η-變換也是有效的

5 λ演算的操作語義

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

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

例子

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)在λ演算的協(xié)調(diào)性研究中是一個比較經(jīng)典的項。((λ x. x x) (λ x. x x))被稱為Ω, ((λ x. x x x) (λ x. x x x))被稱為 Ω2。

一般的把一個λ-項規(guī)約為范式的過程稱為求值，范式也叫做值。在《類型和程序設(shè)計語言》一書中，作者給出了λ-演算中的幾種不同的求值策略。每個策略確定一個項在下一步求值中激活哪一個約式或幾個約式。

注意到在求值的過程中是左結(jié)合，并且當(dāng)且僅當(dāng)左邊以是值了才能對右邊的項進(jìn)一步求值      

6 λ演算的公理化和定理

6.1 λ演算的公理

這一段來自《數(shù)理邏輯與集合論》（第二版 清華大學(xué)出版社）。

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 

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’

13．M≌N => MàN 如果y沒有在M中自由出現(xiàn)，并且只要y替換M中的x，都不會被M中的一個λ綁定。

如果某一公式MàN或者M(jìn) N可以用以上的公理推出，則記為λ├MàN和λ├M N。

規(guī)則13可以加也可以不要，要了表示是考慮α-變換的系統(tǒng)

6.2 不動點理論

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

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

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

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

6.3 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。（規(guī)約的合流性）

推論：MàN1,MàN2 且N1,N2都是范式 則N1≌N2 (范式在α-變換下的唯一性)

 關(guān)系被定義為滿足上述兩條規(guī)則的最小等價關(guān)系 (即在這個等價關(guān)系中減去任何一個映射，它將不再是一個等價關(guān)系)。

對上述等價關(guān)系的一個更具操作性的定義可以這樣獲得：只允許從左至右來應(yīng)用規(guī)則。不允許任何 beta 歸約的 lambda 表達(dá)式被稱為范式。并非所有的 lambda 表達(dá)式都存在與之等價的范式，若存在，則對于相同的形式參數(shù)命名而言是唯一的。此外，有一個算法用來計算范式，不斷地把最左邊的形式參數(shù)替換為實際參數(shù)，直到無法再作任何可能的規(guī)約為止。這個算法當(dāng)且僅當(dāng) lambda 表達(dá)式存在一個范式時才會停止。Church-Rosser 定理 說明了，當(dāng)且僅當(dāng)兩個表達(dá)式等價時，它們會在形式參數(shù)換名后得到同一個范式。

7 lambda 演算中的程序設(shè)計

7.1 自然數(shù)與運算

在 lambda 演算中有許多方式都可以定義自然數(shù)，但最常見的還是邱奇數(shù)，下面是它們的定義：

0 = λ s. λ z. z

1 =λ s. λ z.. s z

2 =λ s. λ z. s (s z)

3 =λ s. λ z. s (s (s z))

以此類推。直觀地說，lambda 演算中的數(shù)字 n 就是一個把函數(shù) f 作為參數(shù)并以 f 的 n 次冪為返回值的函數(shù)。換句話說，Church 整數(shù)是一個高階函數(shù) -- 以單一參數(shù)函數(shù) f 為參數(shù)，返回另一個單一參數(shù)的函數(shù)。

(注意在 Church 原來的 lambda 演算中，lambda 表達(dá)式的形式參數(shù)在函數(shù)體中至少出現(xiàn)一次，這使得我們無法像上面那樣定義 0) 在 Church 整數(shù)定義的基礎(chǔ)上，我們可以定義一個后繼函數(shù)，它以 n 為參數(shù)，返回 n + 1：

SUCC1 = λ n. λ s. λ z. s(n s z)

SUCC2 =  λ n. λ s. λ z. n s(s z)

加法是這樣定義的：

PLUS = λ m. λ n. λ s. λ z. m s (n s z)

PLUS 可以被看作以兩個自然數(shù)為參數(shù)的函數(shù)，它返回的也是一個自然數(shù)。你可以試驗證

PLUS 2 3    與    5

是否等價。乘法可以這樣定義：

MULT = λ m. λ n. m (PLUS n) 0,

MULT2 =λ m. λ n. λ s. λ z. m (n s) z

即 m 乘以 n 等于在零的基礎(chǔ)上 n 次加 m。更簡潔的一種方式是

MULT3 = λ m. λ n. λ s. m (n s)

冪的定義：

       POWER1 = λ m. λ n. m (MULT n) 1

       POWER2 = λ m. λ n. m n  (可能有點問題，我驗證了好象不正確)

正整數(shù) n 的前驅(qū)元 (predecessesor) PRED n = n - 1 要復(fù)雜一些：

PRED = λ n. λ f. λ x. n (λ g. λ h. h (g f)) (λ u. x) (λ u. u)

或者

PRED = λ n. n (λ g. λ k. (g 1) (λ u. PLUS (g k) 1) k) (λ l. 0) 0

注意 (g 1) (λ u. PLUS (g k) 1) k 表示的是，當(dāng) g(1) 是零時，表達(dá)式的值是 k，否則是 g(k) + 1。

   在《類型和程序設(shè)計語言》一書中作者對于數(shù)和各種運算的編碼描述得比較清晰，強(qiáng)烈建議看以下，并且作者還介紹了直接基于原始的布爾類型和數(shù)型的系統(tǒng)，簡稱為λNB，并給出了這兩套系統(tǒng)之間的轉(zhuǎn)換。

7.2 邏輯與斷言

習(xí)慣上，下述兩個定義 (稱為 Church 布爾值) 被用作 TRUE 和 FALSE 這樣的布爾值：

tru = λ u. λ v. u

fls = λ u. λ v. v

這樣我們可以定義一個組合式test=λl.λm.λ n.lmn，使得b為tru時，test b v w規(guī)約為v，而當(dāng)b為fls時，test b v w規(guī)約為w。

并且我們還可以定義邏輯連接詞：

and = λb. λc. b c fls

or =λb. λc. b c tru

not =λb. b fls tru

斷言是指返回布爾值的函數(shù)。最基本的一個斷言 ISZERO，當(dāng)且僅當(dāng)其參數(shù)為零時返回真：

ISZERO = λ n. n (λ x. fls) tru

斷言的運用與上述 TRUE 和 FALSE 的定義，使得 "if-then-else" 這類語句很容易用 lambda 演算寫出。

7.3 遞歸  

遞歸是一種以函數(shù)自身迭代自身變元的算法，一般是通過函數(shù)自身來定義函數(shù)的方式實現(xiàn)。表面看來 lambda 演算不允許遞歸，其實這是一種對遞歸的誤解。考慮階乘函數(shù) f(n) 一般這樣遞歸地定義：

f(n) = 1, 若 n = 0; n·f(n-1), 若 n>0.

λ語言：

FACT = λ n. n (λ u. MULT n (FACT (PRED n))) 1

用 Y-組合子 在 λ語言 中合法地定義：

FACT = Y (λ g. λ n. n (λ u. MULT n (g (PRED n))) 1)

Y = λ f. ((λ x. f (x x)) (λ x. f (x x)))

這一節(jié)我也沒分析透徹，只能原本引用，并且以上的內(nèi)容也只能當(dāng)作一個不嚴(yán)格的了解，暫時還不知道其有沒有錯，不過一點可以肯定的是上面定義的Y-組合子只能用于按名調(diào)用的情況，在按值調(diào)用的形式中是無用的，因為對任何g，表達(dá)式Y(jié)g發(fā)散。想要深入理解還是參看一下《類型和程序設(shè)計語言》這本書，不過書中也沒深入的具體分析按值和按名調(diào)用的作用方式。其實這涉及到不同的操作語義的定義。想要在這里弄透還得找找論文看看。

8 參考文獻(xiàn)和外部連接

• School of Computer Science and Software Engineering, Faculty of Information Technology, Monash University, Australia 3800這個大學(xué)的FP課程中的Lambda演算相關(guān)部分http://www.csse.monash.edu.au/~lloyd/tildeFP/Lambda/Ch/
• wikipedia中l(wèi)ambda演算相關(guān)介紹http://en.wikipedia.org/wiki/Lambda_calculus（維基百科好象被封了，中國有關(guān)方面應(yīng)該開放點），不過可以訪問http://en.wikilib.com/wiki/Lambda_calculus（是一個鏡像站點，有中文和英文版）
• 《數(shù)理邏輯與集合論》第二版 清華大學(xué)出版社
• 《類型和程序設(shè)計語言》BC.Pierce 電子工業(yè)出版社（個人認(rèn)為寫得很好，很值得一看）
• 一個blog http://www.aygfsteel.com/wxb_nudt/archive/2005/05/15/4311.aspx