惰性λ演算中"true"的求值逻辑：传入单参数后如何处理？

基础定义回顾 #

λ演算中true的标准定义是接收两个参数并返回第一个参数的函数：

true = \x.\y.x

当对其进行部分应用（仅传入第一个参数a）时，对应的表达式为：

(\x.\y.x) a

归约结果的一致性 #

无论采用惰性求值还是严格求值，上述表达式的归约结果都是：

\y.a

核心疑问解答 #

惰性求值不会直接将\y.a解析为a，原因如下：

• λ演算的β-归约规则要求：只有当函数被完全应用（所有参数均传入）时，才会触发函数体的求值逻辑。\y.a是一个等待接收参数y的函数，只要未传入y，就不会触发下一步归约——哪怕函数体最终不会使用y。
• 惰性求值的核心是“延迟求值，直到必须使用时才计算”，这里的“必须使用”指的是函数被调用（即完成所有参数的传入）。\y.a本身是一个函数值，在未被调用的情况下，不会主动处理其内部的函数体内容。只有当你将\y.a应用到某个参数（比如(\y.a) b）时，惰性求值才会直接返回a（因为y被忽略，无需对传入的b进行求值）。

总结 #

• 仅完成部分应用时，惰性与严格求值的结果一致，均为\y.a
• 惰性求值不会跳过未应用的参数直接返回a，它仅会在函数完全应用时，跳过对未使用参数的求值

内容的提问来源于stack exchange，提问作者Adam Herbst