λ演算是一套用于研究函數定義、函數應用和遞歸的形式系統。它由 Alonzo Church 和 Stephen Cole Kleene 在 20 世紀三十年代引入，Church 運用 lambda 演算在 1936 年給出 判定性問題 (Entscheidungsproblem) 的一個否定的答案。這種演算可以用來清晰地定義什么是一個可計算函數。關于兩個 lambda 演算表達式是否等價的命題無法通過一個通用的算法來解決，這是不可判定性能夠證明的頭一個問題，甚至還在停機問題之先。Lambda 演算對函數式編程有巨大的影響，特別是Lisp 語言。
Lambda 演算可以被稱為最小的通用程序設計語言。它包括一條變換規則 (變量替換) 和一條函數定義方式，Lambda 演算之通用在于，任何一個可計算函數都能用這種形式來表達和求值。因而，它是等價于圖靈機的。盡管如此，Lambda 演算強調的是變換規則的運用，而非實現它們的具體機器。可以認為這是一種更接近軟件而非硬件的方式。
歷史
最開始，Church 試圖創制一套完整的形式系統作為數學的基礎，當他發現這個系統易受羅素悖論的影響時，就把 lambda 演算單獨分離出來，用于研究可計算性，最終導致了他對判定性問題的否定回答。
非形式化的描述
在 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)))