Good math，bad math是我最近發(fā)現的一個博客。作者Mark Chu-Carroll寫的一系列關于計算機科學理論的文章深入淺出，通俗易懂，屬于茶余飯后絕佳的消遣讀物。俺一直想寫點介紹lambda caculus的小文章，但看了他的“My Fravorite Calculus: Lambda” 后，就打消了這個念頭。有這么好的文章，轉貼就行了，自己就不用再寫不入流的文章。今天先轉介紹lamdba calculus的第一部分。先申明一下，俺的翻譯在不影響作者原意的基礎上（但愿能做到到），有時也插科打諢加點8卦。如果誰覺得文章垃圾，完全因為俺 水平有限。原文絕對精彩。另外，俺數學方面的術語止于大一微積分。所以術語用錯了，還請多多指正。

在計算機科學尤其是是編程語言領域，我們常用一種算子：Lambda Calculus。邏輯學家也常用Lambda Calculus 來研究計算和離散數學結構的本質。其實當初Alanzo Church(就是丘奇-圖靈論點里的那位丘奇老大了）和Stephen Cole Kleene(就是自動機理論里Kleene Star那個Kleene了）推出這個Lambda Calculus，也是為了方便他們做邏輯方面的推理，好證明決定性問題。 當然以Church和圖靈的天才，沒多久他們便證明圖靈機和lambda calculus具有等價的計算能力。Church提出Lambda Calculus時就懷疑他的理論能被用在其它地方。事實證明他的確高瞻遠矚。Lambda Calculus在編程的理論和實踐兩方面都意義深遠。做理論和做函數編程的且不說。就算是玩兒腳本語言的老大們，也多半成天和lambda打交道。說來好玩兒，計算機科學理論的發(fā)展相當詭異。常常是邏輯學家為了推進邏輯理論提出一個理論，若干年后計算機科學家出于實際需求再“重新發(fā)現”一模一樣的理論。 比如說現在很多函數編程語言常用的Hindley-Milner類型系統，就是邏輯學家Roger Hindley 于1969年先發(fā)現，再由大名鼎鼎的牛人Robin Milner于1978年獨立提出。說遠了。Lambda Calculus本身有若干顯著優(yōu)點：

1. 它非常簡單。反正比圖靈機簡單。
2. 它圖靈完備。也就是說，圖靈機能完成的計算，Lambda Calculus也能完成。
3. 它易于讀寫。這點很重要。簡單就是力量。我們不可不記。
4. 它的語義足夠強大，能讓我們用它來推理。
5. 它的計算模型足夠強大
6. 容易創(chuàng)建不同的變種，以便我們探索用不同的方式構建計算或語義時的特性

Lambda Calculus易于讀寫意義重大。正是這個優(yōu)點催生了許多或多或少基于lambda calculus的極為優(yōu)秀的編程語言：Lisp, ML, 和Haskell都在很大程度上基于Lambda calculus開發(fā)出來。

Lambda calculus建立在函數這個概念上。純粹的lambda算子理論中，任何東西都是函數。除了函數外別無它物。不過我們可以用函數搭建出各種東西。其實我們可以從lambda calculus開始，從無到有搭建出整個數學的結構。

牛皮轟轟吧？我們就來看一下lambda calculus為什么這么神奇。對任何一個算子理論來說，我們必須先定義兩個東西。一是句法(syntax)，用來描述什么表達式是合法的；二是一套規(guī)則，用來規(guī)定我們怎么對表達式作合法的符號操作。

Lambda Calculus句法

Lambda calculus 只有三種表達式

1. 函數定義：在lambda calculus里一個函數就是一個表達式，寫成lambda x . <函數體>。意思是“一個函數，帶一個參數X，返回計算函數體后得到的結果”。這個時候我們說這個lambda表達式綁定了參數X。
   
2. 標識符引用（identifier reference): 一個標識符引用就是一個名字。這個名字和包括這個引用的函數定義里的參數同名。
   
3. 函數應用(function application): 這個更簡單，把要應用的值放到函數定義的后面就行了。比如
   (lambda x . plus x x) y

這么簡單的定義能干什么囁？怎么沒有多個參數囁？這個就是數學的 魅力了。我們很快會發(fā)現，多個參數可以被等價的操作（所謂的currying)來代替。而配上簡單的操作后（本質操作就一個：替換），我們就得到了一門強 大的編程語言，不輸基于圖靈機模型的Algo系列語言，比如C。

欲知后事如何，且聽下回分解。