λ 演算

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

极少的构造并不意味着执行行为简单。一个项可以同时含多个 redex，可能存在正规形，也可能无限归约；选择哪个 redex 属于策略，能否汇合或终止属于元理论。把这些问题分开，是 λ 演算作为核心语言的价值。

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

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

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

布尔值可由行为编码：

于是 $\mathsf{true}ab{\to }_{\beta }^{\ast }a$，$\mathsf{false}ab{\to }_{\beta }^{\ast }b$。这里“数据”没有额外标签，只通过选择哪个分支表现自身。

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

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

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

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

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

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