为什么要在λ微积分中引入Ycombinator？

Question

我正在读一本关于λ微积分的书“通过Lambda微积分进行功能编程”（格雷格·迈克尔森）。在书中，作者介绍了用于定义函数的简写形式。例如

def identity = λx.x

继续说，我们应该坚持使用速记法时，“所有定义的名称都应用其定义替换[表达式的求值”]

稍后，在介绍递归时，他以加法函数的定义为例，例如：

def add x y = if iszero y then x else add (succ x) (pred y)

并且要说，如果我们没有上述限制，我们将能够通过缓慢扩展它来评估它。但是，由于我们在表达式的求值之前有替换所有定义的名称的限制，因此我们不能这样做，因为我们继续不确定地替换add，因此需要更详细地考虑递归。
因此，我的问题是：对我们自己施加此限制的理论或实践原因是什么？ （必须替换所有定义的名称
before

函数的评估）？有吗

Answer 1

原因是我们希望遵守lambda演算规则。允许术语的名称表示除立即替换以外的其他含义，这意味着在该语言中添加recursive let expression，这意味着我们将需要一个真正更具表达能力的系统（不再是lambda演算）。

您可以认为原始lambda术语的名称不超过syntactic sugar。 Y组合器正是将递归引入没有内置递归的系统的方法。如果您当前正在阅读的书使您感到困惑，则可能需要在互联网上搜索一些其他有关Y组合器的资源。

Answer 2

我将尝试以我理解的方式发布自己的答案。

对于无类型的lambda演算，没有

实际原因，我们需要Y组合器。通过[[practical，我的意思是，如果某人想要构建一个表达式评估器，则可以在不需要组合器并且仅缓慢扩展定义的情况下进行操作。

尽管出于理论上的原因，我们需要确保在定义函数时，该定义具有一定的含义，并且并未就其本身进行定义。例如以下定义没有太大意义：def something = something

出于这个原因，我们需要查看是否有可能以非自引用的方式重写定义，即可以在不引用自身的情况下定义某些内容。事实证明，在无类型lambda演算中，我们始终可以通过Y组合器来做到这一点。

使用Y组合器，我们总是可以构造方程x = f（x）= f（f（x））= ... = f（f（f（f（x（））））=的解。 ..对于任何f，
即。我们总是可以将自引用定义重写为不包含自身的定义]