λ演算归约错误排查：推导结果与在线求解器不符怎么办

你的归约存在两个核心规则理解错误：

• λ项结构解析错误：λ抽象的作用域为点号右侧尽可能长的合法表达式，直到遇到不匹配的闭合括号为止，因此λt.yt的函数体仅包含yt，后方的z、x均不在λt的绑定范围内；同时λ演算的应用默认左结合，M N P等价于(M N) P，因此(λy.λt.yt)zx的实际结构是((λy.λt.yt)z)x：即先把λy.λt.yt作用于参数z，得到的结果再作为函数作用于参数x，而非把zx整体作为参数传给λy，也不是把zx划入λt的函数体。
• β归约逻辑错误：当λ抽象被应用到参数时，该λ绑定会被消除，需要把函数体内所有对应绑定变量的自由出现替换为参数。你在第一步错误得到λ抽象λt.zxt后，没有意识到λt已经被应用到参数x、应该被消去，反而保留了λt绑定，得到了错误的中间项。

我们先给原式补充括号明确结构，再按β归约规则逐步推导：

1. 原式（补全括号后）：

(λx. y x) ( ((λy. λt. y t) z) x )

2. 先归约最内层的β可归约项(λy. λt. y t) z：将函数体λt.yt中所有被λy绑定的自由y替换为z，得到λt. z t，此时式子变为：

(λx. y x) ( (λt. z t) x )

3. 继续归约内层β可归约项(λt. z t) x：将函数体zt中所有被λt绑定的自由t替换为x，得到z x，此时式子变为：

(λx. y x) (z x)

4. 归约最外层β可归约项(λx. y x) (z x)：注意最外层λx的绑定作用域仅覆盖自身函数体yx，后方参数里的x是自由变量，不受该λx绑定；将函数体yx中被λx绑定的自由x替换为参数zx，得到：

y (z x)

注：如果在线求解器返回结果为yx，通常是原式输入存在偏差：比如将内层的λt.yt误写为λt.t时，((λy.λt.t)z)x会归约为x，最终结果就是yx，和求解器结果一致。

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