檢視 Λ演算的原始碼

'''λ 演算'''（英語：lambda calculus，λ-calculus）是一套對數學邏輯內底發展，以變數縛定佮替換的規則，來研究函式按怎抽象化定義、函式按怎被應用猶閣有遞迴的形式系統。伊由數學家阿隆佐 ・ 邱奇佇咧二十世紀三空年代頭擺發表。lambda 演算做一種廣泛用途的計算模型，會當足深的定義啥物是一个會當算函式，煞任何可計算函式攏會當這種形式表達佮求值，伊會當比單一磁帶圖靈機的計算過程；就算講按呢，lambda 演算強調的是變換規則的運用，毋是實現𪜶的具體機器。

lambda 演算會當比擬是上根本的程式語言，伊包括一條變換規則（變數替換）和一條將函式抽象化定義的方式。因此普遍公認是一種閣較接近軟體毋是硬體的方式。對函數式程式語言造成誠大的影響，比如講 Lisp、ML 語言佮 Haskell 語言。佇一九三六年邱奇利用 λ 演算予出矣對判定性問題（Entscheidungsproblem）的否定：有關於兩个 lambda 運算式敢有等價數的命題，無法度由一个「算講通用的演算法」判斷，這是不可判定效會當證明的頭一个問題，甚至猶佇咧停機這个問題進先。

lambda 演算包括了建構 lambda 項，佮著 lambda 項執行歸約操作。佇上簡單的 lambda 演算中，干焦使用以下的規則來建構 lambda 項：

產生矣諸如：( λx . λy . ( λz . ( λx . zx ) ( λy . zy ) ) ( x y ) ) 的表達式。若表達式是明確抑無歧義的，是阮的括號會當省略仔。對某一寡應用，其中可能包括著邏輯佮數學的常數佮相關的操作。

本文討論的是邱奇的「無類型 lambda 演算」，此後，已經研究出來矣有類型 lambda 演算。

==解說佮應用==

λ 演這是算圖靈完備的，也就是講，這是一个會當用於類比任何圖靈機的通用模型。λ 嘛予人用佇咧'''λ 表達式'''和'''λ 項'''中，用來表示將一个變數縖結佇一个函式頂懸。

λ 演算會當是'''有類型'''抑是講'''無類型'''的，佇咧有類型 λ 演算中（文所寫的是無類型的）， 函式只會當佇參數類型佮輸入類型符合的時陣被應用。有類型 λ 演算比無類型 λ 演算愛弱—— 後者是這个條目的主要部份—— 因為有類型的 λ 運算會當表達的比無類型 λ 演算少；佮這个同時，前者會使予閣較濟定理會當證明。比如講，佇簡單類型 λ 演算中，運算總是會當停止，毋過無類型 λ 演算中這是無一定的（因為停機問題）。 目前有真濟種有類型 λ 演算的一个原因是𪜶予人向望會當做甲閣較濟（做到某一寡較早的有類型 λ 演算做袂到的）的同時又閣會當用證明閣較濟定理。

λ 演算是佇數學、哲學、語言學佮電腦科學中攏有真濟應用。伊佇程式語言理論中占有重要地位，函式語言程式設計實現矣 λ 演算支援。λ 演算佇範圍論中嘛是一个研究熱點。

==歷史==

做對數學基礎研究的一部份，數學家阿隆佐 ・ 邱奇佇二十世紀三空年代提出 λ 演算。但是頭先的 λ 演算系統予證明是邏輯上無自辦的—— 佇一九三五年史蒂芬 ・ 科爾 ・ 克萊尼佮 J . B . Rosser 舉出了 Kleene-Rosser 鋪論。

隨後，佇一九三六年邱奇共彼个版本的關於計算的部份抽出獨立發表—這馬這予人叫做無類型 λ 演算。佇一九四Ｏ年，伊創立了一个計算能力閣較弱毋過邏輯上自洽的系統，這予人號做是簡單類型 λ 演算。

一直到一九六Ｏ年，λ 演算佮程式語言的關係予確立矣；伊進前遮只是一个範式。因為理察 ・ 蒙塔古佮其他的語言學家將 λ 演算應用伊自然語言語法的研究，λ 演算已經開始佇語言學佮電腦科學學界有一席的所在。

若是為啥物邱奇選擇 λ 做符號，連伊本人的解說嘛互相矛盾：頭仔是佇一九六四年的一封批中，伊明確來解說講這是來源於著《數學原理》一書中的類抽象符號（脫字元）， 為著方便閱讀，伊頭先共換做邏輯佮符號（$ \ land $）作為區分，閣改做形狀類似的 λ。伊佇一九八四年又閣重申矣這點，但是閣後來伊閣表示選擇 λ 純粹是尪仔然。

==非形式化就一直感覺講==

佇咧 λ 演算中，逐个表達式的人攏代表一个函式的，這个函式有一个參數，並且會倒轉來一个值。無論是參數佮返回值，嘛攏是一个單參的函式。會當按呢講，λ 演算中干焦一種「類型」，彼就是這種一箍函式。函式是通過 λ 表達式無頭的定義的，這个表達式說明了此函式將對參數進行啥物操作。

比如講，「 加二」函式 f ( x )=x + 二會使用 lambda 演算表示為 λx . x + 二（抑是講 λy . y + 二，參數的號名無關係愛）， 而且 f ( 三 ) 的值得寫作 ( λx . x + 二 ) 三。函式的應用（application）是倒結合的：f x y=( f x ) y。

考慮遮爾一个函式：伊共一个函式做參數，這个函式將被作用佇三上：λf . f 三。若共這（用函式做參數的）函式來作用咱早前的「加二」函式上：( λf . f 三 ) ( λx . x + 二 )，是明顯地，欲講三个表達式：


: ( λf . f 三 ) ( λx . x + 二 ) 佮 ( λx . x + 二 ) 三佮三 + 二是等價的。有兩个參數的函式會當通過 lambda 演算是按呢表達：一个單一參數的函式，伊的回值閣是一个單一參數的函式（參見柯里化）。 比如講，函式 f ( x , y )=x-y 會當寫作 λx . λy . x-y。欲講三个表達式：


: ( λx . λy . x-y ) 七二和 ( λy . 七-y ) 二佮七-二嘛是等價的。毋過這款 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 ) ) 予人叫做是 Ω 二，以此類推。若形式化函式作用的概念無允准 lambda 表達式，就得著組合子邏輯。

===動機===

佇數學佮計算機科學內底，「 可計算的」函式是基礎的觀念。對所講的可計算性，λ-演算提供一个簡單清楚的語義，使計算的性質會當予形式化研究。λ-演算結合兩種簡化的方式，會當予這个語義變做簡單。第一種簡化是無予函式一个確定名稱，而且「匿名」地對待𪜶。比如講，兩數的平方佮函式


: $ \ operatorname { square \ _ sum } ( x , y )=x ^ { 二 } + y ^ { 二 } $

會使用匿名的形式重新寫為：


: $ ( x , y ) \ mapsto x ^ { 二 } + y ^ { 二 } $（理解做一包括 x 和 y 的數組被對映到 $ x ^ { 二 } + y ^ { 二 } $）

仝款所在，


: $ \ operatorname { id } ( x )=x $

會使用匿名的形式重新寫為：


: $ x \ mapsto x $（即輸入是直接對應到伊本身。）

第二个簡省是 λ 演算干焦使用單一个參數輸入的函式。若普通函式需要兩个參數，比如講 $ \ operatorname { square \ _ sum } $ 函式，會當轉做接受單一參數，傳予另外一个函式內底，若中介函式嘛干焦接受一个參數，到尾仔輸出結果。比如講，


: $ ( x , y ) \ mapsto x ^ { 二 } + y ^ { 二 } $

會當重新寫做：


: $ x \ mapsto ( y \ mapsto x ^ { 二 } + y ^ { 二 } ) $

這是叫柯里化的方法，將多參數的函式轉換做多個中介函式的複合鏈，逐中介函式攏干焦接受一个參數。
將 $ \ operatorname { square \ _ sum } $ 函式應用參數 ( 五 , 二 )，直接產生結果


: $ ( ( x , y ) \ mapsto x ^ { 二 } + y ^ { 二 } ) ( 五 , 二 ) $


: $=五 ^ { 二 } + 二 ^ { 二 } $


: $=二十九 $ ,

毋過對柯里化轉換版的評估，需要閣加一步：


: $ { \ Bigl ( } { \ bigl ( } x \ mapsto ( y \ mapsto x ^ { 二 } + y ^ { 二 } ) { \ bigr ) } ( 五 ) { \ Bigr ) } ( 二 ) $


: $=( y \ mapsto 五 ^ { 二 } + y ^ { 二 } ) ( 二 ) $ / / 在內層表達中 $ x $ 的定義做 $ 五 $，這就像 β-歸約仝款。


: $=五 ^ { 二 } + 二 ^ { 二 } $ / / $ y $ 的定義做 $ 二 $，閣再親像 β-歸約。


: $=二十九 $

著愛出仝款結果。

===lambda 演算===

lambda 演算講是由特定形式語法所組成的一種語言，轉換規則會當操作其中的 lambda 項。遮的轉換規則予人看做是一个等式理論或者是一个操作定義。如果上節咧講，lambda 演算中的所有函式攏是匿名的，𪜶無名，𪜶干焦接受一个輸入變數，柯里化用佇實現有偌个輸入變數的函式。

====lambda 項====

lambda 演算的語法共一寡表達式定義做有效的 lambda 演算式，某一寡表達式無效，就親像 C 程式語言中有一寡字串有效，有的無的。有效的 lambda 演算式號做「lambda 項」。

以下三个規則予出著語法內底有效的 lambda 項，如何建構的歸納定義：

* 變數 $ x $ 本身就是一个有效的 lambda 項
* 若是 $ t $ 是一个 lambda 項，而且 $ x $ 是一个變數，著 $ ( \ lambda x . t ) $ 是一个 lambda 項（這號做'''lambda 抽象'''）；
* 若是 $ t $ 和 $ s $ 是 lambda 項，遐爾 $ ( ts ) $ 是一个 lambda 項（這號做'''應用'''）。

其他的攏毋是 lambda 項。所以，lambda 項若準閣會當重複應用這三个規則取得的時間，才是有效的。一寡括號根據某一寡規則會當省略。比如講，上外口的括號通常袂寫入。

「 lambda 抽象」是講一个匿名函式的定義，伊將單一輸入的 $ \ lambda x . t $ 替換做 $ t $ 的表達式，所以產生一个崁名函式，伊採用 $ x $ 的值閣倒轉來 $ t $。比如講，$ \ lambda x . x ^ { 二 } + 二 $ 是表示使用函式的 $ f ( x )=x ^ { 二 } + 二 $ 做為 $ t $ 項的一个 lambda 抽象。lambda 抽象只是先「設定」了函式的定義，猶未使用伊。這个抽象佇咧 $ t $ 項中縛定矣變數 $ x $。一个'''應用'''$ ts $ 表示將函式 $ t $ 應用咧輸入 $ s $，亦即對輸入 $ s $ 使用函式 $ t $ 產生 $ t ( s ) $。

lambda 演算中並無變數聲明的概念。如 $ \ lambda x . x + y $（即 $ f ( x )=x + y $）的定義內底，lambda 演算將 $ y $ 當做猶未定義的變數。lambda 抽象 $ \ lambda x . x + y $ 佇語法內底是有效的，並表示會輸入添加到未知 $ y $ 的函式。

會當用圓括弧對來消除歧義。比如講，$ \ lambda x . ( ( \ lambda x . x ) x ) $ 和 $ ( \ lambda x . ( \ lambda x . x ) ) x $ 表示無仝款的項（就算講𪜶拄仔好化簡單甲仝值）。 遮第一个例定義一个包含子函式的抽象，並將子函式應用於 x（先應用做咧傳回）的結果；啊若第二个例定義一个傳回任何輸入的函式，然後佇應用過程中傳回對輸入做 x 的應用（回回函式然後應用）。

====操作函式的函式====

佇咧 lambda 演算中，函式予人認為是'''頭等等的東西'''，因此函式會當做輸入，抑是作為其他函式的輸出返回。

比如講，$ \ lambda x . x $ 表示對影到本身的函式，$ x \ mapsto x $ 和 $ ( \ lambda x . x ) y $ 表示將這个函式應用於 $ y $。此外，$ ( \ lambda x . y ) $ 是表示無論輸入按怎，始終返回 $ y $ 值的'''常數函式'''$ x \ mapsto y $。lambda 演算中的函式應用是倒結合的，所以 $ stx $ 表示 $ ( st ) x $。

有幾个啊「等價」和「化簡」的概唸，容允將各個 lambda 項「縮減」為「相仝」的 lambda 項。

====$ \ alpha $-等價====

對於 lambda 項，等價的基本形式定義，是 $ \ alpha $-等價。伊掠直覺概念，佇咧 lambda 抽象中一个縛定變數的特別選擇（通常）無重要。
比如講，$ \ lambda x . x $ 和 $ \ lambda y . y $ 是 $ \ alpha $-等價的 lambda 項，𪜶攏表示相仝的函式（自對影函式）； 但是如 $ x $ 和 $ y $ 項則毋是 $ \ alpha $-等價的，因為𪜶嘛無以 lambda 抽象方式縛定的。
佇真濟演示內底，通常會確定講 $ \ alpha $-等價的 lambda 項。

為著會當定義 $ \ beta $-歸約，需要以下定義：

====自由變數====

咱所講的'''自由變數'''是遐的佇咧 lambda 抽象無受著縛定的變數。表達式內的一組自由變數定義歸納如下：

* $ x $ 的自由變數就只是 $ x $
* $ \ lambda x . t $ 的自由變數集合，是佇咧 $ t $ 著徙掉矣 $ x $ 的自由變數集合。
* $ ts $ 的自由變數是 $ t $ 的一組自由變數，佮 $ s $ 的一組自由變數，這兩項變數的並集。

比如講，代表對映自身的 $ \ lambda x . x $，內底的 lambda 項無自由變數，但是咧函式的 $ \ lambda x . yx $ 中的 lambda 項，有一个自由變數 $ y $。

====避免掠著的替換記法====

準講 $ t $，$ s $ 和 $ r $ 是 lambda 項，而且 $ x $ 和 $ y $ 是變數。若寫有無 $ t [x :=r] $ 是一種 _ 避免講予人掠著 _ 的記法方式，表示咧 $ t $ 這乎 lambda 項中，以 $ r $ 來替換 $ x $ 變數的值。這定義為：

* $ x [x :=r]=r $；
* $ y [x :=r]=y $，若是 $ x \ neq y $；
* $ ( ts ) [x :=r]=( t [x :=r] ) ( s [x :=r] ) $；
* $ ( \ lambda x . t ) [x :=r]=\ lambda x . t $；
* 若是 $ x \ neq y $ 而且 $ y $ 無佇咧 lambda 項 $ r $ 的自由變數中，著 $ ( \ lambda y . t ) [x :=r]=\ lambda y . ( t [x :=r] ) $。對於 lambda 項 $ r $，變數 $ y $ 予人叫做是「鮮」的。

比如講，$ ( \ lambda x . x ) [y :=y]=\ lambda x . ( x [y :=y] )=\ lambda x . x $ 和 $ ( ( \ lambda x . y ) x ) [x :=y]=( ( \ lambda x . y ) [x :=y] ) ( x [x :=y] )=( \ lambda x . y ) y $。

鮮度條件（要求 $ y $ 無佇咧 lambda 項 $ r $ 中的自由變數中）對確保替換袂改變函式的意義真重要。比如講，忽視鮮度條件的替代：$ ( \ lambda x . y ) [y :=x]=\ lambda x . ( y [y :=x] )=\ lambda x . x $。這替換會將原本意義做常數函式的 $ \ lambda x . y $，轉換做意義為對映自身函式的 $ \ lambda x . x $。

一般來講，佇無法度滿足鮮度條件的狀況，通利用 $ \ alpha $-重號名使用一个合適的新變數來補救，切換回正確的替換概念；比如講佇 $ ( \ lambda x . y ) [y :=x] $ 中，用一个新變數 $ z $ 重號名這 lambda 抽象，得著 $ ( \ lambda z . y ) [y :=x]=\ lambda z . ( y [y :=x] )=\ lambda z . x $，著會當替換就會當保留原本函式的義涵。

====$ \ beta $-歸約====

β-歸約規定矣形式如 $ ( \ lambda x . t ) s $ 的應用，會使化簡成 $ t [x :=s] $ 項。符號記法 $ ( \ lambda x . t ) s \ to t [x :=s] $ 用於表示 $ ( \ lambda x . t ) s $ 經過 β-歸約轉換做 $ t [x :=s] $。比如講，對著每一个 $ s $，會當轉換做 $ ( \ lambda x . x ) s \ to x [x :=s]=s $。這个表明 $ \ lambda x . x $ 實際上的應用是對映自身函式。仝款所在，$ ( \ lambda x . y ) s \ to y [x :=s]=y $，顯明矣 $ \ lambda x . y $ 是一个常數函式。

lambda 演算會當看做函數式程式語言的理想化版本，如 Haskell 抑是 ML 語言。佇這種觀念的，β-歸約對應該一組計算步驟。
這个步數重複應用 β-轉換，一直到無物件會當閣予人化去。佇咧無型別 lambda 演算中，如本文所寫的，這个歸約的過程可能無法度終止，
比如講 $ \ Omega=( \ lambda x . xx ) ( \ lambda x . xx ) $，是一个特殊的 lambda 項。遮 $ ( \ lambda x . xx ) ( \ lambda x . xx ) \ to ( xx ) [x :=\ lambda x . xx]=( x [x :=\ lambda x . xx] ) ( x [x :=\ lambda x . xx] )=( \ lambda x . xx ) ( \ lambda x . xx ) $ 也就是講，該 lambda 項佇一擺 β-歸約中化簡到本身，因此歸約過程會永遠袂終止。

無型別 lambda 演算的另外一方面是伊並無分無仝種類的資料。比如講，需要編寫干焦針對數字操作的功能。毋過，佇咧無型別項 lambda 演算中，無法度避免函式被應用於真值、字攕抑是其他非數字東西。

==形式化定義==

形式化地，咱對一个識別碼（identifier）的可數無窮集合開始，比如講 { a , b , c , . . . , x , y , z , x 一 , x 二 , . . . }，則所有的 lambda 表達式會當通過後述以 BNF 範式表達的上下文無關係文法描述：

一 . < 表達式 >   : :=< 若看別碼 >
二 . < 表達式 >   : :=( λ < 若看別碼 > . < 表達式 > )
三 . < 表達式 >   : :=( < 表達式 > < 表達式 > )

頭兩條規則用來生做函式，啊若第三條描述了函式是按怎作用佇參數頂懸的。通常，lambda 抽象（規則二）和函式的作用（規則三）中的括弧佇袂產生歧義的情形下會當省略仔。若下假定保證袂產生歧義：（一）函式的作用是倒結合的，和（二）lambda 運算子去予結結到伊後壁的規个表達式。比如講，表達式 ( λx . x x ) ( λy . y ) 會當簡寫做 λ ( x . x x ) λy . y。

類似 λx . ( x y ) 按怎 lambda 表達式並無定義一个函式，因為變數 y 的出現就是自由的，即伊並無予人結合甲表達式內底的任何一个 λ 上。一个 lambda 表達式的自由變數的集合是通過下述規則（是因為 lambda 表達式的結構還納地）定義的：

一 . 咧表達式 V 中，V 是變數，著這个表達式里自由變數的集合干焦 V。
二 . 咧表達式 λV . E 中（V 是變數，E 是另外一个表達式）， 自由變數的集合是 E 中自由變數的集合減去變數 V。因而，E 中那些 V 予人叫做是縖結佇咧 λ 上。
三 . 咧表達式 ( E E') 中，自由變數的集合是 E 和 E'自由變數集合的併集。

例，對表達式 λ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。

佇咧 lambda 表達式的集合上定義一个等價關係 ( 佇遮用==標註 )，「 兩个表達式其實表示的是仝一个函式」按呢的直覺性判斷就按呢表示，這種等價關係是通過所謂的「alpha-變換規則」和「beta-歸約規則」。

==歸約==

歸約的操作包括：

===α-變換===

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-變換會使令 $ \ lambda x . fx $ 和 $ f $ 相換，只要 $ x $ 毋是呢 $ f $ 中的自由變數。下跤說明矣是按怎這條規則佮外延性是等價的：

若是 $ f $ 佮 $ g $ 外延地等價數，即，$ fa==ga $ 嘿所有的 $ \ lambda $ 表達式 $ a $ 成立，著當取 $ a $ 為在 $ f $ 中毋是自由出現的變數 $ x $ 時，阮有 $ f ( x )==g ( x ) $，所以 $ \ lambda x . fx==\ lambda x . gx $，由 eta-變換 f==g。所以只要 eta-變換是有效的，會得著外延性嘛是有效的。

反倒轉來，若是外延性是有效的，著愛由 beta-歸約，嘿所有的 y 有 ( λx . f x ) y==f y，可得 λx . f x==f，即 eta-變換嘛是有效的。

==資料類型的編碼==

基本的 lambda 演算法通用建構布林值，算術，資料結構佮遞迴的模型，如果以下各小節咧講。

===lambda 演算中的算術===

佇咧 lambda 演算中有足濟方式攏會使定義自然數，但是上捷看著的抑是邱奇數，下跤是𪜶的定義：

` ` `
零=λf . λx . x
一=λf . λx . f x
二=λf . λx . f ( f x )
三=λf . λx . f ( f ( f x ) )
` ` `

以此類推。直觀咧講，lambda 演算中的數字 n 就是一个共函式 f 做參數並以 f 的 n 次冪為轉去值的函式。嘛會使講，邱奇整數是一个高階函式--以單一參數函式 f 為參數，倒轉來另外一个單一參數的函式。

( 注意踮邱奇原來的 lambda 演算中，lambda 表達式這个形式參數咧函式體內底上無嘛出現一改，這予咱無法度像頂懸彼定義零 ) 佇邱奇整數定義的基礎頂頭，咱會當定義一个後繼函式，伊以 n 為參數，倒轉來 n + 一：

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

加法是按呢定義的：

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

PLUS 會當被看作以兩个自然數為參數的函式，伊倒轉來嘛是一个自然數。你會使試驗證

` ` `
PLUS 二三
` ` `

佮五敢等價數。乘法會當按呢定義：

` ` `
MULT=λm . λn . m ( PLUS n ) 零 ,
` ` `

即 m 乘以 n 等於佇咧零的基礎頂懸 m 次加 n。另外一種方式是

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

當整數 n 的前驅元（predecessesor）PRED n=n-一愛複雜一寡：

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

抑是講

` ` `
PRED=λn . n ( λg . λk . ( g 一 ) ( λu . PLUS ( g k ) 一 ) k ) ( λl . 零 ) 零
` ` `

注意 ` ( g 一 ) ( λu . PLUS ( g k ) 一 ) k ` 表示的是，當 ` g ( 一 ) ` 著無，表達式的值是 ` k `，抑無是 ` g ( k ) + 一 `。

===邏輯佮叫詞===

慣勢上，欲教兩个定義（叫邱奇布林值）被用作 TRUE 和 FALSE 按呢的布林值：


: 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

運用人講詞佮頂懸 TRUE 和 FALSE 的定義，予得 " if-then-else " 這類語句是誠容易用 lambda 演算寫出。

===有序嘿===

有序嘿（二-元組）資料的類型會當用 TRUE、FALSE 和 IF 來定義。


: 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=零 then 一 else n·f ( n 影一 )。

佇咧 lambda 演算中，你袂當定義包含家己的函式。欲避免按呢，你會當開始於定義一个函式，遮叫 g，伊接受一个函式 f 作為參數閣倒轉來接受 n 作為參數的另外一个函式：


: g  :=λf n . ( if n=零 then 一 else n·f ( n 影一 ) )。

函式 g 倒轉來愛加足捷算的，欲按怎函式 f 著 n 擗一的 n 次應用。使用 ISZERO 謂詞，佮頂頭咧講的布林佮代數定義，函式 g 會用得 lambda 演算來定義。

猶毋過，g 家己猶閣毋是遞迴的；為著欲使用 g 來建立遞迴函式，成做參數傳遞予 g 的 f 函式著愛有特殊的性質。也就是講，成做參數傳遞的 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 g 是 g 的不動點，因為伊展開做 g ( Y g )。這馬乎，欲完成阮對階乘函式的交回呼叫，阮會當簡單的呼叫 g ( Y g ) n，遮的 n 是咱愛計算伊的階乘的數。

比如講假定 n=五，伊展開做：


: ( λn . ( if n=零 then 一 else n·( ( Y g ) ( n 影一 ) ) ) ) 五


: if 五=零 then 一 else 五·( g ( Y g，五孵一 ) )


: 五·( g ( Y g ) 四 )


: 五·( λn . ( if n=零 then 一 else n·( ( Y g ) ( n 影一 ) ) ) 四 )


: 五·( if 四=零 then 一 else 四·( g ( Y g，四配一 ) ) )


: 五·( 四·( g ( Y g ) 三 ) )


: 五·( 四·( λn . ( if n=零 then 一 else n·( ( Y g ) ( n 影一 ) ) ) 三 ) )


: 五·( 四·( if 三=零 then 一 else 三·( g ( Y g，三孵一 ) ) ) )


: 五·( 四·( 三·( g ( Y g ) 二 ) ) )


: . . .

等咧，遞迴的求值演算法的結構。所有遞迴定義的函式攏會當看做某一个其他適當的函式的不動點，所以，使用 Y 所有遞迴定義的函式攏會當表達為 lambda 表達式。特別是，咱這馬會使明深的遞迴定義自然數的減法、乘法佮較謂詞。

===標準化的組合子名稱===

某一寡仔 lambda 項有普遍接受的名稱：


:'''I'''  :=λ _ x _ . _ x _


:'''K'''  :=λ _ x _ . λ _ y _ . _ x _


:'''S'''  :=λ _ x _ . λ _ y _ . λ _ z _ . _ x _ _ z _ ( _ y _ _ z _ )


:'''B'''  :=λ _ x _ . λ _ y _ . λ _ z _ . _ x _ ( _ y _ _ z _ )


:'''C'''  :=λ _ x _ . λ _ y _ . λ _ z _ . _ x _ _ z _ _ y _


:'''W'''  :=λ _ x _ . λ _ y _ . _ x _ _ y _ _ y _


:'''U'''  :=λ _ x _ . λ _ y _ . _ 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 _ 會當藉由使初初的組合子'''I'''，'''K'''抑是'''S'''得著參數 _ P _ 啊若化簡，
就親像 ( λ _ x _ . _ N _ ) _ P _ 經過 β-歸約仝款。'''I'''倒轉來彼个參數。'''K'''則將參數放捒，就親像 ( λ _ x _ . _ N _ )，若是 _ x _ 佇咧 _ N _ 中毋是以自由變數出現。'''S'''共參數傳遞予應用程式的兩个字句，然後共第一个結果應用去第二个的結果之上。

組合子'''B'''和'''C'''類似'''S'''，但是共參數傳遞予應用的一个子項（'''B'''傳予「參數」子項，而且'''C'''傳予「函式」子項）， 若是子中無出現 _ x _，則儲存後續的'''K'''。佮'''B'''和'''C'''相比並，'''S'''組合子實際上透濫兩个功能：
重新排列參數，並且複製一个參數，以便伊會當佇兩个所在使用。'''W'''組合子干焦做後者，產生矣 SKI 組合子演算的 B，C，K，W 系統。

==可計算函式佮 lambda 演算==

自然數的函式 F :'''N'''→'''N'''是會當算函式，若是唯一有一个 lambda 表達式 f，予得對於'''N'''著的每著 x , y 攏有 F ( x )=y 若是唯一 f x==y，遮的 x 和 y 分別是對應於 x 和 y 的邱奇數。這是定義可計算性的足濟種方式之一；就關於其他的方式佮𪜶的等價者的討論請參見邱奇-圖靈論題。

==lambda 演算佮程式語言==

===匿名函式===

譬如計算平方的函式 square 佇咧 Lisp 中會當表示為下的 lambda 表達式符號 lambda 建立一个匿名函式，予定參數列 ( x )，閣有一个做為函式體的表達式( \ * x x )。匿名函式有時叫做 lambda 表達式。

誠濟命令式的語言攏有函式的指標抑是類似的機制。但是函式指標並毋是類型中的一等公民，函式是一等公民若而且唯若函式會當佇執行的時陣建立。下跤一寡語言支援函式的執行的時建立：Smalltalk、JavaScript、Kotlin、Scala、Python 三、C # ( " delegates " )、C + + 十一等。

===化簡策略===

===關於著複雜度的註解===

===伊並行佮伊並發===

==參見==

* 邱奇-圖靈論題
* 遞迴函式
* 可計算函式
* 柯里化

==參考文獻==

==外部連結==

* L . Allison , Some executable λ-calculus examples
* Georg P . Loczewski , The Lambda Calculus and A + +
* To Dissect a Mockingbird : A Graphical Notation for the Lambda Calculus with Animated Reduction
* 人物介紹
* 神奇的呢 λ 演算
* ( 譯 ) The Y combinator ( Slight Return )
* Λ 運算 ︰ 淵源介紹

[[分類: 待校正]]