λ演算

λ演算用很少的语法讨论计算：名字表示变量，抽象表示接收参数的函数，应用表示把一个表达式交给另一个表达式处理。函数与参数处在同一种表达式体系中，所以函数本身也可以作为输入或结果。这种简化让研究者能够把注意力放在计算规则，而不是具体机器指令。

参考：[1]

对一个函数抽象应用参数时，可以把函数体中相应的自由出现替换为参数表达式，这类步骤称为β归约。替换必须避免意外捕获名字，否则原来独立的变量可能被误认成内层参数。适当改名不会改变绑定关系，因而研究会区分名字的表面写法与表达式实际的结构。

参考：[2]

一个表达式可能包含多处可以继续归约的位置。先求参数还是先展开函数体，会影响中间过程；某些表达式沿一种策略能得到结果，沿另一种策略却持续计算。无类型λ演算还存在没有正规形的表达式，因此不能因为规则简单，就推断每个表达式最终都会得到一个可用数值。

参考：[1]

λ演算参与了对有效计算的形式化，其可表达能力与其他经典计算模型之间有严格联系。实际语言借用lambda名称和函数抽象时，通常还加入类型、状态与输入输出，语义不等于直接照搬无类型演算。理解它的价值，在于用清楚的模型分析绑定、函数与求值，而不是把所有函数语言视为同一种系统。

参考：[2]