(参考：《type and Programming Languages》)
一、语法：
t ::= terms:
x variable
λx.t abstraction
t t application
λx.t 可理解为：一个函数，以变量x为参数，返回term t。t是该抽象的body。（lamda表达式的body总是延伸得尽可能长）
l 若x在λx.t 的t中出现，称x由该抽象约束（bind），称λx是一个范围为t的binder。
l 若x出现在某位置，且没有被一个封闭的x上的抽象约束，则称x是自由的（free）。 例如：x y 和 λy. x y 中的x
l 若一个term中不含自由的变量，则称之为闭合的（closed），或称之为一个combinator。
二、操作的语法：
在上面的语法定义中没有内建常数和基本运算符等等，因此唯一的“计算”就是将函数作用于参数（同样也是函数）。
一步计算相当于将一个application重写：用其右手边的元素替代其左手边的abstract的body中的bound variable。即：
其中右边部分表示：将t1中所有的自由的x替换为t2。
例：(λx.x) y → y
(λx.x (λx.x))(u r) → u r (λx.x)
【因为左边的抽象的body： x (λx.x) 中，只有第一个x是自由的。】
形如的term称为redex("reducible expression")；而使用上面的规则重写一个redex，称为beta-reduction。
三、lambda-calculus的求值策略：
1.full beta-reduction：any redex may be reduced at any time。
2.normal order strategy：最左侧的、最外侧的redex总是被优先化简/归约。
3.call by name strategy：不允许在抽象内部的归约。
4.call by value strategy：使用最广泛。（only outermost redexes are reduced？）
四、用Lamda表达式编程
1. 多个参数：使用高阶函数。
例如以一个值对为参数，返回s的函数 f = λ(x, y).s 可写为 f = λx.λy.s ，其含义为“f是一个函数：传入参数u作为x、返回一个传入参数v作为y返回结果s的函数”。则 f u v => λy.[x → u]s v => [y → v][x → u]s
2. Church Booleans
定义term tru和fls如下（区别于常量true和flase）：
tru = λt. λf. t;
fls = λt. λf. f;
则tru v w 返回v；fls v w 返回w。
则可以定义布尔操作如： and = λa. λb. a b fls，则仅在u、v均为tru时 and w v 返回tru，否则返回fls。
3. Pairs
我们可将值对定义为term：
pair = λa. λb. λf. f a b; 这里f应是tru或fst
fst = λp. p tru; 这里的p都是pair
snd = λp. p fls;
例： fst (pair v w) → fst (λb. b v w) → (λp. p tru) (λb. b v w) → (λb. b v w) tru → tru v w → v
4. Church Numerals
定义Church Numerals如下：
c0 = λs. λz. z;
c1 = λs. λz. s z;
c2 = λs. λz. s (s z);
c3 = λs. λz. s (s (s z));
...
每个数字n表示为一个combinator cn ：传入两个参数s和z（分别代表"successor"和"zero"），将s作用于z上n次。
则我们可定义successor函数如下：
scc = λn. λs. λz. s (n s z);
scc是一个combinator，传入一个Church numeral n，返回其后继。
类似的，可定义：
plus = λm. λn. λs. λz. m s (n s z);
times = λm. λn. m s (plus n) c0;
iszro = λm. m (λx. fls) tru;
减法的实现较复杂，通过predecessor function：传入c0返回c0、传入ci+1返回ci。函数ss以一个pair ci cj为参数，返回pair cj cj+1。因此将ss m次应用于pair c0 c0可得到pair c0 c0（当m=0）或pair cm-1 cm（当m>0）。
zz = pair c0 c0;
ss = λp. pair (snd p) (plus c1 (snd p));
prd = λm. fst (m ss zz);
6. Enriching
从前面可以看出，布尔值、数字以及其上的操作可以由纯lamda表达式编码。为了便捷可引入基本的布尔和数值类型。将丰富后的系统称为λNB。在λNB中的两种表达方式可互相转换。要将一个Church boolean转化为一个基本布尔值，只需将其作用于true和false：
realbool = λb. b true false;
而反方向的转化则通过if表达式：
churchbool = λb. if b then tru else fls;
而Church numeral上的一个返回真布尔值的equality function可写为：
realeq = λm. λn. (equal m n) true false;
类似的，将一个Church numeral转化为一个对应的基本数值，通过将其作用于succ和0：
realnat = λm. m (λx. succ x) 0;
7. Recursion
前面讲到，不能再应用求值法则的term称为normal form。然而一些term并不能被求值到normal form。例如下面的divergent combinator：
omega = (λx. x x) (λx. x x);
只含有一个redex，而将其归约后得到的结果仍是omega 本身。
没有normal form的term称做diverge。
omega combinator可一般化地称为fixed-point combinator（call-by-value Y-combinator），可用以定义递归的函数，例如下面的factorial函数：
fix = λf. (λx. f (λy. x x y)) (λx. f (λy. x x y));