λ演算是一個具有與圖靈機(jī)相同計(jì)算能力的形式系統(tǒng)奋姿，由圖靈同學(xué)的老師Alonzo Church于20世紀(jì)30年代提出。
定義
對一個形式系統(tǒng)麸恍，我們的套路就是分析它的語法和語義车伞。λ演算被很多人吹捧上天的優(yōu)點(diǎn)就是它的語法和語義都極度簡單蝉仇，其語法如下：
t := x (variable)
λx.t (abstraction)
t t (application)
類似謂詞邏輯，這里給出綁定和自由變量的定義：
綁定: λx.t中发魄，在t里出現(xiàn)的x稱作被綁定
自由變量: x如果沒有被綁定妒貌，就是一個自由變量
語義規(guī)則只有兩條：
α-conversion: 可以一個abstraction中所有的綁定變量用另一種符號表示
例子: (λx.t[x]) → (λy.t[y])
β-reduction: 可以把一個abstraction中所有綁定出現(xiàn)的變量替換成參數(shù)
例子: ((λx.t) y) → (t[x:=y])
至此，λ演算的定義結(jié)束熄守。
求值
研究語義時蜈垮，我們需要關(guān)心一個語言是否滿足confluence，termination兩條重要性質(zhì)裕照。前者是指同一個式子在不同的推導(dǎo)下會得到同樣的值攒发；后者是指推導(dǎo)過程不會出現(xiàn)死循環(huán)。
為了描述方便晋南，我們定義(λx.t) y這樣的形式叫一個redex惠猿。
對于λ演算，共有4種求值策略：
- full beta-reduction: 每一步都可以隨機(jī)選取一個redex進(jìn)行化簡
- normal-order: 一個λ表達(dá)式可以用一棵樹來表示搬俊，每次只能選擇樹最接近根節(jié)點(diǎn)的redex進(jìn)行化簡（如果同一層有多個redex紊扬，從最左邊的開始）
- call-by-name: 很多同義詞蜒茄，惰性求值，正則序都是
- call-by-value：應(yīng)用序餐屎，每次函數(shù)傳參時檀葛，一定要先求出參數(shù)值
這里偷懶了，想形式化定義這4中求值方法的朋友可以參見TAPL這本書的習(xí)題5.3.6腹缩。
λ演算在full beta-reduction下是滿足confluence性質(zhì)的屿聋，具體證明可以參考Church-Rosser屬性。對于termination藏鹊，我們是很容易寫出一個死循環(huán)的λ表達(dá)式的润讥。
證明圖靈完備性
用λ演算逐步構(gòu)造true，false盘寡，分支結(jié)構(gòu)楚殿，自然數(shù)，加法竿痰，乘法脆粥，減法，不動點(diǎn)影涉，遞歸等概念是很有趣的一個過程变隔，強(qiáng)烈推薦初學(xué)λ演算的朋友自己推導(dǎo)一遍⌒非悖可以參考神奇的λ演算匣缘。
這篇文章在不動點(diǎn)那一節(jié)介紹了著名的Y-combinator，并且展示了它是如何幫助我們找到任意表達(dá)式的不動點(diǎn)的鲜棠。但是在上一節(jié)介紹的call-by-value求值策略下肌厨，Y-combinator卻是會帶來死循環(huán)的遞歸構(gòu)造方法。我們看一個例子：
[定義] Y-combinator: λf.(λx.f(x x)) (λx.f(x x))
[性質(zhì)] Y g = g (Y g)
[例子] g = λf.λn. isZero n then 0 else plus n (f (pred n))
sum = Y g
sum 3 = Y g 3 (1)
= g (Y g) 3 (2)
= g ((λx.g (x x)) (λx.g (x x))) 3 (3)
... ...
死循環(huán)的解釋如下：在(2)步時岔留，(Y g)和3都是g的參數(shù)夏哭，需要先求出(Y g)的值，把g帶入Y之后献联，還需對(x x)優(yōu)先求值竖配，這樣的操作會無限循環(huán)下去。因此在這里介紹一種新的Fixed-point Combinator里逆。
[定義] Fixed-point Combinator: λf. (λx. f (λy. x x y)) (λx. f (λy. x x y))
[性質(zhì)] Fix g = g (Fix g)
[例子] g = λf.λn. isZero n then 0 else plus n (f (pred n))
sum = Fix g
sum 3 = Fix g 3
= g (Fix g) 3
= g ((λx. g (λy. x x y)) (λx.g (λy. x x y))) 3 (*)
= plus 3 (Fix g 2)
= plus 3 (plus 2 (Fix g 1))
= plus 3 (plus 2 (plus 1 0))
= 6
在Fix-point Combinator的推導(dǎo)中进胯，在(*)步驟處，因?yàn)闆]有application原押，滿足call-by-value繼續(xù)向下進(jìn)行的條件胁镐，所以可以繼續(xù)推導(dǎo)下去。
