Lambda 演算
Lambda 演算是可計算函式的理論，即一個形式系統，它形式化了可計算函式的抽象概念。該演算由阿隆佐·丘奇在 1930 年代開發，當時其他研究人員也開發了其他計算模型，這些模型後來被證明是等效的。S. C. 克萊尼開發了遞迴函式，艾倫·麥席森·圖靈開發了一種通用抽象機器，後來被稱為通用圖靈機，以及其他形式系統。遞迴函式可以在 lambda 演算中表達，反之亦然，通用圖靈機也可以在 lambda 演算中定義，遞迴函式和 lambda 演算可以在通用圖靈機中定義，其他未在此處描述的計算模型也是如此。每次嘗試構建一個系統來捕捉計算概念的結果都是一個等效的理論，這是一個強烈的跡象，表明不存在其他“更強大”的系統，這無法被證明，因此被稱為丘奇-圖靈論題。換句話說，它指出任何可計算函式都可以在這些系統中的任何一箇中被定義。你可能注意到形式系統、理論和模型用於指代這些形式主義，讓我們說一下這意味著什麼。形式理論是一個形式系統，它捕捉了可計算函式的抽象概念。
Lambda 演算是計算機科學的一個基礎，就像微積分是牛頓物理學的基礎一樣。另一個基礎是馮·諾依曼機，它是通用圖靈機的硬體實現，當然作為任何物理實現，它具有有限的記憶體。
Lambda 演算作為函數語言程式設計語言的基礎，就像馮·諾依曼機是指令式程式設計語言的基礎一樣。
計算機科學中一個重要的主題是程式語言的語義，即如何說明程式語言的含義。Lambda 演算是丹娜·斯科特開發的指稱語義的基礎。
在 lambda 演算中研究了不同的 lambda 理論。無型別 lambda 演算導致了一個不一致的理論，因為存在一個等價於樸素集合論中羅素悖論的悖論。這促使人們開發了有型別 lambda 理論。
無型別 lambda 演算公式是從一個無限的變數集 、形式為 的抽象，其中 是一個變數，而 是 lambda 演算公式，也稱為 lambda 項，最後一個是形式為 的應用，其中 和 也是 lambda 項，僅此而已。
存在轉換規則， 和 定義如下
