λ演算中的标准型与求值策略 我们先从λ演算中最基本的概念开始。λ项由变量、抽象和应用构成。当一个λ项无法再进行任何β归约时，我们就说它达到了 范式 。范式代表了计算的结果，是λ演算中的“最终答案”。 然而，存在一些λ项，它们可以通过不同的归约路径得到不同的范式，甚至有些路径永远无法终止。这就促使我们研究 求值策略 ——即规定归约顺序的规则。求值策略决定了我们先归约哪个redex（可归约式）。 最常见的两种策略是： 按名调用 ：只归约最外层、最左侧的redex，且不事先归约函数体 按需调用 ：按名调用的优化版本，避免对同一表达式重复求值 这两种策略都是 惰性求值 ，只有在必要时才进行归约。与之相对的是 严格求值 （如按值调用），它要求先对参数完全求值。 理解这些基础后，我们来看 标准型定理 ：如果一个λ项存在范式，那么通过始终归约最左侧、最外层的redex（称为 标准归约 ），一定能得到这个范式。这意味着虽然存在多条归约路径，但至少有一条是“可靠”的。 最后， 头范式 是一个重要的中间概念：它是形如λx₁...λxₙ.yM₁...Mₘ的项（头部是变量）。即使某个项没有范式，它也可能有头范式，这对应着计算的部分结果。按名调用和按需调用都能保证：如果头范式存在，就一定能找到它。