λ-演算中的归约策略 λ-演算的归约策略决定了表达式求值的具体顺序，对计算终止性和效率有直接影响。以下分步骤展开说明： 基础概念：β-可约式与归约路径 λ-项中形如 (λx.M)N 的子项称为 β-可约式 （redex）。对该子项进行替换操作 [N/x]M 称为一次β-归约。一个项可能包含多个β-可约式，选择不同可约式会形成不同的 归约路径 。例如项 (λx.x)((λy.y)z) 包含两个可约式，分别对应外层抽象和内层抽象。 标准归约策略：最左最外 最左最外归约 （Normal Order Reduction）始终选择位置最靠左且最外层的可约式进行归约。此策略保证若能得到范式，则必能通过有限步归约到达（标准化定理）。例如对 (λx.y)((λz.zz)w) ，最左最外策略会跳过内层可约式 (λz.zz)w ，直接归约外层可约式得到 y 。 严格归约策略：最左最内 最左最内归约 （Applicative Order Reduction）优先归约最左且最内层的可约式，即先求值函数参数再应用函数。例如对 (λx.xx)((λy.y)z) ，会先归约参数 (λy.y)z → z ，再得到 (λx.xx)z → zz 。此策略可能无法终止（如参数包含发散项时），但与实际编程语言求值顺序更接近。 惰性求值：按需调用 在 按名调用 （Call-by-name）策略中，函数调用时直接替换参数（不预先求值），但同一参数可能被多次求值。 按需调用 （Call-by-need）通过共享机制优化此过程，首次求值参数后保存结果供后续使用，形成惰性求值。例如在 (λx.x+x)(complex_term) 中，按需调用会确保 complex_term 仅计算一次。 策略的语义影响与一致性 所有归约策略均满足 合流性 （Church-Rosser定理）：若项可通过不同路径归约为范式，则这些范式在α-等价意义下唯一。但不同策略的终止性不同：最左最外策略最具终止性，而严格策略在参数发散时可能导致范式无法到达。例如 (λx.y)(ΔΔ) （其中 Δ=λx.xx ）在最左最外策略下一步得 y ，而在最左最内策略下会无限循环。