複製鏈接
請複製以下鏈接發送給好友
https://baike.baidu.hk/item/λ演算/8019133
複製
複製成功

λ演算

鎖定
λ演算（英語：lambda calculus，λ-calculus）是一套從數學邏輯中發展，以變量綁定和替換的規則，來研究函數如何抽象化定義、函數如何被應用以及遞歸的形式系統。它由數學家阿隆佐·邱奇在20世紀30年代首次發表。lambda演算作為一種廣泛用途的計算模型，可以清晰地定義什麼是一個可計算函數，而任何可計算函數都能以這種形式表達和求值，它能模擬單一磁帶圖靈機的計算過程；儘管如此，lambda演算強調的是變換規則的運用，而非實現它們的具體機器。
中文名
λ演算
外文名
λ-calculus
別    名
最小的通用程序設計語言
作    者
Alonzo Church 與 Stephen C.K.
時    代
20 世紀三十年代

目錄

  1. 1 簡介
  2. 2 發展歷史
  1. 3 非形式化的直覺描述
  1. 4 形式化定義
  2. 5 參見

λ演算簡介

λ演算（英語：lambda calculus，λ-calculus）是一套從數學邏輯中發展，以變量綁定和替換的規則，來研究函數如何抽象化定義、函數如何被應用以及遞歸的形式系統。它由數學家阿隆佐·邱奇在20世紀30年代首次發表。lambda演算作為一種廣泛用途的計算模型，可以清晰地定義什麼是一個可計算函數，而任何可計算函數都能以這種形式表達和求值，它能模擬單一磁帶圖靈機的計算過程；儘管如此，lambda演算強調的是變換規則的運用，而非實現它們的具體機器。
lambda演算可比擬是最根本的編程語言，它包括了一條變換規則（變量替換）和一條將函數抽象化定義的方式。因此普遍公認是一種更接近軟件而非硬件的方式。對函數式編程語言造成很大影響，比如Lisp、ML語言和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演算。 [1] 

λ演算發展歷史

最開始，邱奇試圖創制一套完整的形式系統作為數學的基礎，當他發現這個系統易受羅素悖論的影響時，就把lambda演算單獨分離出來，用於研究可計算性，最終導致了他對判定性問題的否定回答。 [1] 

λ演算非形式化的直覺描述

在λ演算中，每個表達式都代表一個函數，這個函數有一個參數，並且會返回一個值。不論是參數和返回值，也都是一個單參的函數。可以這麼説，λ演算中只有一種“類型”，那就是這種單參函數。函數是通過λ表達式匿名地定義的，這個表達式説明了此函數將對其參數進行什麼操作。
例如，“加2”函數f(x)= x + 2可以用lambda演算表示為λx.x + 2（或者λy.y + 2，參數的取名無關緊要），而f(3)的值可以寫作(λx.x + 2) 3。函數的應用（application）是左結合的：f x y =(f x) y。
考慮這麼一個函數：它把一個函數作為參數，這個函數將被作用在3上：λf.f 3。如果把這個（用函數作參數的）函數作用於我們先前的“加2”函數上：(λf.f 3)(λx.x+2)，則明顯地，下述三個表達式：
  • (λf.f 3)(λx.x+2) 與 (λx.x + 2) 3 與 3 + 2
是等價的。有兩個參數的函數可以通過lambda演算這樣表達：一個單一參數的函數，它的返回值又是一個單一參數的函數（參見柯里化）。例如，函數f(x, y) = x - y可以寫作λx.λy.x - y。下述三個表達式：
  • (λx.λy.x - y) 7 2 與 (λy.7 - y) 2 與 7 - 2
也是等價的。然而這種lambda表達式之間的等價性，無法找到某個通用的函數來判定。
並非所有的lambda表達式都能被歸約至上述那樣的確定值，考慮
  • (λx.x x)(λx.x x)
或
  • (λx.x x x)(λx.x x x)
然後試圖把第一個函數作用在它的參數上。(λx.x x)被稱為ω組合子，((λx.x x)(λx.x x))被稱為Ω，而((λx.x x x) (λx.x x x))被稱為Ω2，以此類推。若僅形式化函數作用的概念而不允許lambda表達式，就得到了組合子邏輯。 [1] 

λ演算形式化定義

形式化地，我們從一個標識符（identifier）的可數無窮集合開始，比如{a, b, c, ..., x, y, z, x1, x2, ...}，則所有的lambda表達式可以通過下述以BNF範式表達的上下文無關文法描述：
  1. <表達式>::= <標識符>
  2. <表達式>::= (λ<標識符>.<表達式>)
  3. <表達式>::= (<表達式> <表達式>)
頭兩條規則用來生成函數，而第三條描述了函數是如何作用在參數上的。通常，lambda抽象（規則2）和函數作用（規則3）中的括弧在不會產生歧義的情況下可以省略。如下假定保證了不會產生歧義：（1）函數的作用是左結合的，和（2）lambda操作符被綁定到它後面的整個表達式。例如，表達式 (λx.x x)(λy.y) 可以簡寫成λ(x.x x) λy.y 。
類似λx.(x y)這樣的lambda表達式並未定義一個函數，因為變量y的出現是自由的，即它並沒有被綁定到表達式中的任何一個λ上。一個lambda表達式的自由變量的集合是通過下述規則（基於lambda表達式的結構歸納地）定義的：
  1. 在表達式V中，V是變量，則這個表達式裏自由變量的集合只有V。
  2. 在表達式λV .E中（V是變量，E是另一個表達式），自由變量的集合是E中自由變量的集合減去變量V。因而，E中那些V被稱為綁定在λ上。
  3. 在表達式 (E E')中，自由變量的集合是E和E'中自由變量集合的並集。
例，對於表達式λx.x（我們將第一個x視作變量，第二個x視作表達式），其中表達式x中，由1，它的自由變量集合是x，又由2，表達式λx.x的自由變量的集合是表達式x的自由變量集合減去變量x。所以對於表達式λx.x，它的自由變量集合是空。
例，對於表達式λx.x x由形式化描述的第3點，我們把它看作((λx.x)(x))，(λx.x)和(x)分別為表達式，由上一例知道(λx.x)的自由變量集合為空，表達式(x)的變量集合為變量x，所以對於λx.x x，它的自由變量集合為x與空的並，即x。
在lambda表達式的集合上定義了一個等價關係(在此用==標註)，“兩個表達式其實表示的是同一個函數”這樣的直覺性判斷即由此表述，這種等價關係是通過所謂的“alpha-變換規則”和“beta-歸約規則”。 [1] 

λ演算參見

參考資料
  • 1.    Alonzo Church, The Calculi of Lambda-Conversion (ISBN 978-0-691-08394-0)[1]