lambda-calculus - lambda 演算中的 Beta 缩减 : Order of evaluation important?

Question

给定以下 lambda 表达式，其中 \ 类似于 lambda:

(\kf.f(\c.co)km)(\x.dox)(\le.le)

如果我将(\c.co)k转换成ko是不是错了？我这样做了，显然，这是错误的。正确的做法是首先评估外部函数，这意味着 (\f.f(\c.co)(\x.dox)m)(\le.le) 应该是所需的解决方案。

这是真的吗，因为我在我们的讲义中找不到任何可以表明这一点的规则？如果是，为什么我不能先评估内部功能？尽管如此，我已经这样做了，而且我的解决方案是正确的。

问候。

Answer 1

我问过我的TA，他说application是left associative，意思是

(\kf.f(\c.co)km)(\x.dox)(\le.le)

相当于

( [\kf.( [ f(\c.co) ]k )m ][\x.dox] )[ \le.le ]

这就解释了为什么 k 不能应用于 (\c.co)。:/

方括号/括号仅用于使其更具可读性。

问候。