Lambda演算（一）大道至簡

從選擇信息專業開始到回爐讀書爲止，四捨五入碼了八年代碼。對於計算機科學的認知僅限於：

1）使用不一樣語言實現特定功能

2）實現不一樣算法以增進系統性能

3）搭建不一樣架構進行組織管理

 

但從未思考一些本質問題，好比程序中的函數是什麼？系統中的進程是什麼？類是什麼？這些經常使用概念，都會使用，也會用描述加以解釋，但沒有想過須要進行形式化的定義。所以，其實歷來沒有進過計算機科學的大門。

 

上兩個學期修習了Principles of Programming Language, Logic兩門課程，加之瀏覽了一些verification，type theory 和其餘演算的內容，方覺任督二脈始通。要想練得精純內功，輸出難度和效率顯然遠高過輸入。但願在博客總結完成事後，能有透徹的理解。

 

開篇

一切計算機運算過程，均可以歸約於最簡單的模型，好比圖靈機，好比Lambda演算。

 

Lambda演算, 出自Alonzo Church三十年代的書The Calculi of Lambda-Conversion。Alonzo設計Lambda演算的初衷，是爲了以一種通用的形式化方式來表示複雜的計算過程。

 

假設有一羣原始人，他們的數學系統裏用+號來表示兩數相加，卻沒有×號，那麼他們想要表達乘這種運算的時候，只能用..+..+..這種表達式，或者用描述式的「十個加」，一旦他們引入了×號，就至關於有了一種形式化的方法來表達乘運算。

 

儘管現代數學系統裏，除了加號和乘號以外，冪、積分、累加等等運算符號不停地被髮明出來，可是想用它們組成表達式來表示一段計算機程序的運算過程，仍是顯得無比繁瑣。

 

Lambda演算使用了一套極其簡單的符號系統：{λ, ., (, )}以及變量名，就能表示一切圖靈可計算的問題的計算過程，所以，它是一種通用的形式化演算。

 

Alonzo證實了Lambda演算沒法解決可斷定性問題（Entscheidungsproblem） ，它所能實現的計算複雜度是與圖靈機相等的。換句話說，Lambda演算和與圖靈機等價。所以，它是圖靈完備的。

 

下面開始理解Lambda演算： 

 

（一） 函數

數學中的函數，能夠看做一種映射。計算機科學中的函數一樣是一組映射規則，這種規則會將給定的值（參數）映射到結果（返回值）上。在計算機中，這個規則具體表現爲一段操做。這段操做被應用於參數的過程稱做歸約，歸約以後，原有的參數+操做表達式被簡化成一個返回值。

 

這個函數（規則、操做、anything）能夠表示爲 f a。表達式左邊f爲函數名，右邊a爲形參名。

 

如同數學函數有定義域和值域，一個計算機函數所能做用的參數，也有必定範圍。對於超出範圍的a，f a是無心義的。

 

（二）多個參數

當一個函數有兩個參數a，b時，寫做 f a b，狀況變得複雜了一些。令一個函數 g = f a，咱們能夠發現，對於任意定義域內的g，均可以得出g b = f a b。所以，f a b 等價於（f a）b。左邊括號裏的整個表達式爲一個函數（f a），右邊爲變量名b。

 

所以，對於有兩個參數的函數，其歸約過程等效於將函數f應用於第一個參數a，返回一個簡化後的函數g，再將g應用於第二個參數b，返回計算結果。

 

更進一步，三個參數的函數f a b c 可拆解爲單個參數（f a b）c，或兩個參數（f a）b c。不管哪一種拆解方式，最終都歸爲((f a) b) c。

 

將該結論拓展至通常狀況，任意多個參數的函數，最終均可以拆解爲單個參數的函數組合。

 

（三）Lambda符號

假設咱們有一個函數f=x+1，在形式化的表達式中，將用具體的表達式x+1來替換f。假設這個函數是f=x，則以前的 f x, 寫做 x x。咱們並沒有法區分是在討論變量x，仍是談論一個將參數映射到它本身的函數 x。所以，Alonzo引入符號Lambda （λ）來區分這兩種狀況。

x 單純表示一個變量x，λx.x表示一個函數，點號左邊的x指定這個函數的形參是x，右邊表示這個函數的表達式，表達式中的全部x都是形參，在將來的歸約中，都會被實參替換。

 

舉例來講，λx.(x^2-1)，x是參數，x^2-1是函數表達式，表示這個函數返回參數值的平方減一。

 

根據（二）中有關多個參數的討論，λx.λy.（x+y），則等效於λx.（λy.（x+y）），其中λy.（x+y）表示一個函數，這個函數返回參數與x的和，x在此處是一個值不定的量（變量），或者說還沒有綁定值的名字，加上λx.部分後，λy.（x+y）中的x就成了另外一個形參，而這個函數返回的是參數x與參數y的和。