给定以下 lambda 表达式，其中 \ 类似于 lambda：
(\kf.f(\c.co)km)(\x.dox)(\le.le)
如果我将(\c.co)k 转换为ko 会出错吗？我这样做了，显然，这是错误的。正确的方法是首先评估外部函数，这意味着 (\f.f(\c.co)(\x.dox)m)(\le.le) 将是所需的解决方案。
这是真的吗，因为我在我们的讲义中找不到任何可以表明这一点的规则？如果是，为什么我不能先评估内部功能？我已经这样做了，但我的解决方案是正确的。
问候。
【问题讨论】：
标签： lambda-calculus
我问了我的TA，他说应用是左关联的，意思是
(\kf.f(\c.co)km)(\x.dox)(\le.le)
等价于
( [\kf.( [ f(\c.co) ]k )m ][\x.dox] )[ \le.le ]
这就解释了为什么k 不能应用于(\c.co)。：/
括号/括号仅用于使其更具可读性。
问候。
【讨论】：
因此，（无类型的）lambda 演算中的 beta-reduction 就是我们所说的 confluent 重写规则。这意味着如果您可以通过 beta 缩减将A 重写为B，并且还可以通过 beta-reduction 将A 重写为C，那么您可以找到一些D，这样B 会重写为D 和 C 重写为 D - 实际上会有一些共同的后代。用于 lambda 演算的定理通常称为Church-Rosser theorem。整体属性有时称为菱形属性，因为该图类似于菱形（两条路径分支出来，但最终又重新组合在一起）。这也意味着，无论您如何选择应用 beta-reduction，“终止”lambda 表达式的最终结果都是相同的。
但是，并非所有 lambda 项都有一个最终结果。这意味着无类型演算不是我们所说的规范化。有很多 lambda 项会在 beta-reduction 下永远扩展（永远不会达到不可约或 正常 形式）。在这些情况下，有一些系统来安排你的重写是很有用的，因为它可以确保对两个相同的程序进行相同的程序评估。
当然，您需要确保遵守 lambda 的绑定规则，因此您不要尝试将术语应用于错误的 lambda 变量。
【讨论】：
这显然是在问题得到满意回答之后的方式。但是，我不得不对 lambda 演算中的“求值顺序”有点挣扎，而这个更详尽的答案主要是为了后代，以防其他人有同样的疑问。 @danyel 的回答非常有帮助，我将以此为基础。
正如 OP 正确指出的那样，没有关于评估顺序的明确规则。然而，应用程序是左关联的规则导致了这样一个规则 - 最外面的应用程序将在内部应用程序之前进行评估。
在表达式中，
(\kf.f(\c.co)km)(\x.dox)(\le.le):让我们先做一些简化（使用第一个原则，每个术语 e 要么是变量 x，要么是抽象 \x.y，要么是应用程序 e1e2）：
\c.co = e1, \x.dox = e2,\le.le = e3。这导致原始表达式转换为：
(\kf.f(e1)km)(e2)(e3)。让我们考虑上面表达式中最左边的项：
(\kf.(f(e1)km)) = e4并仔细查看抽象的主体：
- (fe1)km，或(f(\c.co))km
beta redex（可简化表达式）是(\x.e1)e2 形式的表达式。上面的表达式看起来不像，也不是 beta redex（因为基于可用信息， f 不是抽象）。这就是为什么不能减少它以及为什么将\c.co 应用于k 是错误的。
所以e4 没有减少并保持原样，这导致：
((e4)(e2))(e3)。((e4)(e2)) 是第一个 beta redex，实际上e2 替换了k，正如所指出的。
还有一点，((e4)(e2)) 不是首先应用于(e3)，原因相同：它 (((e4)(e2))e3) 不是 beta redex，它的形式是：
((\kf.body)e2)e3.内部表达式 (\kf.body)e2) 是第一个可以减少的有效 beta redex。这样做会导致提供的答案。
【讨论】：