我正在阅读一本关于 λ 演算的书“通过 Lambda 演算进行函数式编程”（Greg Michaelson）。在书中，作者介绍了定义函数的简写符号。例如
def identity = λx.x
并继续说我们应该坚持在使用这种速记时“所有定义的名称都应该在计算表达式之前被它们的定义替换”
后来，在介绍递归时，他以加法函数的定义为例，例如：
def add x y = if iszero y then x else add (succ x) (pred y)
并且可以说，如果我们没有上面提到的限制，我们将能够通过缓慢扩展来评估这个函数。然而，由于我们有在计算表达式之前替换所有定义的名称的限制，我们不能这样做，因为我们继续无限地替换add，因此需要以更详细的方式考虑递归。
因此，我的问题如下：对我们自己施加这种限制的理论或实践原因是什么？（必须在评估函数之前替换所有定义的名称）？有吗？
我试图通过添加连续的语法层来展示如何从一个非常简单的语言构建一种丰富的语言，其中每一层都可以转换为前一层。因此，区分必须终止的翻译和不需要的评估很重要。我认为递归可以转换为非递归真的很有趣。如果我的解释没有帮助，我很抱歉。
我将尝试以我理解的方式发布我自己的答案。
对于无类型的 lambda 演算，没有实际原因，我们需要 Y 组合器。实际上，我的意思是，如果有人想构建表达式评估器，则可以在不需要组合器的情况下完成它，而只需慢慢扩展定义即可。
但是，出于理论上的原因，我们需要确保当我们定义一个函数时，这个定义有一定的意义，而不是根据它本身来定义的。例如，以下定义没有太多意义：
def something = something
出于这个原因，我们需要看看是否有可能以非自引用的方式重写定义，即是否可以在不引用自身的情况下定义某事物。事实证明，在无类型的 lambda 演算中，我们总是可以通过 Y-combinator 做到这一点。
使用 Y 组合器，我们总是可以构造方程 x=f(x)=f(f(x))=...=f(f(f(f(x)))=... 的解。对于任何 f，
即我们总是可以将自引用定义重写为不包含自身的定义
原因是我们希望遵守 lambda 演算的规则。允许术语的名称表示除立即替换之外的任何含义将意味着在语言中添加递归 let 表达式，这意味着我们需要一个真正更具表现力的系统（不再是 lambda 演算）。
您可以将这些名称视为原始 lambda 术语的语法糖。Y-combinator 正是将递归引入没有内置它的系统的方法。如果您当前正在阅读的书让您感到困惑，您可能需要在 Internet 上搜索一些解释 Y-combinator 的其他资源。