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

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

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

語法 名稱 描述
x 變數 用字元或字串來表示參數或者數學上的值或者表示邏輯上的值
(λx.M) 抽象化 一個完整的函式定義(M是一個 lambda 項),在表達式中的 x 都會綁定為變數 x。
(M N) 應用 將函式M作用於參數N。 M 和 N 是 lambda 項。

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

本文討論的是邱奇的「無類型lambda演算」,此後,已經研究出來了一些有類型lambda演算

解釋與應用

編輯

λ演算是圖靈完備的,也就是說,這是一個可以用於類比任何圖靈機的通用模型[1] λ也被用在λ表達式λ項中,用來表示將一個變數繫結在一個函式上。

λ演算可以是有類型或者無類型的,在有類型λ演算中(上文所述是無類型的),函式只能在參數類型和輸入類型符合時被應用。有類型λ演算比無類型λ演算要弱——後者是這個條目的主要部分——因為有類型的λ運算能表達的比無類型λ演算少;與此同時,前者使得更多定理能被證明。例如,在簡單類型λ演算中,運算總是能夠停止,然而無類型λ演算中這是不一定的(因為停機問題)。目前有許多種有類型λ演算的一個原因是它們被期望能做到更多(做到某些以前的有類型λ演算做不到的)的同時又希望能用以證明更多定理。

λ演算在數學哲學[2]語言學[3][4]電腦科學[5]中都有許多應用。它在程式語言理論中占有重要地位,函數式程式設計實現了λ演算支援。λ演算在範疇論中也是一個研究熱點。[6]

歷史

編輯

作為對數學基礎研究的一部分,數學家阿隆佐·邱奇在20世紀30年代提出了λ演算。[7][8] 但最初的λ演算系統被證明是邏輯上不自洽的——在1935年史蒂芬·科爾·克萊尼J. B. Rosser舉出了Kleene-Rosser悖論英語Kleene–Rosser paradox[9][10]

隨後,在1936年邱奇把那個版本的關於計算的部分抽出獨立發表—現在這被稱為無類型λ演算。[11] 在1940年,他創立了一個計算能力更弱但是邏輯上自洽的系統,這被稱為簡單類型λ演算[12]

直到1960年,λ演算與程式語言的關係被確立了;在這之前它只是一個範式。由於理察·蒙塔古和其他語言學家將λ演算應用於自然語言語法的研究,λ演算已經開始在語言學[13]和電腦科學學界擁有一席之地。[14]

至於為何邱奇選擇λ作為符號,連他本人的解釋也互相矛盾:最初是在1964年的一封信中,他明確解釋稱這是來源於《數學原理》一書中的類抽象符號(脫字元),為了方便閱讀,他首先將其換成邏輯與符號( )作為區分,然後又改成形狀類似的λ。他在1984年又重申了這一點,但再後來他又表示選擇λ純粹是偶然[15]

非形式化的直覺描述

編輯

在λ演算中,每個表達式都代表一個函式,這個函式有一個參數,並且會返回一個值。不論是參數和返回值,也都是一個單參的函式。可以這麼說,λ演算中只有一種「類型」,那就是這種一元函式。函式是通過λ表達式匿名地定義的,這個表達式說明了此函式將對其參數進行什麼操作。

例如,「加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表達式,就得到了組合子邏輯

動機

編輯

在數學和電腦科學中,「可計算的」函式是基礎觀念。對於所謂的可計算性,λ-演算提供了一個簡單明確的語義,使計算的性質可以被形式化研究。λ-演算結合了兩種簡化方式,使得這個語義變得簡單。第一種簡化是不給予函式一個確定名稱,而「匿名」地對待它們。例如,兩數的平方和函式

 

可以用匿名的形式重新寫為:

 (理解成一包含xy的數組被對映到 

同樣地,

 

可以用匿名的形式重新寫為:

 (即輸入是直接對應到它本身。)

第二個簡化是λ演算只使用單一個參數輸入的函式。如果普通函式需要兩個參數,例如 函式,可轉成接受單一參數,傳給另一個函式中介,而中介函式也只接受一個參數,最後輸出結果。例如,

 

可以重新寫成:

 

這是稱為柯里化的方法,將多參數的函式轉換成為多個中介函式的複合鏈,每個中介函式都只接受一個參數。 將 函式應用於參數(5,2),直接產生結果

 
 
 ,

而對於柯里化轉換版的評估,需要再多一步:

 
  //在內層表達式中 的定義為 ,這就像β-歸約一樣。
  // 的定義為 ,再次如同β-歸約。
 

得出相同結果。

lambda演算

編輯

lambda演算是由特定形式語法所組成的一種語言,一組轉換規則可操作其中的lambda項。這些轉換規則被看作是一個等式理論或者一個操作定義。如上節所述,lambda演算中的所有函式都是匿名的,它們沒有名稱,它們只接受一個輸入變數,柯里化用於實現有多個輸入變數的函式。

lambda項

編輯

lambda演算的語法將一些表達式定義為有效的lambda演算式,而某一些表達式無效,就像C程式語言中有些字串有效,有些則不是。有效的lambda演算式稱為「lambda項」。

以下三個規則給出了語法上有效的lambda項,如何建構的歸納定義:

  • 變數 本身就是一個有效的lambda項
  • 如果 是一個lambda項,而 是一個變數,則  是一個lambda項(稱為lambda抽象);
  • 如果  是lambda項,那麼 是一個lambda項(稱為應用)。

其它的都不是lambda項。因此,lambda項若且唯若可重複應用這三個規則取得時,才是有效的。一些括號根據某些規則可以省略。例如,最外面的括號通常不會寫入。

「lambda抽象」是指一個匿名函式的定義,它將單一輸入的 替換成 的表達式,所以產生了一個匿名函式,它採用 的值並返回 。例如, 是表示使用函式 作為 項的一個lambda抽象。lambda抽象只是先「設定」了函式定義,還沒使用它。這個抽象在 項中綁定了變數 。一個應用 表示將函式 應用在輸入 ,亦即對輸入 使用函式 產生 

lambda演算中並沒有變數聲明的概念。如 (即 )的定義中,lambda演算將 當作尚未定義的變數。lambda抽象 在語法上是有效的,並表示將其輸入添加到未知 的函式。

可用圓括弧對來消除歧義。例如,  表示不同的項(儘管它們剛好化簡到相同值)。這裡第一個例子定義了一個包含子函式的抽象,並將子函式應用於x(先應用後傳回)的結果;而第二個例子定義了一個傳回任何輸入的函式,然後在應用過程中傳回對輸入為x的應用(返回函式然後應用)。

操作函式的函式

編輯

在lambda演算中,函式被認為是頭等物件,因此函式可以當作輸入,或作為其它函式的輸出返回。

例如, 表示對映到本身的函式,  表示將這個函式應用於 。此外, 則表示無論輸入為何,始終返回 值的常數函式 。lambda演算中的函式應用是左結合的,因此 表示 

有幾個「等價」和「化簡」的概念,允許將各個lambda項「縮減」為「相同」的lambda項。

α-等價

編輯

對於lambda項,等價的基本形式定義,是 -等價。它捕捉了直覺概念,在lambda抽象中一個綁定變數的特別選擇(通常)並不重要。 比如,   -等價的lambda項,它們都表示相同的函式(自對映函式);但如  項則不是 -等價的,因為它們並非以lambda抽象方式綁定的。 在許多演示中,通常會確定 -等價的lambda項。

為了能夠定義 -歸約,需要以下定義:

自由變數

編輯

所謂的自由變數是那些在lambda抽象不受到綁定的變數。表達式中的一組自由變數定義歸納如下:

  •  的自由變數就只是 
  •  的自由變數集合,是在 中移除了 的自由變數集合。
  •  的自由變數是 的一組自由變數,與 的一組自由變數,這兩項變數的並集。

例如,代表對映自身的 ,其中的lambda項沒有自由變數,但是在函式 中的lambda項,有一個自由變數 

避免捕獲的替換記法

編輯

假設   是lambda項,而  是變數。如果寫成 是一種避免被捕獲的記法方式,表示在 這個lambda項中,以 來替換 變數的值。這定義為:

  •  
  •  ,如果 
  •  
  •  
  • 如果 而且 不在lambda項 的自由變數中,則 。對於lambda項 ,變數 被稱為是「新鮮」的。

例如,  

新鮮度條件(要求 不在lambda項 中的自由變數中)對於確保替換不會改變函式的意義很重要。例如,忽視新鮮度條件的替代: 。此替換會將原本意義為常數函式的 ,轉換成意義為對映自身函式的 

一般來說,在無法滿足新鮮度條件的情況,可利用 -重新命名使用一個合適的新變數來補救,切換回正確的替換概念;比如在 中,使用一個新變數 重新命名這個lambda抽象,獲取 ,則替換就能保留原本函式的義涵。

β-歸約

編輯

β-歸約規定了形式如 的應用,可以化簡成 項。符號記法 用於表示  經過β-歸約轉換為 。例如,對於每個 ,可轉換為 。這表明 實際上的應用是對映自身函式。同樣地, ,表明了 是一個常數函式。

lambda演算可視為函數式程式語言的理想化版本,如HaskellML語言。在這種觀點下,β-歸約對應於一組計算步驟。 這個步驟重複應用β-轉換,一直到沒有東西能再被化簡。在無型別lambda演算中,如本文所述,這個歸約過程可能無法終止, 比如 ,是個特殊的lambda項。這裡   也就是說,該lambda項在一次β-歸約中化簡到本身,因此歸約過程將永遠不會終止。

無型別lambda演算的另一方面是它並不區分不同種類的資料。例如,需要編寫只針對數字操作的功能。然而,在無型別的lambda演算中,沒有辦法避免函式被應用於真值、字串或其它非數字物件。

形式化定義

編輯

形式化地,我們從一個識別碼(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-歸約規則」。

歸約

編輯

歸約的操作包括:

操作 名稱 描述
(λx.M[x]) → (λy.M[y]) α-轉換 重新命名表達式中的綁定(形式)變數。用於避免名稱衝突。
((λx.M) E) → (M[x:=E]) β-歸約 在抽象化的函式定義體中,以參數表達式代替綁定變數。

α-變換

編輯

Alpha-變換規則表達的是,被繫結變數的名稱是不重要的。比如說λx.x和λy.y是同一個函式。儘管如此,這條規則並非像它看起來這麼簡單,關於被繫結的變數能否由另一個替換有一系列的限制。

Alpha-變換規則陳述的是,若V與W均為變數,E是一個lambda表達式,同時E[V:=W]是指把表達式E中的所有的V的自由出現都替換為W,那麼在W不是 E中的一個自由出現,且如果W替換了V,W不會被E中的λ繫結的情況下,有

λV.E == λW.E[V:=W]

這條規則告訴我們,例如λx.(λx.x) x這樣的表達式和λy.(λx.x) y是一樣的。

β-歸約

編輯

Beta-歸約規則表達的是函式作用的概念。它陳述了若所有的E'的自由出現在E [V:=E']中仍然是自由的情況下,有

((λV.E) E') == E [V:=E']

成立。

==關係被定義為滿足上述兩條規則的最小等價關係(即在這個等價關係中減去任何一個對映,它將不再是一個等價關係)。

對上述等價關係的一個更具操作性的定義可以這樣獲得:只允許從左至右來應用規則。不允許任何beta歸約的lambda表達式被稱為Beta範式。並非所有的lambda表達式都存在與之等價的範式,若存在,則對於相同的形式參數命名而言是唯一的。此外,有一個演算法使用者計算範式,不斷地把最左邊的形式參數替換為實際參數,直到無法再作任何可能的規約為止。這個演算法若且唯若lambda表達式存在一個範式時才會停止。Church-Rosser定理說明了,若且唯若兩個表達式等價時,它們會在形式參數換名後得到同一個範式。

η-變換

編輯

前兩條規則之後,還可以加入第三條規則,eta-變換,來形成一個新的等價關係。Eta-變換表達的是外延性的概念,在這裡外延性指的是,對於任一給定的參數,若且唯若兩個函式得到的結果都一致,則它們將被視同為一個函式。Eta-變換可以令    相互轉換,只要   不是   中的自由變數。下面說明了為何這條規則和外延性是等價的:

   外延地等價,即,  對所有的   表達式  成立,則當取   為在   中不是自由出現的變數  時,我們有 ,因此  ,由eta-變換f == g。所以只要eta-變換是有效的,會得到外延性也是有效的。

相反地,若外延性是有效的,則由beta-歸約,對所有的y有(λx .f x) y == f y,可得λx .f x == f,即eta-變換也是有效的。

資料類型的編碼

編輯

基本的lambda演算法可用於建構布林值,算術,資料結構和遞迴的模型,如以下各小節所述。

lambda演算中的算術

編輯

在lambda演算中有許多方式都可以定義自然數,但最常見的還是邱奇數,下面是它們的定義:

0 = λf.λx.x
1 = λf.λx.f x
2 = λf.λx.f (f x)
3 = λf.λx.f (f (f x))

以此類推。直觀地說,lambda演算中的數字n就是一個把函式f作為參數並以f的n次冪為返回值的函式。換句話說,邱奇整數是一個高階函式 -- 以單一參數函式f為參數,返回另一個單一參數的函式。

(注意在邱奇原來的lambda演算中,lambda表達式的形式參數在函式體中至少出現一次,這使得我們無法像上面那樣定義0)在邱奇整數定義的基礎上,我們可以定義一個後繼函式,它以n為參數,返回n + 1:

SUCC = λn.λf.λx.f(n f x)

加法是這樣定義的:

PLUS = λm.λn.λf.λx.m f (n f x)

PLUS可以被看作以兩個自然數為參數的函式,它返回的也是一個自然數。你可以試試驗證

PLUS 2 3 

與5是否等價。乘法可以這樣定義:

MULT = λm.λn.m (PLUS n) 0,

即m乘以n等於在零的基礎上m次加n。另一種方式是

MULT = λm.λn.λf.m (n f)

正整數n的前驅元(predecessesor)PRED n = n - 1要複雜一些:

PRED = λn.λf.λx.n (λg.λh.h (g f)) (λu.x) (λu.u)

或者

PRED = λn.n(λg.λk.(g 1) (λu.PLUS(g k) 1) k) (λl.0) 0

注意(g 1)(λu.PLUS(g k) 1) k表示的是,當g(1)是零時,表達式的值是k,否則是g(k)+ 1

邏輯與謂詞

編輯

習慣上,下述兩個定義(稱為邱奇布林值)被用作TRUEFALSE這樣的布林值:

TRUE := λx.λy.x
FALSE := λx.λy.y
(注意FALSE等價於前面定義邱奇數零)

接著,通過這兩個λ-項,我們可以定義一些邏輯運算

AND := λp q.p q FALSE
OR := λp q.p TRUE q
NOT := λp.p FALSE TRUE
IFTHENELSE := λp x y.p x y

我們現在可以計算一些邏輯函式,比如:

AND TRUE FALSE
≡(λp q.p q FALSE) TRUE FALSE →β TRUE FALSE FALSE
≡(λx y.x) FALSE FALSE →β FALSE

我們見到AND TRUE FALSE等價於FALSE

「謂詞」是指返回布林值的函式。最基本的一個謂詞是ISZERO,若且唯若其參數為零時返回真,否則返回假:

ISZERO := λn.n (λx.FALSE) TRUE

運用謂詞與上述TRUEFALSE的定義,使得"if-then-else"這類語句很容易用lambda演算寫出。

有序對

編輯

有序對(2-元組)資料類型可以用TRUEFALSEIF來定義。

CONS := λx y.λp.IF p x y
CAR := λx.x TRUE
CDR := λx.x FALSE

鏈結串列資料類型可以定義為,要麼是為空串列保留的值(e.g.FALSE),要麼是CONS一個元素和一個更小的列表。

附加的編程技術

編輯

lambda演算出現在相當大量的編程習慣用法中,其中許多程式語言最初以lambda演算作為語義基礎,在此背景下開發的;有效地利用lambda演算作為基底。因為幾個程式語言部份含括了lambda演算(或者非常相似的東西),所以這些技術也可以在實際的編程中見到,但有可能被認為是模糊或外來的。

命名常數

編輯

在lambda演算中,函式庫將採用預先定義好的函式集合,其中lambda項僅僅是特定的常數。純粹的lambda演算法並不具有命名常數的概念,因為所有的原子λ項都是變數;但是在程式主體中,我們可將一個變數當成常數的名稱,利用lambda抽象把這個變數綁定,並將該lambda抽象應用於預期的定義,來類比命名常數的作法。因此在N(「主程式」的另一個lambda項)中,要以f來表示M(一些明確的lambda項),則寫成如下:

f.N) M

作者經常引入類似如let語法糖,允許以更直觀的次序撰寫上述內容:

let f = M in N

通過等號鏈結這個命名常數,即可將lambda演算「編程」的一個lambda項,寫為零或多個函式的定義,而使用構成程式主體的那些函式。這個let顯著的限制,是在M中並沒有定義f名稱,因為M不在綁定f的lambda抽象範疇之內;這意味著遞迴函式定義不能以let來使用M。更進步的letrec語法糖允許以直覺的方式編寫遞迴函式定義,而不需用到不動點組合子。

遞迴與不動點

編輯

遞迴是使用函式自身的函式定義;在表面上,lambda演算不允許這樣。但是這種印象是誤解。考慮個例子,階乘函式f(n)遞迴的定義為

f(n):= if n = 0 then 1 else n·f(n-1)

在lambda演算中,你不能定義包含自身的函式。要避免這樣,你可以開始於定義一個函式,這裡叫g,它接受一個函式f作為參數並返回接受n作為參數的另一個函式:

g := λf n.(if n = 0 then 1 else n·f(n-1))

函式g返回要麼常數1,要麼函式fn-1的n次應用。使用ISZERO謂詞,和上面描述的布林和代數定義,函式g可以用lambda演算來定義。

但是,g自身仍然不是遞迴的;為了使用g來建立遞迴函式,作為參數傳遞給gf函式必須有特殊的性質。也就是說,作為參數傳遞的f函式必須展開為呼叫帶有一個參數的函式g -- 並且這個參數必須再次f函式!

換句話說,f必須展開為g(f)。這個到g的呼叫將接著展開為上面的階乘函式並計算下至另一層遞迴。在這個展開中函式f將再次出現,並將被再次展開為g(f)並繼續遞迴。這種函式,這裡的f = g(f),叫做g的不動點,並且它可以在lambda演算中使用叫做悖論算子不動點算子來實現,它被表示為Y -- Y組合子

Y = λg.(λx.g(x x))(λx.g(x x))

在lambda演算中,Y gg的不動點,因為它展開為g(Y g)。現在,要完成我們對階乘函式的遞迴呼叫,我們可以簡單的呼叫 g(Y g)n,這裡的n是我們要計算它的階乘的數。

比如假定n = 5,它展開為:

(λn.(if n = 0 then 1 else n·((Y g)(n-1)))) 5
if 5 = 0 then 1 else 5·(g(Y g,5-1))
5·(g(Y g)4)
5·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 4)
5·(if 4 = 0 then 1 else 4·(g(Y g,4-1)))
5·(4·(g(Y g)3))
5·(4·(λn.(if n = 0 then 1 else n·((Y g)(n-1))) 3))
5·(4·(if 3 = 0 then 1 else 3·(g(Y g,3-1))))
5·(4·(3·(g(Y g)2)))
...

等等,遞迴的求值演算法的結構。所有遞迴定義的函式都可以看作某個其他適當的函式的不動點,因此,使用Y所有遞迴定義的函式都可以表達為lambda表達式。特別是,我們現在可以明晰的遞迴定義自然數的減法、乘法和比較謂詞。

標準化的組合子名稱

編輯

某一些lambda項有普遍接受的名稱:

I := λx.x
K := λxy.x
S := λxyz.x z (y z)
B := λxyz.x (y z)
C := λxyz.x z y
W := λxy.x y y
U := λxy.y (x x y)
ω := λx.x x
Ω := ω ω
Y := λg.(λx.g (x x)) (λx.g (x x))

其中有幾個在「消除lambda抽象」中有直接的應用,將lambda項變為組合演算的術語。

消除lambda抽象

編輯

如果N是一個沒有λ-抽象的lambda項,但可能包含了命名常數(組合子),則存在一個lambda項T(x,N),這相同於一個缺少λ-抽象(除了作為命名常數的一部份,如果這些被認為是非原子的)的λx.N;也可以被視為匿名變數,就如同T(x,N)從N之中刪除所有出現的x,同時仍然允許在N包含x的位置替換參數值。

轉換函式T可由下式定義:

T(x, x) := I
T(x, N) := K N if x is not free in N.
T(x, M N) := S T(x, M) T(x, N)

在這兩種情況下,形式T(x,N)P可藉由使初始的組合子IKS獲取參數P而化簡, 就像x.N) P經過β-歸約一樣。I返回那個參數。K則將參數拋棄,就像x.N),如果xN中不是以自由變數出現。S將參數傳遞給應用程式的兩個子句,然後將第一個結果應用到第二個的結果之上。

組合子BC類似於S,但把參數傳遞給應用的一個子項(B傳給「參數」子項,而C傳給「函式」子項),如果子項中沒有出現x,則儲存後續的K。與BC相比,S組合子實際上混合了兩個功能: 重新排列參數,並複製一個參數,以便它可以在兩個地方使用。W組合子只做後者,產生了SKI組合子演算的B,C,K,W系統。

可計算函式和lambda演算

編輯

自然數的函式F: NN可計算函式若且唯若存在著一個lambda表達式f,使得對於N中的每對x, y都有F(x) = y若且唯若f x == y,這裡的xy分別是對應於x和y的邱奇數。這是定義可計算性的多種方式之一;關於其他方式和它們的等價者的討論請參見邱奇-圖靈論題

lambda演算與程式語言

編輯

匿名函式

編輯

比如計算平方的函式 square 在 Lisp 中可以表示為如下的 lambda 表達式

(lambda (x) (* x x))

符號 lambda 建立一個匿名函式,給定參數列 (x) ,以及一個作為函式體的表達式 (* x x)。 匿名函式有時稱為 lambda 表達式。

很多命令式語言都有函式指標或者類似的機制。但是函式指標並不是類型中的一等公民,函式是一等公民若且唯若函式可以在執行時建立。 下面一些語言支援函式的執行時建立: SmalltalkJavaScriptKotlinScalaPython3C# ("delegates")、 C++11等。

化簡策略

編輯

關於複雜度的註釋

編輯

並行與並發

編輯

參見

編輯

參考文獻

編輯
  1. ^ Turing, A. M. Computability and λ-Definability. The Journal of Symbolic Logic. December 1937, 2 (4): 153–163. JSTOR 2268280. doi:10.2307/2268280. 
  2. ^ Coquand, Thierry, "Type Theory"頁面存檔備份,存於網際網路檔案館), The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.).
  3. ^ Moortgat, Michael. Categorial Investigations: Logical and Linguistic Aspects of the Lambek Calculus. Foris Publications. 1988. ISBN 9789067653879. 
  4. ^ Bunt, Harry; Muskens, Reinhard (編), Computing Meaning, Springer, 2008, ISBN 9781402059575 
  5. ^ Mitchell, John C., Concepts in Programming Languages, Cambridge University Press: 57, 2003, ISBN 9780521780988 
  6. ^ Pierce, Benjamin C. Basic Category Theory for Computer Scientists. : 53. 
  7. ^ Church, A. A set of postulates for the foundation of logic. Annals of Mathematics. Series 2. 1932, 33 (2): 346–366. JSTOR 1968337. doi:10.2307/1968337. 
  8. ^ For a full history, see Cardone and Hindley's "History of Lambda-calculus and Combinatory Logic" (2006).
  9. ^ Kleene, S. C.; Rosser, J. B. The Inconsistency of Certain Formal Logics. The Annals of Mathematics. July 1935, 36 (3): 630. doi:10.2307/1968646. 
  10. ^ Church, Alonzo. Review of Haskell B. Curry, The Inconsistency of Certain Formal Logics. The Journal of Symbolic Logic. December 1942, 7 (4): 170–171. JSTOR 2268117. doi:10.2307/2268117. 
  11. ^ Church, A. An unsolvable problem of elementary number theory. American Journal of Mathematics. 1936, 58 (2): 345–363. JSTOR 2371045. doi:10.2307/2371045. 
  12. ^ Church, A. A Formulation of the Simple Theory of Types. Journal of Symbolic Logic. 1940, 5 (2): 56–68. JSTOR 2266170. doi:10.2307/2266170. 
  13. ^ Partee, B. B. H.; ter Meulen, A.; Wall, R. E. Mathematical Methods in Linguistics. Springer. 1990 [29 Dec 2016]. 
  14. ^ Alama, Jesse "The Lambda Calculus"頁面存檔備份,存於網際網路檔案館), The Stanford Encyclopedia of Philosophy (Summer 2013 Edition), Edward N. Zalta (ed.).
  15. ^ Cardon, Felice; Hindley, J. Roger. History of Lambda-calculus and Combinatory Logic. 2006. 

外部連結

編輯