λ 演算

λ 演算把计算压缩成“抽象接受实参”。变量给出引用，抽象形成函数，应用把函数与实参相接，β-步骤再以代入实现调用。函数与参数采用同一种项语法，所以函数能够接收函数、返回函数，也能把自身作为数据传递。

极少的构造并不意味着执行行为简单。redex 是应用节点左侧已经出现抽象的局部形状；不必先计算整个函数体才能辨认。例如 $(\lambda x.x)((\lambda y.y)z)$ 有内外两个 redex。先收缩外层会留下 $(\lambda y.y)z$，先收缩内层会得到 $(\lambda x.x)z$，两条路径再各走一步都到 $z$。这个小例子展示“选择归约位置”和“最后得到什么”是不同问题；所有分叉的可汇合性仍需要一般定理证明。

恒等函数满足 $(\lambda x.x)y{\to }_{\beta }y$。下面的项暴露了绑定边界：

若把参数 $y$ 直接文本替换进函数体，会得到 $\lambda y.y$，原本自由的 $y$ 被内层抽象错误捕获，项的含义已经改变。正确做法先把内层绑定变量 α-换名：

结果中的 $y$ 仍然自由，$z$ 才是函数参数。两种结果 $\lambda y.y$ 与 $\lambda z.y$ 既不字面相等，也不 α-等价；错误捕获确实改变了项。

布尔值可由行为编码：

应用左结合，故 $\mathsf{true}ab$ 先视为 $((\lambda t.\lambda f.t)a)b$。对绑定变量适当换名后，两步为 $(\lambda f.a)b\to a$；$\mathsf{false}ab$ 则先得到 $(\lambda f.f)b$，再得到 $b$。这里“数据”没有额外标签，只通过选择哪个分支表现自身。

这种选择行为不自动等于实用语言中的短路条件式。若调用值求值器在调用前求出两个分支，$\mathsf{true}a\mathrm{\Omega }$ 仍会在第二实参上发散；要延迟未选分支，可先把分支包装成函数，再只调用被选中的那个。编码能否实现预期控制行为，必须连同求值策略一起判断。

无类型演算允许自应用。令

则 $\mathrm{\Omega }{\to }_{\beta }\mathrm{\Omega }$。项 $(\lambda x.y)\mathrm{\Omega }$ 收缩最外层可得正规形 $y$，若持续归约参数却会发散。它同时说明三个边界：闭项未必终止，存在正规形不代表所有归约路径终止，完整 β-归约也不等于某个确定求值器。

λ 演算是函数式语言与操作语义理路操作语义Operational semantics以配置、推导规则和转移关系规定程序怎样执行及其可观察结果。的理论原型。替换语义直接把实参写入函数体；环境解释器则把函数表示为代码与定义环境组成的闭包理路程序语言闭包Programming-language closure · Function closure · Lexical closure将函数代码与其定义位置的词法环境配对而成的运行时函数值。。两种实现路径必须给出相同的词法绑定行为。

无类型演算可用不动点组合子理路不动点组合子与递归Fixed-point combinator在无类型 λ 演算中把函数送到它自身的不动点，从而在没有递归原语时表达递归。在没有 let rec 原语时构造一般递归，具体 $Y/Z$ 展开与策略边界由专页承担。

β-归约理路β-归约Beta reduction收缩函数应用 redex，以无捕获替换把实参代入函数体的一步改写关系。、Church–Rosser 定理理路Church–Rosser 定理Church–Rosser theorem · Confluence theorem for beta-reduction完整 β-归约的合流定理：任意有限分叉都能继续归约到共同后继。和正规化理论分别刻画局部计算、分叉汇合与终止。简单类型 λ 演算理路简单类型 λ 演算Simply typed lambda calculus · STLC以基础类型和箭头类型约束 λ 项，获得类型安全与强正规化的最小函数演算。加入类型限制，排除 $\mathrm{\Omega }$ 一类项并获得强正规化。

在可计算性侧，无类型 λ 演算与图灵机刻画同一类可计算函数；在逻辑侧，类型化 λ 项通过 Curry–Howard 对应承担证明对象的角色。前者允许一般非终止，后者的终止性取决于具体类型系统。