Lambda calculus



http://zh.wikipedia.org/wiki/Lambda_%E6%BC%94%E7%AE%97

λ演算lambda calculus)是一套用於研究函數定義、函數應用和遞歸形式系統。它由阿隆佐·邱奇和他的學生史蒂芬·科爾·克萊尼20世紀30年代引入。邱奇運用λ演算在1936年給出判定性問題(Entscheidungsproblem)的一個否定的答案。這種演算可以用來清晰地定義什麼是一個可計算函數。關於兩個lambda演算表達式是否等價的命題無法通過一個「通用的演算法」來解決,這是不可判定性能夠證明的頭一個問題,甚至還在停機問題之先。Lambda演算對函數式程式語言有巨大的影響,比如Lisp語言ML語言Haskell語言

Lambda演算可以被稱為最小的通用程式語言。它包括一條變換規則(變數替換)和一條函數定義方式,Lambda演算之通用在於,任何一個可計算函數都能用這種形式來表達和求值。因而,它是等價於圖靈機的。儘管如此,Lambda演算強調的是變換規則的運用,而非實現它們的具體機器。可以認為這是一種更接近軟體而非硬體的方式。




Comments