簡單λ演算
Lambda演算簡介：
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.
λ演算是一套用于研究函數定義、函數應用和遞歸的形式系統。它由 Alonzo Church 和 Stephen Cole Kleene 在 20 世紀三十年代引入，Church 運用 lambda 演算在 1936 年給出 判定性問題 (Entscheidungsproblem) 的一個否定的答案。這種演算可以用來清晰地定義什么是一個可計算函數。關于兩個 lambda 演算表達式是否等價的命題無法通過一個通用的算法來解決，這是不可判定性能夠證明的頭一個問題，甚至還在停機問題之先。Lambda 演算對函數式編程有巨大的影響，特別是Lisp 語言。
同時，數理邏輯中對于lambda演算的介紹就簡單得多：
λ-演算可以說是最簡單、最小的一個形式系統。它是在二十世紀三十年代由Alonzo Church 和 Stephen Cole Kleene發明的。至今，在歐洲得到了廣泛的發展。可以說，歐洲的計算機科學是從λ-演算開始的，而現在仍然是歐洲計算機科學的基礎，首先它是函數式程序理論的基礎，而后，在λ-演算的基礎上，發展起來的π-演算、χ-演算，成為近年來的并發程序的理論工具之一，許多經典的并發程序模型就是以π-演算為框架的。
Lambda 演算可以被稱為最小的通用程序設計語言。它包括一條變換規則 (變量替換) 和一條函數定義方式，Lambda 演算之通用在于，任何一個可計算函數都能用這種形式來表達和求值。因而，它是等價于圖靈機的。盡管如此，Lambda 演算強調的是變換規則的運用，而非實現它們的具體機器。可以認為這是一種更接近軟件而非硬件的方式。 Lambda演算表達了兩個計算機計算中最基本的概念“代入”和“置換”。“代入”我們一般理解為函數調用，或者是用實參代替函數中的形參；“置換”我們一般理解為變量換名規則。后面會講到，“代入”就是用lambda演算中的β-歸約概念。而“替換”就是lambda演算中的α-變換。
目錄
- 1 歷史
- 2 非形式化的描述
- 3 形式化的定義
-
- 3.1字母表
- 3.2 λ-項
- 3.3 公式
- 3.4 λ-項中的變量自由出現法則
- 3.5 λ x的控制域
- 4 變換與等價關系
-
- 4.1 α-變換
- 4.2 β-歸約
- 4.3 等價關系
- 4.4 η-變換
- 5 λ演算的操作語義
- 6 λ演算的公理化和定理
-
- 6.1 λ演算的公理
- 6.2 不動點理論
- 6.3 Church-Rosser定理及其等價定理
- 7 lambda 演算中的程序設計
-
- 7.1 自然數與運算
- 7.2 邏輯與斷言
- 7.3 遞歸
- 8 參考文獻和外部鏈接
|
1 歷史
最開始，Church 試圖創制一套完整的形式系統作為數學的基礎，當他發現這個系統易受羅素悖論的影響時，就把 lambda 演算單獨分離出來，用于研究可計算性，最終導致了他對判定性問題的否定回答。
2 非形式化的描述
在 lambda 演算中，每個表達式都代表一個只有單獨參數的函數，這個函數的參數本身也是一個只有單一參數的函數，同時，函數的值是又一個只有單一參數的函數。函數是通過 lambda 表達式匿名地定義的，這個表達式說明了此函數將對其參數進行什么操作。例如，“加 2”函數 f(x) = x + 2 可以用 lambda 演算表示為 λ x. x + 2 (λ y. y + 2 也是一樣的，參數的取名無關緊要) 而 f(3) 的值可以寫作 (λ x. x + 2) 3。函數的作用 (application) 是左結合的：f x y = (f x) y。考慮這么一個函數：它把一個函數作為參數，這個函數將被作用在 3 上：λ f. f 3。如果把這個 (用函數作參數的) 函數作用于我們先前的“加 2”函數上：(λ f. f 3) (λ x. x+2)，則明顯地，下述三個表達式：
(λ f. f 3) (λ x. x+2) 與 (λ x. x + 2) 3 與 3 + 2
是等價的。有兩個參數的函數可以通過 lambda 演算這么表達：一個單一參數的函數的返回值又是一個單一參數的函數 (參見 Currying)。例如，函數 f(x, y) = x - y 可以寫作 λ x. λ y. x - y。下述三個表達式：
(λ x. λ y. x - y) 7 2 與 (λ y. 7 - y) 2 與 7 - 2
也是等價的。然而這種 lambda 表達式之間的等價性無法找到一個通用的函數來判定。
并非所有的 lambda 表達式都可以規約至上述那樣的確定值，考慮
(λ x. x x) (λ x. x x)
或
(λ x. x x x) (λ x. x x x)
然后試圖把第一個函數作用在它的參數上。 (λ x. x x) 被稱為 ω 組合子，((λ x. x x) (λ x. x x)) 被稱為 Ω，而 ((λ x. x x x) (λ x. x x x)) 被稱為 Ω2，以此類推。
若僅形式化函數作用的概念而不允許 lambda 表達式，就得到了組合子邏輯。
3 形式化的定義
3.1字母表
lambda演算系統中合法的字符如下：
1. 標識符 (identifier) 的可數無窮集合：{ x1，x2，x3，…}變元（變元的數量是無窮的，不能在有限步驟內窮舉，這個很重要，后面有定理是根據這一點證明的）
2. à 歸約
3. 等價
4. λ，（，） （輔助工具符號，一共有三個，λ和左括號右括號）
所有能夠在lambda演算系統中出現的合法符號只有以上四種，其他符號都是非法的。例如λx.x+2，如果沒有其他對于＋符號的說明，那么這就是一個非法的λ演算表達式。
3.2 λ-項
λ-項在一些文章中也稱為λ表達式（lambda expression），它是由上面字母表中的合法字符組成的表達式，合法的表達式組成規則如下：
1. 任一個變元是一個項
2. 若M，N是項，則（MN）也是一個項 （function application，函數應用）
3. 若M是一個項，而x是一個變元，則（λx.M）也是一個項 （function abstraction，函數抽象）
4. 僅僅由以上規則歸納定義得到的符號串是項
則所有的 lambda 表達式可以通過下述以 BNF 范式表達的上下文無關文法描述：
- <expr> ::= <identifier>
- <expr> ::= (λ <identifier> . <expr>)
- <expr> ::= (<expr> <expr>)
說明1：通常，lambda 抽象 (規則 2) 和函數作用 (規則 3) 中的括號在不會產生歧義的情況下可以省略。如下假定保證了不會產生歧義：
(1) 函數的作用是左結合的。
(2) lambda 操作符被綁定到它后面的整個表達式。
例如，表達式 ((λ x. (x x)) (λ y. y)) 可以簡寫成 (λ x. x x) λ y.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都僅僅是一個變量而已，談不上函數代入。
說明4：這里的另一難點就是要區分變量和元變量，如：M＝λx.x，這里x為變量，是我們在語法系統中定義了的，而M為元變量，沒有在語法系統中定義，是我們用來表示的助記符。我們必須根據上下文來區分誰是變量，誰是元變量。
上面是λ-項的形式化定義，有一些是可以與函數理論直觀聯系的，而另一些只是說明這個λ-項是合法的，不一定有直觀的字面意義。
3.3 公式
若M，N是λ-項，則MàN，M N是公式。
3.4 λ-項中的變量自由出現法則
類似 λ x. (x y) 這樣的 lambda 表達式并未定義一個函數，因為變量 y 的出現是自由的，即它并沒有被綁定到表達式中的任何一個 λ 上。在一個λ-項中，變量要么是自由出現的，要么是被一個λ符號綁定的。還是以函數的方式來理解變量的自由出現和綁定。例如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) 萛\nfree(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的。
一個不含自由變量的項稱為封閉項；封閉項也稱為組合子。最簡單的組合子，稱為恒等函數：id=λx.x
3.5 λ x的控制域
來看兩個λ-項，λx.xx和λx.(xx)有何不同？根據左結合的法則，λx.xx＝(λx.x)x，其中第一個x是被λ綁定的，而第二個x則是自由出現的。而λx.(xx)中兩個x都是被λ綁定的。這表明了兩個λ-項中λx的控制域是不同的。
我們知道謂詞演算中量詞也是有控制域的，λx的控制域與它們類似，這里就不給出詳細的定義了。其實也很直觀。
4 變換與等價關系
4.1 α-變換
α-變換規則表達的是，被綁定變量的名稱是不重要的。比如說 λ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中的一個λ綁定。即：替換的變元不能在M中自由出現，并且也只替換M中的自由變元
這條規則告訴我們，例如 λ x. (λ x. x) x 這樣的表達式和 λ 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
α-變換主要用來表達函數中的變量換名規則，需要注意的是被換名的只能是M（函數體）中變量的自由出現。
4.2 β-歸約
β-歸約表達的是函數應用或者函數代入的概念。前面提到MN是合法的λ-項，那么MN的含義是將M應用到N，通俗的說是將N作為實參代替M中的約束變量，也就是形參。β-歸約的規則如下：
(λx.M)N à M[x/N] 如果N中所有變量的自由出現都在M[x/N]中保持自由出現
注意： (lx. ly.(y x))y ?ly.(y y)是錯的，應為y在ly.(y x)中不自由出現，這時要歸約就應該先用α-變換把ly.(y x)中的y換成其他變元
β-歸約是λ演算中最重要的概念和規則，它是函數代入這個概念的形式化表示。
一些例子如下：
(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
需要多加練習才能習慣這種歸約。
4.3 等價關系
在 lambda 表達式的集合上定義了一個等價關系 (在此用 標注)，“兩個表達式其實表示的是同一個函數”這樣的直覺性判斷即由此表述，這種等價關系是通過所謂的“alpha-變換規則”和“beta-歸約規則”得到的。
f g:當且僅當（1）g≌f ;(2)g甪 or f甮 ;(3)存在h，f h且h g之一成立。
關系被定義為滿足上述規則的最小等價關系 (即在這個等價關系中減去任何一個映射，它將不再是一個等價關系)。
4.4 η-變換
前兩條規則之后，還可以加入第三條規則，η-變換，來形成一個新的等價關系。η-變換表達的是外延性的概念，在這里外延性指的是，兩個函數對于所有的參數得到的結果都一致，當且僅當它們是同一個函數。
η-變換：λ x . f x f，只要 x 不是 f 中的自由出現。
f 與 g 外延的等價：對任意lambda 表達式 a，如果有f a g a成立，則f g也成立。
下面說明了為何這條規則和外延性是等價的：（即由η-變換可以證明外延等價，相反由外延等價也可以證明η-變換）
f a g a 對所有的 lambda 表達式 a 成立，則當取 a 為在 f 中不是自由出現的變量 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.。
通俗的說法是，將一個λ-項進行β-歸約，也就是進行實參代入形參的過程，如果通過有窮步代入，可以得到一個不能夠再進行代入的λ-項，那么這就是它的范式。如果無論怎樣代入，總存在可以繼續代入的子項，那么它就沒有范式。
例子
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。
一般的把一個λ-項規約為范式的過程稱為求值，范式也叫做值。在《類型和程序設計語言》一書中，作者給出了λ-演算中的幾種不同的求值策略。每個策略確定一個項在下一步求值中激活哪一個約式或幾個約式。
注意到在求值的過程中是左結合，并且當且僅當左邊以是值了才能對右邊的項進一步求值
6 λ演算的公理化和定理
6.1 λ演算的公理
這一段來自《數理邏輯與集合論》（第二版 清華大學出版社）。
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’
13．M≌N => MàN 如果y沒有在M中自由出現，并且只要y替換M中的x，都不會被M中的一個λ綁定。
如果某一公式MàN或者M N可以用以上的公理推出，則記為λ├MàN和λ├M N。
規則13可以加也可以不要，要了表示是考慮α-變換的系統
6.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)…)))。
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。（規約的合流性）
推論：MàN1,MàN2 且N1,N2都是范式 則N1≌N2 (范式在α-變換下的唯一性)
關系被定義為滿足上述兩條規則的最小等價關系 (即在這個等價關系中減去任何一個映射，它將不再是一個等價關系)。
對上述等價關系的一個更具操作性的定義可以這樣獲得：只允許從左至右來應用規則。不允許任何 beta 歸約的 lambda 表達式被稱為范式。并非所有的 lambda 表達式都存在與之等價的范式，若存在，則對于相同的形式參數命名而言是唯一的。此外，有一個算法用來計算范式，不斷地把最左邊的形式參數替換為實際參數，直到無法再作任何可能的規約為止。這個算法當且僅當 lambda 表達式存在一個范式時才會停止。Church-Rosser 定理 說明了，當且僅當兩個表達式等價時，它們會在形式參數換名后得到同一個范式。
7 lambda 演算中的程序設計
7.1 自然數與運算
在 lambda 演算中有許多方式都可以定義自然數，但最常見的還是邱奇數，下面是它們的定義：
0 = λ s. λ z. z
1 =λ s. λ z.. s z
2 =λ s. λ z. s (s z)
3 =λ s. λ z. s (s (s z))
以此類推。直觀地說，lambda 演算中的數字 n 就是一個把函數 f 作為參數并以 f 的 n 次冪為返回值的函數。換句話說，Church 整數是一個高階函數 -- 以單一參數函數 f 為參數，返回另一個單一參數的函數。
(注意在 Church 原來的 lambda 演算中，lambda 表達式的形式參數在函數體中至少出現一次，這使得我們無法像上面那樣定義 0) 在 Church 整數定義的基礎上，我們可以定義一個后繼函數，它以 n 為參數，返回 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 可以被看作以兩個自然數為參數的函數，它返回的也是一個自然數。你可以試驗證
PLUS 2 3 與 5
是否等價。乘法可以這樣定義：
MULT = λ m. λ n. m (PLUS n) 0,
MULT2 =λ m. λ n. λ s. λ z. m (n s) z
即 m 乘以 n 等于在零的基礎上 n 次加 m。更簡潔的一種方式是
MULT3 = λ m. λ n. λ s. m (n s)
冪的定義：
POWER1 = λ m. λ n. m (MULT n) 1
POWER2 = λ m. λ n. m n (可能有點問題，我驗證了好象不正確)
正整數 n 的前驅元 (predecessesor) PRED n = n - 1 要復雜一些：
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 表示的是，當 g(1) 是零時，表達式的值是 k，否則是 g(k) + 1。
在《類型和程序設計語言》一書中作者對于數和各種運算的編碼描述得比較清晰，強烈建議看以下，并且作者還介紹了直接基于原始的布爾類型和數型的系統，簡稱為λNB，并給出了這兩套系統之間的轉換。
7.2 邏輯與斷言
習慣上，下述兩個定義 (稱為 Church 布爾值) 被用作 TRUE 和 FALSE 這樣的布爾值：
tru = λ u. λ v. u
fls = λ u. λ v. v
這樣我們可以定義一個組合式test=λl.λm.λ n.lmn，使得b為tru時，test b v w規約為v，而當b為fls時，test b v w規約為w。
并且我們還可以定義邏輯連接詞：
and = λb. λc. b c fls
or =λb. λc. b c tru
not =λb. b fls tru
斷言是指返回布爾值的函數。最基本的一個斷言 ISZERO，當且僅當其參數為零時返回真：
ISZERO = λ n. n (λ x. fls) tru
斷言的運用與上述 TRUE 和 FALSE 的定義，使得 "if-then-else" 這類語句很容易用 lambda 演算寫出。
7.3 遞歸
遞歸是一種以函數自身迭代自身變元的算法，一般是通過函數自身來定義函數的方式實現。表面看來 lambda 演算不允許遞歸，其實這是一種對遞歸的誤解。考慮階乘函數 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)))
這一節我也沒分析透徹，只能原本引用，并且以上的內容也只能當作一個不嚴格的了解，暫時還不知道其有沒有錯，不過一點可以肯定的是上面定義的Y-組合子只能用于按名調用的情況，在按值調用的形式中是無用的，因為對任何g，表達式Yg發散。想要深入理解還是參看一下《類型和程序設計語言》這本書，不過書中也沒深入的具體分析按值和按名調用的作用方式。其實這涉及到不同的操作語義的定義。想要在這里弄透還得找找論文看看。
8 參考文獻和外部連接
posted @
2007-07-16 16:43 饅頭 閱讀(410) |
評論 (0) |
編輯 收藏