λ演算
維基百科,自由的 encyclopedia
λ演算(英語:lambda calculus,λ-calculus)是一套從數學邏輯中發展,以變數綁定和替換的規則,來研究函式如何抽象化定義、函式如何被應用以及遞迴的形式系統。它由數學家阿隆佐·邱奇在20世紀30年代首次發表。lambda演算作為一種廣泛用途的計算模型,可以清晰地定義什麼是一個可計算函式,而任何可計算函式都能以這種形式表達和求值,它能模擬單一磁帶圖靈機的計算過程;儘管如此,lambda演算強調的是變換規則的運用,而非實現它們的具體機器。
![]() | 此條目包含過多行話或專業術語,可能需要簡化或提出進一步解釋。 |
lambda演算可比擬是最根本的編程語言,它包括了一條變換規則(變數替換)和一條將函式抽象化定義的方式。因此普遍公認是一種更接近軟體而非硬體的方式。對函數式編程語言造成很大影響,比如Lisp、ML語言和Haskell語言。在1936年邱奇利用λ演算給出了對於判定性問題(Entscheidungsproblem)的否定:關於兩個lambda運算式是否等價的命題,無法由一個「通用的演算法」判斷,這是不可判定效能夠證明的頭一個問題,甚至還在停機問題之先。
lambda演算包括了建構lambda項,和對lambda項執行歸約的操作。在最簡單的lambda演算中,只使用以下的規則來建構lambda項:
More information 語法, 名稱 ...
語法 | 名稱 | 描述 |
---|---|---|
x | 變量 | 用字元或字串來表示參數或者數學上的值或者表示邏輯上的值 |
(λx.M) | 抽象化 | 一個完整的函數定義(M是一個 lambda 項),在表達式中的 x 都會綁定為變量 x。 |
(M N) | 應用 | 將函數M作用於參數N。 M 和 N 是 lambda 項。 |
Close
產生了諸如:(λx.λy.(λz.(λx.zx)(λy.zy))(x y))的表達式。如果表達式是明確而沒有歧義的,則括號可以省略。對於某些應用,其中可能包括了邏輯和數學的常量以及相關操作。
本文討論的是邱奇的「無類型lambda演算」,此後,已經研究出來了一些有類型lambda演算。