lambda 演算中的 Eta 抽象有何用途？

Question

lambda 演算中的 Eta 抽象意味着跟随。

函数f可以写成\x -> f x

• Eta 抽象在减少 lambda 表达式时有什么用处吗？
• 它只是某些表达式的另一种书写方式吗？

实际用例将不胜感激。

Answer 1

eta 的减少/扩大只是法律规定的结果

f = g

一定是，对于任何 x

f x = g x

反之亦然。

因此给出：

f x = (\y -> f y) x

通过减少右侧的 beta 值，我们得到

f x = f x

这一定是真的。由此我们可以得出结论

f   = \y -> f y