引入
在 lambda 演算中，所有事物都是函数
lambda 演算式中有三种项：
-
变量
x，形如x -
变量
x在另外一个项t1中的抽象abstraction，形如λx . t1 -
将项
t1作用于t2，形如t1 t2
有如下的简单的递归定义来总结上述三种项的形式：
t ::= x (variable)
λx.t (abstraction)
t t (application)
抽象语法与具体语法
具体语法指程序员直接编写或阅读的代码，比如一段 C++ 代码 x = 1 + 2 * 3;
抽象语法则是更加本质的一种表示，采用抽象语法树 abstract syntax trees 的方式，更清楚地揭示语法中项和项之间关系，对于上面一串代码可能有如下抽象语法树 AST：
=
/ \
x +
/ \
1 *
/ \
2 3
lambda 项表示的是一棵语法树，即使我们写成线性形式（一行）
为了简化 lambda 演算，做出如下两个约定：
-
左结合，意味着
x y t等价于(x y) t -
抽象
abstraction的右部应当尽可能向右拓展（尽可能长），意味着λx . λy . x y x等价于λx . (λy . ((x y) x))
作用域
还需要讨论变量 x 的作用域 scope，也就是 x 什么时候是“自由”的：对于 x，当 x 出现在 λx . t 的 t 中时，我们认为 x 是被约束 bound 的，否则是自由的
一个不含自由变量的项成为封闭项（组合子 combinators），最简单的组合子，称为恒等函数，记作 id = λx . x
操作语义
在原教旨主义纯粹的 lambda 运算中，没有内置的常数，原始运算符等等，“运算”的唯一含义是将函数应用 application 于参数（同样也是函数）上
计算（上文所说的 application）的步骤为将左侧的 abstraction 中的约束变量替换成右侧的参数，记作：
(λx . t12) t2 → [x → t2] t12
[x → t2] 意为由 t2 代换在 t12 中所有自由出现的 x
比如： (λx . x) y 经计算之后为 y
由 Church 的定义，[x → t2] t12 称为一个可归约表达式 redex，并且根据上述操作进行计算的操作称为 beta 规约
下面给出了几个求值策略，用来确定项在下一步求值中如何激活这个可归约表达式
- 全
beta规约full beta-reduction：任何时刻都可以归约任何一个redex，比如：
对于 (λx . x)((λx . x)(λz . (λx . x) z)) ≡ id(id(λz . id (z)))
可以从内向外归约 id(id(λz . id (z))) → id(id(λz . z)) → ... → λz . z
显然从外向内归约可以得到一样的结果
-
常规顺序策略
normal order strategy：外面的redex最先归约 -
按名调用策略
call by name strategy：和常规顺序策略类似，但是不允许在abstraction内部进行归约，同样以上文的例子为例，λz . id z被认为不可进行归约，演算进行到λz . id z就停止了 -
按值调用策略
call by value strategy: 最常用的策略；归约外层redex，且一个 redex 会被归约仅当它的参数已经是一个值value，即一个计算已经完成，已经不能被归约的形式，包括 lambda abstractions，numbers，booleans 等。
本书中采用按值调用策略