给定以下 lambda 表达式，其中\类似于lambda：
(\kf.f(\c.co)km)(\x.dox)(\le.le)
(\c.co)k如果我转换成是错的ko吗？我这样做了，显然，这是错误的。正确的方法是首先评估外部函数，这意味着(\f.f(\c.co)(\x.dox)m)(\le.le)将是所需的解决方案。
这是真的吗，因为我在我们的讲义中找不到任何可以表明这一点的规则？如果是，为什么我不能先评估内部功能？我已经这样做了，但是我的解决方案是正确的。
问候。
问问题
1836 次
3 回答
2
我问了我的TA，他说应用程序是左关联的，意思是
(\kf.f(\c.co)km)(\x.dox)(\le.le)
相当于
( [\kf.( [ f(\c.co) ]k )m ][\x.dox] )[ \le.le ]
这就解释了为什么k不能应用于(\c.co).:/
括号/括号仅用于使其更具可读性。
问候。
于 2013-01-28T21:18:03.067 回答
2
因此，（无类型的）lambda 演算中的 beta-reduction 就是我们所说的融合重写规则。这意味着如果您可以A使用Bbeta 缩减重写，也A可以C使用 beta-reduction 重写，那么您可以找到一些D这样的B重写D 和 C重写D- 实际上会有一些共同的后代。用于 lambda 演算的定理通常称为Church-Rosser 定理。整体属性有时称为菱形属性，因为该图类似于菱形（两条路径分支出来，但最终又重新组合在一起）。这也意味着无论您如何选择应用 beta 缩减，“终止”lambda 表达式的最终结果都是相同的。
但是，并非所有 lambda 项都有一个最终结果。这意味着无类型演算不是我们所说的规范化。有很多 lambda 项会在 beta 归约下永远扩展（永远不会达到不可归约或正常形式）。在这些情况下，有一些系统来安排你的重写是很有用的，因为它可以确保对两个相同的程序进行相同的程序评估。
当然，您需要确保遵守 lambda 的绑定规则，因此不要尝试将术语应用于错误的 lambda 变量。
于 2013-01-29T16:16:36.517 回答
2
这显然是在问题得到满意回答之后的方式。但是，我不得不对 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))没有首先应用：它 ( ) 不是 beta redex，它的形式是：((\kf.body)e2)e3。内部表达式 (\kf.body)e2) 是第一个可以减少的有效 beta redex。这样做会导致提供的答案。(e3)((e4)(e2))e3
于 2017-02-11T16:45:18.837 回答