生物指數

[拼音]：λ zhuanhuan yansuan

[英文]：calculus of λ-conversion

用以定義可計算函式的形式演算系統。其特點是把函式與函式值明顯區分，並把函式的演算歸結為按一定規則進行一系列的轉換，最後得到函式值。它在遞迴函式論和程式設計語言方面有重要應用。

研究概況

M.熊芬克爾、H.B.柯里和A.丘奇等分別於20年代開始研究組合邏輯和λ演算。丘奇從幾個基本函數出發，構造λ可定義函式類。λ可定義函式與遞迴函式的等價性是丘奇為其論題直觀的可計算函式類等同於遞迴函式類辯護時使用的論證之一。歷史上第一個不可判定問題就是丘奇構造的“任意給定的λ演算的表示式是否有歸約式”。圖靈機可計算函式與一般遞迴函式的等價性是通過λ演算證明的。在遞迴函式論的早期研究中，λ演算起了重要作用。

丘奇最初把λ演算設計為他的一般函式系統的一部分，並試圖使此函式系統成為數學的基礎。S.C.克林和J.B.羅塞證明了這個系統是不一致的。丘奇於1941年提出現有部分作為一致的子理論。1969年D.斯科特構造了該理論的模型，進一步完善了λ演算系統。

基本內容

數學中的函式記法f(x)既可表示函式值，也可表示函式本身。為了避免這種含混，丘奇限定f(x)只表示函式值，而用λxf(x)表示函式。從研究變元取值和函式施用於變元的概念入手，用λ表示式定義函式，用一些嚴格定義的關於λ表示式的轉換規則刻劃函式的計算過程。

λ 表示式

用於從幾個基本函數出發定義可計算函式類。λ表示式是從初始符號（λ，左、右括號，變數字母）開始歸納地定義的：任何變數是λ表示式；如果M、N是λ表示式，則MN是λ表示式；如果M是λ表示式，x是自由出現於M中的變數，則λxM是λ表示式（如果變數x出現在M中某個形如λxM′的子表示式中，則稱x在M中是約束出現的;否則稱x在M中是自由出現的）。表示式λxM表示一個變元的函式，λx稱為約束變數部分，M稱為體部分。以後繼函式f（x）=x+1為例，其λ表示式為λx(x+1)，f(x)施用於整數自變數3可用如下λ表示式表示

f(3)=λx(x+1)(3)

式中子表示式λx(x+1)稱為該λ表示式的運算元部分;子表示式3稱為其運算元部分。於是表示式(MN)表示把運算元部分M施用於運算元部分N，這對應於函式的變數取值為N的情形。函式符號本身也可作為變數賦值。

正整數作為常函式可由λ表示式定義，加、減、乘和乘冪等初等函式也可由λ表示式定義。可由λ表示式定義的函式稱為λ可定義的。丘奇證明，每個部分遞迴函式是λ可定義的，而且每個λ可定義的函式是部分遞迴的，即λ可定義函式與部分遞迴函式是等價的。

轉換規則

λ演算的計算過程，是按照一些嚴格定義的轉換規則，進行λ表示式的轉換。這些規則，保證把一個λ表示式轉換成另一個等價的λ表示式。如果用M[x/N]表示以N代換M中x的自由出現所得到的結果，則λ演算有如下規則：如果y不在M中自由出現，則λxM可用等價的λyM[x/y]代換；如果M的約束變數中既不含x，也不含自由出現於N中的變數，則可用M[x/N]代換λ表示式中任何(λxM)N，也可用(λxM)N代換λ表示式中任何的M[x/N]。按這些規則進行的轉換稱為β轉換。通過修改或新增某些規則，可得到其他型別的轉換。

一個λ表示式如果不再含有λxMA形式的子表示式，則稱為歸約式，它對應於函式值。例如λ表示式λx(x+1)(3)+λx(x+1)（4）經上述規則轉換成(3+1)+(4+1)，這個歸約式對應於函式值 9。任意給定的一個表示式是否有歸約式這個問題，是不可判定的。如果一個λ表示式含有一個以上的形如λxMA的子表示式，則計算的下一步是不確定的。但這種不確定性並不影響計算的最終結果。一般地，如果一個λ表示式的不同轉換序列均導致歸約式，則這些歸約式是等價的。

λ演算與程式設計語言

ALGOL、LISP等程式設計語言的結構與丘奇的λ演算之間存在著一種本質的對應關係。例如，λ 演算中的函式λ(x1x2…xn）M 與 ALGOL 過程之間存在明顯的對應關係：前者的約束變數部分為λ(x1x2…xn)對應於後者的過程引數表；前者的體部分M對應於後者的過程體。λ演算也能反映巢狀子程式和求值次序等結構，可以用作研究某些程式語言的比較自然的模型，函式式語言LISP就是建立在λ演算的基礎上的。