介紹如何進行簡單lambda演算的計算（規約）：形如下面這樣的題目：
intro
https://www.jianshu.com/p/ebae04e1e47c 這一篇很清晰，基本涵蓋了本文的內容。
可跳過本節，基本對做題沒幫助
關鍵字
小寫單字符用以命名參數，也叫變量（數學含義的）。
外加四個符號'('，')'，'.'，'λ'。
由它們組成符號串叫λ表達式，核心λ演算表達式是非常冗長的(見下文).為了清晰和簡煉，再加上一類符號：
大寫單字符、 特殊字符(如+、-、*、/)、大小寫組成的標識符代替一個λ表達式。
EBNF語法
<λ-表達式> ：： = <變量>
| λ<變量>.<λ-表達式>
| (<λ-表達式><λ-表達式>)
| (<λ-表達式>)
<變量> ：： =<字母>
表達式的四種形式分別對應：（表達式也稱公式，）[1]
- 標識符引用（Identifier reference）：標識符引用就是一個名字（實參），這個名字用於匹配函數表達式中的某個參數名。
- 函數定義：Lambda演算中的函數是一個表達式，寫成：
lambda x . body，表示“一個參數(形參）為x的函數，它的返回值為body的計算結果。” 這時我們說：Lambda表達式綁定了參數x。 - 函數應用（Function application）：函數應用寫成把函數值放到名字前面的形式，如
(lambda x . plus x x) y。 - 加括號仍是表達式
變量
作為變量的標識符可以代表參數或名字。
閉包（closure）或者叫完全綁定（complete binding）。在對一個Lambda演算表達式進行求值的時候，不能引用任何未綁定的標識符。如果一個標識符是一個閉合Lambda表達式的參數，我們則稱這個標識符是（被）綁定的；如果一個標識符在任何封閉上下文中都沒有綁定，那么它被稱為自由變量。
函數
函數是頭等程序對象（函數是值），可作為函數的輸入輸出。
縮寫與變形
-
用λ演算表示計算首先要表示域，由於λ演算系統的值也是公式，則每個域中先定義最基本幾個公式，其它值通過演算實現。這樣，表示計算的問題全集中在λ演算上了。由於λ演算中一切語義概念均用λ表達式表達。為了清晰采用命名替換使之更易讀。
T = λx.λy.x //邏輯真值 F = λx.λy.y //邏輯假值 1 = λx.λy.x y //數1 2 = λx.λy.x(x y) //數2 n=λx.λy.x(x(…(x y)…)//n個x zerop = λn.n(λx.F)T //判零函數 + = add = λx.λy.λa.λb.((x a)(y a)b)zerop中的F、T可以用λ表達式展開，其它用法同。
-
庫里化：將兩個參數的函數變為兩個單參數函數：寫只有一個參數的函數，而這個函數返回一個帶一個參數的函數。
庫里化的原因是 核心的λ演算只有單目運算，例如：add 1它返回的結果是函數，再應用到后面的表達式上。這樣，3+4就寫add 3 4，add 3返回“加3函數”應用到4上當然就是7。寫全了是：
（λx.λy.λa.λb.((x a)(y a) b )）(λp.λq.(p p(p q)))(λs.λt.(s s s(s t))) =λa.λb.(a(a(a(a(a(a(a b)))))))
λa.λb.λc.λz.E = λabcz.E
= λ(abcz).E
= λ(a，b，c，z).E
= λa.(λb.(λc.(λz.E)))//庫里化，因為語法中lambda后只有一個 變量
- 命名 以大寫單字符或標識符命名其λ表達式：
G = (λx.(y(yx)))
((λx.(y(yx)))(λx.(y(yx)))) = (G G) = H
規約
Lambda演算（規約）只有兩條真正的法則：稱為Alpha和Beta。Alpha也被稱為「轉換」，Beta也被稱為「規約」。λ函數的語義是它應用到變元上所實現的數學函數計算。從符號演算的角度應用就是符號表達式的歸約(reduction)，歸約將復雜的表達式化成簡單形式，即按一定的規則對符號表達式進行置換。
法則
(1) β歸約，β歸約的表達式是一個λ應用表達式(λx.M N)，其左邊子表達式是λ函數表達式，右邊是任意λ表達式。β歸約以右邊的λ表達式置換函數體M中λ指明的那個形參變量。形式地，我們用[N/x,M]表示對（λx.M N）的置換。
先看一例，相互歸約的符號標以下橫線。
例11-4 歸約數1的后繼
(succ 1) => (λn. (λx.λy.n x(x y))1) //寫出succ的λ表達式
=> (λx.λy.（1 x(x y))）
=> (λx.λy.（(λp.λq.p q) x(x y))） //寫出1的λ表達式
=> (λx.λy.（(λq. x q)(x y))
=> (λx.λy.x(x y))=2 //按定義
(2) α 換名 歸約中如發生改變束定性質，則允許換名(λ后跟的變量名)，以保證原有束定關系。例如：
(λx. (λy.x)) (z y) //(z y)中y是自由變量
=> λy.(z y) //此時(z y)中y被束定了，錯誤！
=> (λx.(λw.x))(z y) //因(λy.x)中函數體無y，可換名
=> λw.(z y) // 正確！
(3) η 歸約 是消除一層約束的歸約，形如λx.F x的表達式若x在F中不自由出現，則：
λx.F x => F
它的逆是任何一個F都可以加一套λx( )x，只要x在F中不自由出現。
顯然，λx.f(x) => f 是β歸約的特例。
優先級 【難點】
注意規約中的優先級比較混亂，其實按照λ演算的運算規則，誰先歸約最后歸約其結果是一樣的。（Church-Rosser定理）每次歸約只要找到可歸約的子公式(λ應用表達式，即一個是λ函數表達式，一個是變元)即可歸約，λ演算沒有規定順序。
比如
λx.λy.x y a b
= λx.(λy.x y) a b //庫里化的定義
=(λy.a y) b //合並前三項
=a b//去掉括號，括號可以任意添加，然后合並前三項
空格是可以無視的，主要看括號。那些基本范式的參數后面的body是默認加括號的，比如zerop = λn.n(λx.F)T 其實應該是λn.(n(λx.F)T)
其實括號也是隨意的 以下表達式有相同的語義：
(fa)，f(a)，(f)a，(f)(a)，((f)(a))
比如
λa.λb.((1 a) (1 a) b)
= λa.λb.((1 a) 1 a b )
= λa.λb.((1 a) λx. λy. x y a b)
= λa.λb.((1 a) (a b))
= λa.λb.(( λx. λy. x y a) (a b))
= λa.λb.( λx. λy. x y a (a b))//去括號
= 2
不過2的范式里確實是有括號的，這一點很迷
規約的語義
對應用表達式符號歸約時，當施行（除α規則外）所有變換規則后沒有新形式出現，則這種λ表達式叫范式。（並非所有λ表達式均可歸約為范式。前述(λx.x x)(λx.x x)為不可歸約的。）范式即λ演算的語義解釋，歸約后形如λx.F它就是函數，形如x x，(y (λx.z))就只能解釋為數據了，只可以把它放在另一個應用中作變元進一步歸約。
一些規則
有以下規則：
[1]若x不在M中自由出現，結果為M；
[2]若M = x,結果為N；
[3]若M = λy.k, x≠y,y不在N中自由出現，結果為λy.[N/x,k]；
[4]若M = λy.k, x≠y,y在N中自由出現，結果為λz.[N/x,[z/y,k]],z≠x≠y且不在M,N