3

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

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

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

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

问候。

4

3 回答 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 回答