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