Try   HackMD

啥物是 Lambda Calculus

話頭

Lambda calculus 是數學家 Alonzo Church 發表出來的,是用替換規則來稽考函數的一个形式系統。
原底 lambda calculus 干焦是欲用來研究數學的基礎,毋過後來咱發現伊有真濟袂䆀的應用,所以佇這馬的計算機科學(computer science)、邏輯學甚至是語言學攏會使看著伊的身影。
尤其是這幾冬,有愈來愈濟寫程式的人認捌著講函數型程式設計(functional programming)的理路是誠有智慧,寫 FP 袂輸一件蓋奅的代誌,lambda calculus 嘛綴咧出現佇逐家的面頭前。

雖然伊名後壁的 calculus 佮微積分仝名,無過莫予伊嚇驚著。
lambda calculus 無啥物複雜的運算,嘛無啥物恐怖的符號,干焦一點仔替換規則。
咱佇這篇文內底會對數學函數的概念開始,簡單、直覺的紹介 lambda calculus。

函數

咱凡勢攏捌佇咧高中的數學課學著一點仔函數的概念:咱通共函數當做一个機器,予伊一个物件,經過機器運作了後變做另外一个物件予咱。
咱予函數的物件號做「自變數(independent variable)」,伊應轉來予咱的物件號做「應變數(dependent variable)」。
假使這个函數的名是

f,咱就用
f(x)
來代表咱予伊
x
了後的應變數,讀做「
f
of
x
」。

比論講有一个函數號做

g,予伊
3
伊就應
30
、予伊
12
伊就應
120

就是隨在咱予
g
啥物數字
n
,伊攏應這个數字的
10
倍。
咱就通寫做
g(n)=10n
讀做「
g
of
n
平平
10n
」。
佇數學文獻內底,咱嘛定定會共寫做
g:n10n
讀做「
g
n
映到
10n
」。
若共函數內底的對應關係像按呢共寫起來,欲知影這个函數會按怎應就簡單矣。
比論講欲知影
g(23)
是偌濟,咱就共正手邊的
n
換做
23
,所以
g(23)
就是
10×23
,平平
230

咱佇這篇文內底共這款「共
x
替換作
a
」的操作寫做
[a/x]
,那按呢拄才咧計算
g(23)
的步數就會寫做
g(23)=10n[23/n]=10×23=230.

毋管是佗一種寫法,咱攏會用一个「抽象」的符號(親像頭前的

n)來代表自變數;若應變數內底有佮自變數對應的符號,欲來「應用」這个函數的時陣(親像頭前欲算
g(23)
),咱就共彼寡符號攏「替換」做欲予伊的物件(親像頭前的
[23/n]
)就好矣。
嘛是因為寫按呢了後,自變數的符號會含佇咧應變數內底,清國的數學家李善蘭就共應變數號做「函數」(「函」是「包含」的意思),隨著數學的發展,這个名慢慢仔嘛變做今仔日代表規个對應的用法。

李善蘭《代微積拾級》〈凡例〉

一、諸數字之旨各異。函數者,言其數中函元之加、減、乘、約、開方、自乘諸數也;長數者,言幾何漸增漸減之微數也;變數者,言其數或漸變大、或漸變小、非一定之數也;常數者,言其數一定不變也。

李善蘭《代微積拾級》〈卷十 微分一〉

凡此變數中函彼變數,則此為彼之函數。如直線之式為

=,則地為天之函數。又平圜之式為
=
、橢圜之式為……,皆地為天之函數也。

漢字
意義 x y a b R + -

數學發展到這馬,會當叫做函數(function)的物件早就毋是干焦頭前寫的彼款爾矣。
佇今仔日的數學內底,任何的對應關係,只要伊袂一个應兩三个,按呢伊就通號做是函數,比論下跤的

ψ 嘛是函數:
ψ(x)={1,若是講 x 是素數;0,若是講 x 毋是素數。

這个
ψ
就較僫寫做進前啥物應變數內底有自變數的彼款矣。
雖然按呢寫起來是真方便,毋過咱若欲看這个
ψ
到底會按怎應,就無遐直接矣。
比論講,咱若欲知影
ψ(2117)
是啥,就愛先去檢查講
2117
敢是素數:
2117=29×73
毋是素數,所以
ψ(2117)=0

就是講,若對「計算」的角度來看,咱較有法度來研究的,凡勢干焦上頭前彼種有明確的符號照步來予咱替換、運算的函數爾爾矣。
所以,為著欲單純研究彼款通替換的函數,美國數學家 Alonzo Church 就提出了 lambda calculus 這款系統,專門來操作「抽象」、「應用」、「替換」。
續落來咱就來看講啥物是 lambda calculus。

啥物是 Lambda?

Lambda 的定義

咱這馬要緊的操作是「抽象」(abstraction)、「應用」(application)、「替換」(substitution)。
比論用進前的數學寫法,咱會當按呢表達定義佮使用一个函數:

抽象f:x3x+5應用f(10)
Lambda 的寫法其實差無偌濟,會當講是換一个寫法爾爾。
比論講拄才的就寫做
抽象f=λx.3x+5應用f 10

就是講,應用是免括號的;啊抽象的時陣,代表自變數的符號囥佇
λ
.
的中央,代表應變數的部分囥佇
.
的後壁。
咱若無想欲共這个函數號名,
f 10
嘛會使直接寫做
(λx.3x+5) 10

咱欲操作的這款物件號做「lambda 項」,伊是按呢定義:

  • 【變數】咱有一堆符號
    {x,y,}
    ,內底的任何一个符號攏通算是一个 lambda 項;
  • 【抽象】若講
    x
    是咱的符號、
    M
    是一个 lambda 項,按呢
    λx.M
    嘛是一个 lambda 項;
  • 【應用】若講
    N
    M
    攏是 lambda 項,按呢
    N M
    嘛是一个 lambda 項;
  • 若有需要,通添括號
    ()
    予咱的表達閣較清楚;
  • 為著表達方便,會當共一寡物件當做 lambda 項罔用,比論講數字
    3
    、運算
    x+y

照按呢定義,下跤的攏是合法的 lambda 項:

x
x x
λx.x
x y
(x y) z
x (y z)
λx.y
λx.(λy.x)
λx.(x y)
(λx.x) y
x (λy.y)
(λx.x) (λy.y)

為著方便咱寫,咱閣有一寡寫法的約定:

  • 應用是「對倒爿結合(left-associative)」的,就是講
    L M N
    是代表
    (L M) N
  • 抽象的範圍是
    λ.
    後壁(佮伊仝一個括號內底的)規句,就是講
    • λx.M N
      代表
      λx.(M N)
    • (λx.M) N
      的括號袂當省;
  • λx.λy.M
    會當直接寫
    λxy.M

α
變換

函數內底的符號干焦是佇咱咧應用的時陣予咱參考的對象爾爾,符號是選

x 抑是選
y
根本無差別。
這代表講咱嘛會使改變 lambda 項的符號,只要改了袂影響伊的函數意義就好,比論講
λx.y x
會當改做
λz.y z

愛注意的是,咱逐擺改符號攏是改規組抽象結構
(λ)
內底的符號。
這款改符號的變換其實嘛有嚴格的定義,號做「
α
變換」,毋過彼攏是為著欲予這套 lambda calculus 系統閣較完整,毋免去依賴函數意義。
其實咱簡單對函數改參考符號的意義來理解就會用得矣。

β
簡化

欲算「應用」的時佮函數仝款,若欲算

(λx.M) N,結果就是做「替換」
M[N/x]
,共應變數
M
內底佮自變數
x
對應的符號替換做
N

愛注意的是,咱袂使直接共所有仝款的符號替換掉,愛先檢查講伊敢真正有予自變數縛牢。
比論講
(λ\colorredx.(λ\colorgreenx.\colorgreenx+1) (\colorredx+1)) 3
欲算上外口應用
3
的部分,是愛算做
(λx.x+1) 4
,毋通算做是
(λx.4) 4

咱若欲避免無細膩替換毋著的狀況,會當先透過
α
變換共每一个
λ
後壁的符號換作全部攏無仝了後才來算。
應用的時陣到底欲按怎替換嘛有嚴格的定義,號做「
β
簡化」,毋過仝款是為著欲予系統閣較完整爾爾,咱嘛會使直接對函數意義去理解。

凡勢有人看到遮就會問講,像頂頭的

(λ\colorredx.(λ\colorgreenx.\colorgreenx+1) (\colorredx+1)) 3 有兩个應用結構,按呢到底是愛先應用外口的
(λ\colorredx.) 3
抑是內底的
(λ\colorgreenx.\colorgreenx+1) (\colorredx+1)
才著?
其實,咱欲選佗一个代先算攏無要緊,Church–Rosser 定理共咱講選佗一个結果攏仝款。
(λ\colorredx.(λ\colorgreenx.\colorgreenx+1) (\colorredx+1)) 3共符號攏換無仝 α (λ\colorredx.(λ\colorgreeny.\colorgreeny+1) (\colorredx+1)) 3若是外口的 \colorredx 先應用 [3/\colorredx]β (λ\colorgreeny.\colorgreeny+1) 4 [4/\colorgreeny]β 5若是內底的 \colorgreeny 先應用 [(\colorredx+1)/\colorgreeny]β (λ\colorredx.\colorredx+2) 3 [3/\colorredx]β 5

啥物攏是 Lambda

猶未寫完…