Λ演算

λ演算(英語:lambda calculus,λ-calculus)是一套從數學邏輯中發展,以變數綁定和替換的規則,來研究函式如何抽象化定義、函式如何被應用以及遞迴形式系統。它由數學家阿隆佐·邱奇在20世紀30年代首次發表。Lambda演算作為一種廣泛用途的計算模型,可以清晰地定義什麼是一個可計算函式,而任何可計算函式都能以這種形式表達和求值,它能模擬單一磁帶图灵机的計算過程;儘管如此,Lambda演算強調的是變換規則的運用,而非實現它們的具體機器。

Lambda演算可比擬是最根本的編程語言,它包括了一條變換規則(變數替換)和一條將函式抽象化定義的方式。因此普遍公認是一種更接近軟體而非硬體的方式。對函數式編程語言造成很大影響,比如LispML语言Haskell语言。在1936年邱奇利用λ演算給出了對於判定性問題(Entscheidungsproblem)的否定:關於兩個lambda運算式是否等價的命題,無法由一個「通用的演算法」判斷,這是不可判定效能夠證明的頭一個問題,甚至還在停机问题之先。

Lambda演算包括了建構lambda項,和對lambda項執行歸約的操作。在最簡單的lambda演算中,只使用以下的規則來建構lambda項:

語法名稱描述
a變量表示參數或數學/邏輯值的字元或字串
(λx.M)抽象化函數定義(M是一個lambda項)。變量x在表達式中已被綁定。
(M N)應用將函數應用於參數。 M 和 N 是 lambda 項。

產生了諸如:(λx.λy.(λz.(λx.zx)(λy.zy))(x y))的表達式。如果表達式是明確而沒有歧義的,則括號可以省略。對於某些應用,其中可能包括了邏輯和數學的常量以及相關操作。

本文讨论的是邱奇的“无类型lambda演算”,此后,已经研究出来了一些有类型lambda演算

其他语言
bosanski: Lambda račun
нохчийн: Лямбда-ларар
čeština: Lambda kalkul
Ελληνικά: Λογισμός λάμδα
Esperanto: Lambda-kalkulo
español: Cálculo lambda
فارسی: جبر لاندا
français: Lambda-calcul
hrvatski: Lambda račun
italiano: Lambda calcolo
日本語: ラムダ計算
한국어: 람다 대수
Nederlands: Lambdacalculus
português: Cálculo lambda
srpskohrvatski / српскохрватски: Lambda račun
Simple English: Lambda calculus
slovenčina: Lambda kalkul
српски / srpski: Ламбда рачун
svenska: Lambdakalkyl
українська: Лямбда-числення
Tiếng Việt: Phép tính lambda