【发布时间】：2017-11-22 16:15:18
【问题描述】：
我对 lambda 缩减是如何终止的感到困惑。例如，数字 2 写成
\xy.xxy
为什么我们不应该继续应用 beta 替换规则并让它像这样
\xy.(x)xy
＝＞\ab.axy
＝＞\b.yx
＝＞y
这显然是错误的。但我不知道为什么。任何人都可以帮助我吗？谢谢！
【问题讨论】：
【发布时间】：2017-11-22 16:15:18
【问题描述】：
如果您在进行替换时遇到问题，我建议您使用完全展开的表单
\xy.xxy
是不是
\xy.(x)xy
是的
λx. λy. (x x) y
可以 eta 化简为
λx. λy. (x x) y
λx. (x x)
λx. x x
在head normal form中，不能进一步减少
在这个特定的问题中不需要测试版替换
【讨论】：