λ演算，λ(Lambda（大寫Λ，小寫λ）讀音：lan b（m） da（蘭畝達）['læ;mdə])演算是一套用於研究函式定義、函式套用和遞歸的形式系統。它由 Alonzo Church 和 Stephen Cole Kleene 在 20 世紀三十年代引入，Church 運用 lambda 演算在 1936 年給出 判定性問題 (Entscheidungsproblem) 的一個否定的答案。這種演算可以用來清晰地定義什麼是一個可計算函式。關於兩個 lambda 演算表達式是否等價的命題無法通過一個通用的算法來解決，這是不可判定性能夠證明的頭一個問題，甚至還在停機問題之先。
基本介紹
- 中文名：λ演算
- 外文名：λ-calculus
- 作者：Alonzo Church 與 Stephen C.K.
- 時代：20 世紀三十年代
- 別名：最小的通用程式設計語言
基本概念,非形式化描述,套用,匿名函式,歸約策略,並行與並發,
基本概念
λ 演算可以被稱為最小的通用程式設計語言。它包括一條變換規則 (變數替換) 和一條函式定義方式，λ演算之通用在於，任何一個可計算函式都能用這種形式來表達和求值。因而，它是等價於圖靈機的。儘管如此，λ演算強調的是變換規則的運用，而非實現它們的具體機器。可以認為這是一種更接近軟體而非硬體的方式。它一個數理邏輯形式系統，使用變數代入和置換來研究基於函式定義和套用的計算。希臘字母λ被用來在λ演算模型中表示將一個變數綁定在一個函式中。
λ演算可以是有類型的也可以是無類型的，僅僅當輸入的的數據類型對於有類型的λ演算函式來說是可以接受的時，有類型的λ演算函式才能被使用。λ演算模型在數學，物理學，語言學和計算機科學等不同領域有著廣泛的套用。它在程式語言的理論發展上起到了很重要的作用，並對函式式編程起到了很大的影響，甚至可以說函式式編程就是對λ演算模型的一種實現。同時，它也是範疇論的當前研究對象之一。
λ演算模型最初的形式系統在1935年被 Stephen Kleene 和 J. B. Rosser提出的Kleene–Rosser悖論證明為是前後矛盾的，接著，在1936年，Church單獨出版了λ演算模型中的和純計算有關的部分，也就是如今被稱為的無類型λ演算。在1940年，他提出了一個弱化計算，但是邏輯自洽的形式系統，如今被稱之為簡單類型λ演算。
在20世紀60年代之前，λ演算和程式語言之間的關係被釐清之前，λ演算模型一直都僅僅是一個理論上的形式系統，多虧了Montague和其他的幾位語言學家在自然語言的語義方面的研究，λ演算開始在語言學和計算機科學的研究中占有一席之地。
非形式化描述
在 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 上：λ x. x 3。如果把這個 (用函式作參數的) 函式作用於我們先前的“加 2”函式上：(λ x. x 3) (λ x. x+2)，則明顯地，下述三個表達式：
(λ x. x 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) 被稱為 ω 組合子 (combinator)，((λ x. x x) (λ x. x x)) 被稱為 Ω，而 ((λ x. x x x) (λ x. x x x)) 被稱為 Ω2，以此類推。
若僅有形式化函式作用的註記而不允許 lambda 表達式，就得到了組合子邏輯 (combinatory logic)。
形式化定義
形式化地，我們從一個標識符 (identifier) 的可數無窮集合開始，比如 {a, b, c, ..., x, y, z, x1, x2, ...}，則所有的 lambda 表達式可以通過下述以 BNF 範式表達的上下文無關文法描述：
<expr> ::= <identifier>
<expr> ::= (λ <identifier> . <expr>)
<expr> ::= (<expr> <expr>)
頭兩條規則用來生成函式，而第三條描述了函式是如何作用在參數上的。通常，lambda 抽象 (規則 2) 和函式作用 (規則 3) 中的括弧在不會產生歧義的情況下可以省略。如下假定保證了不會產生歧義：(1) 函式的作用是左結合的，和 (2) lambda 操作符被綁定到它後面的整個表達式。例如，表達式 ((λ x. (x x)) (λ y. y)) 可以簡寫成 (λ x. x x) λ y.y。
類似 λ x. (x y) 這樣的 lambda 表達式並未定義一個函式，因為變元 y 的出現是自由的，即它並沒有被綁定到表達式中的任何一個 λ 上。變元出現次數的綁定是通過下述規則 (基於 lambda 表達式的結構歸納地) 定義的：
在表達式 V 中，V 是變元，則這個表達式里變元 V 只有一次自由出現。
在表達式 λ V . E 中 (V 是變元，E 是另一個表達式)，變元自由出現的次數是 E 中變元自由出現的次數，減去 E 中 V 自由出現的次數。因而，E 中那些 V 被稱為綁定在 λ 上。
在表達式 (E E' ) 中，變元自由出現的次數是 E 和 E' 中變元自由出現次數之和。
在 lambda 表達式的集合上定義了一個等價關係 (在此用 == 標註)，“兩個表達式其實表示的是同一個函式”這樣的直覺性判斷即由此表述，這種等價關係是通過所謂的“alpha-變換規則”和“beta-消解規則”。
α-變換
Alpha-變換規則表達的是，被綁定變數的名稱是不重要的。比如說 λx.x 和 λy.y 是同一個函式。儘管如此，這條規則並非像它看起來這么簡單，關於被綁定的變數能否由另一個替換有一系列的限制。
Alpha-變換規則陳述的是，若 V 與 W 均為變元，E 是一個 lambda 表達式，同時 E[V/W] 是指把表達式 E 中的所有的 V 的自由出現都替換為 W，那么在 W 不是 E 中的一個自由出現，且如果 W 替換了 V，W 不會被 E 中的 λ 綁定的情況下，有
λ V. E == λ W. E[V/W]
這條規則告訴我們，例如 λ x. (λ x. x) x 這樣的表達式和 λ y. (λ x. x) y 是一樣的。
β-消解
Beta-消解規則表達的是函式作用的概念。它陳述了若所有的 E' 的自由出現在 E [V/E' ] 中仍然是自由的情況下，有
((λ V. E ) E' ) == E [V/E' ]
成立。
== 關係被定義為滿足上述兩條規則的最小等價關係 (即在這個等價關係中減去任何一個映射，它將不再是一個等價關係)。
對上述等價關係的一個更具操作性的定義可以這樣獲得：只允許從左至右來套用規則。不允許任何 beta 消解的 lambda 表達式被稱為範式。並非所有的 lambda 表達式都存在與之等價的範式，若存在，則對於相同的形式參數命名而言是唯一的。此外，有一個算法用戶計算範式，不斷地把最左邊的形式參數替換為實際參數，直到無法再作任何可能的消解為止。這個算法若且唯若 lambda 表達式存在一個範式時才會停止。Church-Rosser 定理 說明了，若且唯若兩個表達式等價時，它們會在形式參數換名後得到同一個範式。
η-變換
前兩條規則之後，還可以加入第三條規則，eta-變換，來形成一個新的等價關係。Eta-變換表達的是外延性的概念，在這裡外延性指的是，兩個函式對於所有的參數得到的結果都一致，若且唯若它們是同一個函式。Eta-變換可以令 λ x . f x 和 f 相互轉換，只要 x 不是 f 中的自由出現。下面說明了為何這條規則和外延性是等價的：
若 f 與 g 外延地等價，即，f a == g a 對所有的 lambda 表達式 a 成立，則當取 a 為在 f 中不是自由出現的變數 x 時，我們有 f x == g x，因此 λ x . f x == λ x . g x，由 eta-變換 f == g。所以只要 eta-變換是有效的，會得到外延性也是有效的。
相反地，若外延性是有效的，則由 beta-消解，對所有的 y 有 (λ x . f x) y == f y，可得 λ x . f x == f，即 eta-變換也是有效的。
lambda 演算中的運算
在 lambda 演算中有許多方式都可以定義自然數，但最常見的還是Church 整數，下面是它們的定義：
0 = λ f. λ x. x
1 = λ f. λ x. f x
2 = λ f. λ x. f (f x)
3 = λ f. λ x. f (f (f x))
以此類推。直觀地說，lambda 演算中的數字 n 就是一個把函式 f 作為參數並以 f 的 n 次冪為返回值的函式。換句話說，Church 整數是一個高階函式 -- 以單一參數函式 f 為參數，返回另一個單一參數的函式。
(注意在 Church 原來的 lambda 演算中，lambda 表達式的形式參數在函式體中至少出現一次，這使得我們無法像上面那樣定義 0) 在 Church 整數定義的基礎上，我們可以定義一個後繼函式，它以 n 為參數，返回 n + 1：
SUCC = λ n. λ f. λ x. f (n f x)
加法是這樣定義的：
PLUS = λ m. λ n. λ f. λ x. m f (n f x)
PLUS 可以被看作以兩個自然數為參數的函式，它返回的也是一個自然數。你可以試試驗證
PLUS 2 3 與 5
是否等價。乘法可以這樣定義：
MULT = λ m. λ n. m (PLUS n) 0,
即 m 乘以 n 等於在零的基礎上 n 次加 m。另一種方式是
MULT = λ m. λ n. λ f. m (n f)
正整數 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。
邏輯與斷言
習慣上，下述兩個定義 (稱為 Church 布爾值) 被用作 TRUE 和 FALSE 這樣的布爾值：
TRUE = λ u. λ v. u
FALSE = λ u. λ v. v
斷言是指返回布爾值的函式。最基本的一個斷言 ISZERO，若且唯若其參數為零時返回真：
ISZERO = λ n. n (λ x. FALSE) TRUE
斷言的運用與上述 TRUE 和 FALSE 的定義，使得 "if-then-else" 這類語句很容易用 lambda 演算寫出。
遞歸
遞歸是一種以函式自身疊代自身變元的算法，一般是通過函式自身來定義函式的方式實現。表面看來 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)))
套用
正如Peter Landin1965年在論文 A Correspondence between ALGOL 60 and Church's Lambda-notation中指出的一樣，面向過程的程式設計語言在λ演算模型的體系中是可以理解的，因為它提供了基本的過程抽象和程式套用機制。
匿名函式
以Lisp中的乘方函式為例,它可以使用lambda表達式表達為：
(lambda (x) (* x x))
以上是一個可以用作頭等函式的例子。在這個表達式中，lambda創造了一個匿名函式並給予了它一個參數列表(x),雖然它只有一個參數，而(* x x)則是函式的主體。這個函式在Haskell中的實現是完全一樣的。匿名函式有時候也被叫做lambda表達式。
再舉個例子，Pascal和其它的命令式語言 長期以來都支持將通過函式指針的機制來將子程式 作為參數傳遞到其它子程式裡面去。然而，函式指針並不是 函式成為頭等函式類型的充分條件，因為一個頭等數據類型必須要能夠在運行時創建出一個它的實例。而支持運行時創建函式的語言有Smalltalk,Javascript,和最近的Scala,Eiffel,C#和C++11等。
歸約策略
在程式語言的理論研究中，求值策略(Evaluation strategy)是一組用來確定程式設計語言中的表達式求值的規則。求值策略主要規定了在什麼時候和用什麼樣的順序給函式的實際參數求值，何時把參數代換入函式內，和用怎樣的形式來進行代換。通常，人們使用λ演算模型中的歸約策略來建模求值策略。
無論一個表達式是否為標準狀態，將這個這個表達式化為標準型所需要的工作量很大程度上依賴于歸約策略的使用。而歸約策略的不同又和函式式編程中的及早求值還有惰性求值之間的不同有關。
1.完全β-歸約 (Full β-reduction)
任何參數在任何時候都可以被歸約，其實就是沒有任何的歸約策略，天知道會發生什麼。
2.套用次序 (Applicative order)
最右邊，最內部的表達式總是首先被歸約，直觀上可以知道，這意味著函式的參數總是在函式調用之前就被歸約了。套用次序總是企圖用標準形式去調用函式，即便在很多時候這是不可能的。 大多數的程式設計語言(包括Lisp,ML和命令式語言C和Java等)都被描述為嚴格類型語言，意思是使用了不正確形式參數的函式是形式不正確的。它們在實際上就是使用了套用次序和傳值調用歸約，但通常被成為及早求值策略。
3.正常次序 (Normal order) 最左邊，最外部的表達式總是首先被歸約，這也就意味著無論什麼時候，參數都是再被歸約之前就被替換進了抽象的函式體裡面了。
4.傳名調用 (Call by name) 和正常次序一樣，但是不會在抽象的函式體中再進行歸約，比如說，λx.(λx.x)x在這個策略中是正常形式, 雖然它包含了可歸約的表達式(λx.x)x
5.傳值調用 只有最外部的表達式被歸約:一個表達式僅僅當它的右邊已經被規約為一個值了才會被歸約
6.傳需求調用 “傳需求調用”和傳名調用類似，如果函式的實參被求值了，這個值就會被存儲起來已備未來使用。它產生的結果和傳名調用一樣；但是如果函式的這個實參被調用了多次，那么傳需求調用可以提高程式運行效率。它在現實語境中也被叫做惰性求值。
並行與並發
函式式編程在一開始就是面向並發處理的，這也得益於lambda的性質，lambda演算的Church-Rosser性質意味著歸約(β歸約)可以以任何順序進行，甚至是並行來進行。這意味著各種不同的非確定性歸約策略都是相近的。然而，lambda演算並不提供任何直接的並行結構。一個人可以添加像Futures結構體這樣的並髮結構體到lambda演算中去。相關的進程代數已經為了進程通信和並發而被研究了出來。
在λ-演算的基礎上，發展起來的π-演算、χ-演算，成為近年來的並發程式的理論工具之一，許多經典的並發程式模型就是以π-演算為框架的。
