lambda 演算中的 Eta 抽象用于什么？

Question

λ演算中的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

Answer 2

首先，为了澄清术语，转述 Haskell wiki 中 Eta conversion 文章中的一段引述（也包含上述 Will Ness 的评论）：

从\x -> f x 转换为f 将 构成 eta reduction，并以相反的方式移动 将是 eta abstraction 或 expansion。 eta conversion 一词可以指代任一方向的过程。

• 广泛使用 η-reduction 可导致Pointfree programming。
• 它通常也用于某些编译时优化。

找到的用例总结：

1. 无点（风格）编程
2. 允许在使用严格/急切评估策略的语言中进行惰性评估
3. 编译时优化
4. 扩展性

1。无点（风格）编程

来自Tacit programming 维基百科文章：

隐性编程，也称为无点式，是一种编程 函数定义不识别参数的范式 （或“点”）他们操作。相反，定义仅仅是 编写其他函数

从sth's answer 借用一个 Haskell 示例（这也显示了我在这里选择忽略的组合）：

inc x = x + 1

可以改写为

inc = (+) 1

这是因为（在yatima2975's reasoning 之后）inc x = x + 1 只是\x -> (+) 1 x 的语法糖，所以

\x -> f       x   => f
\x -> ((+) 1) x   => (+) 1

（请查看Ingo's answer 以获取完整证明。）

在其用法上有一个good thread on Stackoverflow。 （另见this repl.it snippet。）

2。允许在语言中使用严格/急切的评估策略进行惰性评估

使得在急切/严格的语言中使用惰性求值成为可能。

引用Eta Expansion 上的 MLton 文档：

Eta 扩展会延迟对 f 的评估，直到应用周围的函数/lambda，并且每次应用函数/lambda 时都会重新评估 f。

有趣的 Stackoverflow 线程：Can every functional language be lazy?

2.1 重击

我可能是错的，但我认为 thunking 或 thunks 的概念属于这里。来自the wikipedia article on thunks：

在计算机编程中，thunk 是用于注入 附加计算到另一个子程序中。 Thunks 主要是 用于延迟计算直到需要其结果，或插入 在另一个子程序的开头或结尾进行操作。

Structure and Interpretation of Computer Programs (pdf) 的4.2 Variations on a Scheme — Lazy Evaluation 对thunk 有非常详细的介绍（尽管后者没有出现“lambda calculus”这个短语，但值得一读）。

（这篇论文看起来也很有趣，但还没有时间研究它：Thunks and the λ-Calculus。）

3。编译时优化

完全不了解这个话题，因此只提供来源：

• 来自Georg P. Loczewski's The Lambda Calculus：

  在 Lambda Calculus、A++、SML、Haskell、Miranda 等“惰性”语言中，eta 转换、抽象和归约等主要用于编译器。 （参见 [Jon87] 第 22 页。）

  [Jon87] 扩展到的位置

  西蒙·L·佩顿·琼斯
  The Implementation of Functional Programming Languages
  Prentice Hall International，赫特福德郡，HP2 7EZ，1987。
  国际标准书号 0 13 453325 9.

• search results for "eta" reduction abstraction expansion conversion "compiler" optimization

4。 Extensionality

^{这是另一个我知之甚少的话题，而且是比较理论化的，所以就这样吧：}

来自Lambda calculus 维基百科文章：

η-reduction 表达了extensionality 的思想，在这种情况下，两个函数是相同的当且仅当它们对所有参数给出相同的结果。

其他一些来源：

• nLab 在Eta-conversion 上的条目更深入地探讨了它与可扩展性的联系，以及它与beta-conversion 的关系

• 理论计算机科学 Stackexchange 上 What's the point of η-conversion in lambda calculus? 中的大量信息（但请注意：已接受答案的作者似乎对 eta 减少和可扩展性之间的关系的普遍看法持异议，因此请确保阅读整个页面。大部分内容都在我的脑海中，所以我没有意见。）

• question above has been cross-posted to Math Exchange as well

• 说到“我头上”的东西：这里是Conor McBride's take；我唯一理解的是 eta 转换在某些情况下可能会引起争议，但阅读他的回复是试图找出一种外星语言 (couldn't resist)

^{将此页面递归保存在 Internet 存档中，因此如果任何链接不再存在，那么 that snapshot 可能也已保存这些链接。}