歷史
萊布尼茨曾有過以下兩個想法：
- 創(chuàng)造一門‘形式語言’，來描述所有可能的問題
- 找到一種方法款筑，可以解決所有該形式語言描述的問題
第二個問題被稱為Entscheidungsproblem（可判定性）腋么。
1936年咕娄，Turing 和 Church 分別推出了兩種不同的模型來解決可計算問題。
Church 提出了一個形式系統(tǒng)叫做 lambda 演算珊擂，并通過這一系統(tǒng)定義了可計算函數(shù)的符號表示圣勒。
Turing 提出了圖靈機(jī)模型费变。
依據(jù)圖靈機(jī)模型，馮諾依曼型計算機(jī)被創(chuàng)造圣贸。指令式語言挚歧，如 Fortran，Pascal 等都是以圖靈機(jī)為基礎(chǔ)吁峻，他們都依賴于狀態(tài)序列滑负。
而函數(shù)式語言，如 ML用含，Lisp矮慕，Haskell等則是以 lambda 演算為基礎(chǔ)。
Lambda
Lambda 演算由3個部分（lambda terms)組成：expressions, variables, abstractions.
lambda terms 定義如下：
<expression> := <name>|<function>|<application>
<function> := λ <name>.<expression> (also called abstraction)
<application>:= <expression><expression>
- name(variables) 為一個無限長的標(biāo)識符集合啄骇，如 V = {v,v',v'',v'''...}
- 表達(dá)式是可以是一個標(biāo)識符或者一個函數(shù)抽象或者是兩者的組合
- 函數(shù)抽象由兩部分組成：頭部和函數(shù)體痴鳄。頭部為 λ 加上一個標(biāo)識符，body 為一個表達(dá)式缸夹。使用 . 進(jìn)行分隔痪寻。一個簡單的例子：
λx.x
函數(shù)應(yīng)用
我們把 FA 稱為函數(shù)應(yīng)用，把表達(dá)式 F 看做是一個算法明未，而表達(dá)式 A 看做一個輸入槽华。
表達(dá)式可以自己應(yīng)用自己, FF，這樣可以實現(xiàn)遞歸趟妥。
函數(shù)應(yīng)用默認(rèn)為左結(jié)合猫态，即 E1E2E3 . . . En == ((E1E2)E3). . . En)
Free and bound variables
在函數(shù)抽象中，如果函數(shù)體中存在的標(biāo)識符存在于頭部, 稱為綁定標(biāo)識符（bound variables）披摄。在函數(shù)應(yīng)用中亲雪，輸入會被代換到綁定的標(biāo)識符上。
不存在于頭部的疚膊，稱為自由標(biāo)識符（free variables)义辕。
比如下面這個表達(dá)式中，x 為 bound variable寓盗，y 為 free variable
λx.xy
注意 λx.xy 與 λx.xz 并不等價灌砖，因為 y 和 z 可能不相等。而 λxy.xy 與 λab.ab 是等價的傀蚌，我們可以通過下面的 alpha 替換得到基显。
Alpha 替換
我們可以在命名不沖突的情況下，把表達(dá)式中綁定的標(biāo)識符替換為其他標(biāo)識符善炫。
(λz.z) ≡ (λy.y) ≡ (λt.t) ≡ (λu.u)
Beta 化簡
在函數(shù)應(yīng)用中撩幽，我們用輸入的表達(dá)式代入到函數(shù)體中綁定的標(biāo)識符上，這一過程稱為 Beta 化簡。
(λx.xy)z
[x:=z] 把 z 代入到函數(shù)體中的 x
zy
一個復(fù)雜的例子：
((λx.x)(λy.y))z
[x:=(λy.y)]
(λy.y)z
[y:=z]
z
柯理化
當(dāng)我們的表達(dá)式有多個參數(shù)的時候窜醉，可以以柯理化的方式表示:
λxy.xy 與 λx.(λy.xy) 是等價的宪萄。
(λxy.xy)wz ≡ (λx.(λy.xy))wz ≡ wz
(λx.(λy.xy))wz
[x:=w]
(λy.wy)z
[y:=z]
wz
Normal form
我們可以通過 Beta 化簡不斷使用一個表達(dá)式去替換另一個表達(dá)式，重復(fù)這一過程榨惰，直到無法再替換后所得到的表達(dá)式稱為 normal form拜英。
一個例子, 2000/100 并不是 normal form，而完全計算后的 2 是 normal form读串。
另一個例子聊记， λx.x 為 normal form， 而 (λx.x)z 不是 normal form恢暖，它可以被化簡為 z排监，這才是 normal form。
并不是所有的表達(dá)式都能化簡到 normal form 的杰捂。比如下面這個例子：
(λx.xx)(λx.xx)
[x:=(λx.xx)]
(λx.xx)(λx.xx)
