Lambda calculus 是數學家 Alonzo Church 發表出來的,是用替換規則來稽考函數的一个形式系統。
原底 lambda calculus 干焦是欲用來研究數學的基礎,毋過後來咱發現伊有真濟袂䆀的應用,所以佇這馬的計算機科學(computer science)、邏輯學甚至是語言學攏會使看著伊的身影。
尤其是這幾冬,有愈來愈濟寫程式的人認捌著講函數型程式設計(functional programming)的理路是誠有智慧,寫 FP 袂輸一件蓋奅的代誌,lambda calculus 嘛綴咧出現佇逐家的面頭前。
雖然伊名後壁的 calculus 佮微積分仝名,無過莫予伊嚇驚著。
lambda calculus 無啥物複雜的運算,嘛無啥物恐怖的符號,干焦一點仔替換規則。
咱佇這篇文內底會對數學函數的概念開始,簡單、直覺的紹介 lambda calculus。
咱凡勢攏捌佇咧高中的數學課學著一點仔函數的概念:咱通共函數當做一个機器,予伊一个物件,經過機器運作了後變做另外一个物件予咱。
咱予函數的物件號做「自變數(independent variable)」,伊應轉來予咱的物件號做「應變數(dependent variable)」。
假使這个函數的名是 ,咱就用 來代表咱予伊 了後的應變數,讀做「 of 」。
比論講有一个函數號做 ,予伊 伊就應 、予伊 伊就應 。
就是隨在咱予 啥物數字 ,伊攏應這个數字的 倍。
咱就通寫做 讀做「 of 平平 」。
佇數學文獻內底,咱嘛定定會共寫做 讀做「 共 映到 」。
若共函數內底的對應關係像按呢共寫起來,欲知影這个函數會按怎應就簡單矣。
比論講欲知影 是偌濟,咱就共正手邊的 換做 ,所以 就是 ,平平 。
咱佇這篇文內底共這款「共 替換作 」的操作寫做 ,那按呢拄才咧計算 的步數就會寫做
毋管是佗一種寫法,咱攏會用一个「抽象」的符號(親像頭前的 )來代表自變數;若應變數內底有佮自變數對應的符號,欲來「應用」這个函數的時陣(親像頭前欲算 ),咱就共彼寡符號攏「替換」做欲予伊的物件(親像頭前的 )就好矣。
嘛是因為寫按呢了後,自變數的符號會含佇咧應變數內底,清國的數學家李善蘭就共應變數號做「函數」(「函」是「包含」的意思),隨著數學的發展,這个名慢慢仔嘛變做今仔日代表規个對應的用法。
李善蘭《代微積拾級》〈凡例〉
一、諸數字之旨各異。函數者,言其數中函元之加、減、乘、約、開方、自乘諸數也;長數者,言幾何漸增漸減之微數也;變數者,言其數或漸變大、或漸變小、非一定之數也;常數者,言其數一定不變也。
李善蘭《代微積拾級》〈卷十 微分一〉
凡此變數中函彼變數,則此為彼之函數。如直線之式為 ,則地為天之函數。又平圜之式為 、橢圜之式為……,皆地為天之函數也。
漢字 天 地 甲 乙 味 丄 丅 意義 x
y
a
b
R
+
-
數學發展到這馬,會當叫做函數(function)的物件早就毋是干焦頭前寫的彼款爾矣。
佇今仔日的數學內底,任何的對應關係,只要伊袂一个應兩三个,按呢伊就通號做是函數,比論下跤的 嘛是函數:
這个 就較僫寫做進前啥物應變數內底有自變數的彼款矣。
雖然按呢寫起來是真方便,毋過咱若欲看這个 到底會按怎應,就無遐直接矣。
比論講,咱若欲知影 是啥,就愛先去檢查講 敢是素數: 毋是素數,所以 。
就是講,若對「計算」的角度來看,咱較有法度來研究的,凡勢干焦上頭前彼種有明確的符號照步來予咱替換、運算的函數爾爾矣。
所以,為著欲單純研究彼款通替換的函數,美國數學家 Alonzo Church 就提出了 lambda calculus 這款系統,專門來操作「抽象」、「應用」、「替換」。
續落來咱就來看講啥物是 lambda calculus。
咱這馬要緊的操作是「抽象」(abstraction)、「應用」(application)、「替換」(substitution)。
比論用進前的數學寫法,咱會當按呢表達定義佮使用一个函數:
Lambda 的寫法其實差無偌濟,會當講是換一个寫法爾爾。
比論講拄才的就寫做
就是講,應用是免括號的;啊抽象的時陣,代表自變數的符號囥佇 佮 的中央,代表應變數的部分囥佇 的後壁。
咱若無想欲共這个函數號名, 嘛會使直接寫做 。
咱欲操作的這款物件號做「lambda 項」,伊是按呢定義:
照按呢定義,下跤的攏是合法的 lambda 項:
為著方便咱寫,咱閣有一寡寫法的約定:
函數內底的符號干焦是佇咱咧應用的時陣予咱參考的對象爾爾,符號是選 抑是選 根本無差別。
這代表講咱嘛會使改變 lambda 項的符號,只要改了袂影響伊的函數意義就好,比論講 會當改做 。
愛注意的是,咱逐擺改符號攏是改規組抽象結構 內底的符號。
這款改符號的變換其實嘛有嚴格的定義,號做「 變換」,毋過彼攏是為著欲予這套 lambda calculus 系統閣較完整,毋免去依賴函數意義。
其實咱簡單對函數改參考符號的意義來理解就會用得矣。
欲算「應用」的時佮函數仝款,若欲算 ,結果就是做「替換」 ,共應變數 內底佮自變數 對應的符號替換做 。
愛注意的是,咱袂使直接共所有仝款的符號替換掉,愛先檢查講伊敢真正有予自變數縛牢。
比論講 欲算上外口應用 的部分,是愛算做 ,毋通算做是 。
咱若欲避免無細膩替換毋著的狀況,會當先透過 變換共每一个 後壁的符號換作全部攏無仝了後才來算。
應用的時陣到底欲按怎替換嘛有嚴格的定義,號做「 簡化」,毋過仝款是為著欲予系統閣較完整爾爾,咱嘛會使直接對函數意義去理解。
凡勢有人看到遮就會問講,像頂頭的 有兩个應用結構,按呢到底是愛先應用外口的 抑是內底的 才著?
其實,咱欲選佗一个代先算攏無要緊,Church–Rosser 定理共咱講選佗一个結果攏仝款。
猶未寫完…