從選擇資訊專業開始到回爐讀書為止，四捨五入碼了八年**。對於電腦科學的認知僅限於：
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的和。
閱讀計畫2 《大道至簡》
本文寓意於史，自商朝西周中期講起，寫愚公盡一百八十年而不成其事，築城而自守 京城氏世代著書而不知 道 出世而小隱 智叟知時應勢，聚財而不斂，入世而大隱。在 大道至簡 一書中，只論述 工程中的行事之法 因此，便在書末附以此文，來講述比 行事之法 更為重要的 卓立目標，道而馳之 的思想。這本書與其他教科...
03大道至簡閱讀筆記
大道至簡這本書，書如其名，它並沒有告訴你具體的方法與手法，只是敘述了基本的原理和思想。它陳述的是一種途徑 乙個方面，以及一些探求的途徑 方面過程中的故事與思考。我們在進行軟體開發的時候，過程是非常重要的，無論成敗都非常有用，我們所做的一切到最後歐都會變成自己的經歷儲存在自己的知識庫裡。讀完達大道至簡...
測試小故事99 大道至簡
大道至簡。大道理 最有價值的道理是非常簡單和樸素的，用一兩句話就能說清楚。知易行難。簡簡單單，最原始的選擇，是多數人希望的，卻是做起來困難 多數人無法做到。苦苦尋找簡單之法，總不得法，欲速而不達。想偷懶 想省事，想提公升 想實現，總想得道 總想投機。不論做什麼事，總想簡簡單單的成事，少了份堅持，少了...