λ演算（也寫作λ-calculus）是數學邏輯中的一個形式系統，用于表達基于函數抽象和應用的計算，使用變量綁定和替換。 它是一種通用計算模型，可用于模擬任何圖靈機。 它由數學家阿朗佐丘奇在 1930 年代引入，作為他對數學基礎研究的一部分。

λ演算包括構造 § lambda 項并對它們執行 § 縮減操作。 在最簡單的 lambda 演算形式中，項僅使用以下規則構建：

• x {\displaystyle x} – 變量，表示參數或數學/邏輯值的字符或字符串。
• ( λ x . M ) {\textstyle (\lambda x.M)} – 抽象，函數定義（M {\textstyle M} 是一個 lambda 項）。 變量 x {\textstyle x} 在表達式中綁定。
• ( M N ) {\displaystyle (M\ N)} – 應用程序，將函數 M {\textstyle M} 應用于參數 N {\textstyle N} 。 M {\textstyle M} 和 N {\textstyle N} 是 lambda 項。

減少操作包括：

• ( λ x . M [ x ] ) → ( λ y . M [ y ] ) {\textstyle (\lambda x.M[x])\rightarrow (\lambda y.M[y])} – α -轉換，重命名表達式中的綁定變量。 用于避免名稱沖突。
• ( ( λ x . M ) E ) → ( M [ x := E ] ) {\textstyle ((\lambda x.M)\ E)\rightarrow (M[x:=E])} – β-reduction，用抽象主體中的參數表達式替換綁定變量。

如果使用 De Bruijn 索引，則不再需要 α 轉換，因為不會發生名稱沖突。 如果減少步驟的重復應用最終終止，那么根據 Church-Rosser 定理，它將產生 β-正規形式。

如果使用通用的 lambda 函數（例如 Iota 和 Jot），則不需要變量名，它們可以通過以各種組合調用自身來創建任何函數行為。

λ演算是圖靈完備的，也就是說，它是一個通用的計算模型，可以用來模擬任何圖靈機。 與它同名的希臘字母 lambda (λ) 在 lambda 表達式和 lambda 術語中用于表示綁定函數中的變量。

λ演算可以是無類型的或有類型的。 在類型化 lambda 演算中，只有當函數能夠接受給定輸入的數據類型時才能應用函數。 有類型的 lambda 演算比無類型的 lambda 演算弱，這是本文的主要主題，因為有類型的 lambda 演算可以表達的比無類型的演算少，但另一方面，有類型的 lambda 演算可以證明更多的東西 ; 例如，在簡單類型的 lambda 演算中，它是一個定理，即每個評估策略都會針對每個簡單類型的 lambda 項終止，而無類型 lambda 項的評估不需要終止。 有許多不同類型的 lambda 演算的原因之一是希望在不放棄能夠證明關于微積分的強定理的情況下做更多（無類型演算可以做的事情）。

λ演算在數學、哲學、語言學和計算機科學的許多不同領域都有應用。 λ演算在編程語言理論的發展中發揮了重要作用。 函數式編程語言實現了 lambda 演算。 λ演算也是范疇論當前的一個研究課題。

lambda 演算由數學家 Alonzo Church 在 1930 年代引入，作為對數學基礎研究的一部分。 1935 年，斯蒂芬·克林 (Stephen Kleene) 和 J. B. 羅瑟 (J. B. Rosser) 提出了克林-羅瑟悖論，證明原始系統在邏輯上是不一致的。

隨后，丘奇在 1936 年分離并發表了與計算相關的部分，即現在所謂的無類型 lambda 演算。 1940 年，他還引入了一種計算能力較弱但邏輯一致的系統，稱為簡單類型 lambda 演算。

直到 1960 年代它與編程語言的關系被闡明之前，lambda 演算只是一種形式主義。

由于 Richard Montague 等語言學家在自然語言語義學上的應用，lambda 演算開始在語言學和計算機科學中享有重要地位。

Church 使用希臘字母 lambda (λ) 作為 lambda 演算中函數抽象符號的原因尚不確定，部分原因可能是 Church 自己的解釋相互矛盾。 根據 Cardone 和 Hindley (2006)：

順便問一下，丘奇為什么選擇符號“λ”？ 在 [一封未發表的 1964 年寫給 Harald Dickson 的信中]，他明確指出它來自懷特海和羅素用于類抽象的符號“ x ^ {\displaystyle {\hat {x}}} ”，首先修改“ x ^ {\displaystyle {\hat {x}}} ” 到 “ ∧ x {\displaystyle \land x} ” 來區分函數。