從選擇信息專業開始到回爐讀書為止，四舍五入碼了八年代碼。對於計算機科學的認知僅限於：
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的和。