我必须将以下 lambda 表达式简化为 WHNF，但我不太确定该怎么做：
(λx y. x 3) (+ 4) (+ 6 7)
那么，我该怎么做呢？按名称减少呼叫？
(λz x. (λx. x) z) xWHNF 中有这个表达式（其他示例）吗？
问问题
680 次
1 回答
6
WHNF（弱头范式）意味着你要么有一个值（例如一个整数），要么一个表达式属于(λx . e(x))可能e(x)包含对 的引用的表达式x，所以基本上你有结果是一个函数。
在您的情况下，您拥有的表达式包含一些需要减少的应用程序：
(λx . λy. x 3) (+ 4) (+ 6 7) = (λy . (+ 4) 3) (+ 6 7)
= (+ 4) 3
= 7
请注意，在这种情况下y不会出现在函数体中，因此+ 6 7在还原期间“消失”。
不，不在(λz x. (λx. x) z) xWHNF中，因为“顶级运算符”仍然是一个应用程序。请注意，这种情况下的减少有点棘手，因为您在外部有一个自由变量并且也绑定了。但是，我们可以先进行一些重命名：然后执行归约：现在在 WHNF 中。请注意，我们不会减少应用程序，因为它位于.xλx(λz k. (λt. t) z) x(λk. (λt. t) x)(λt. t) xλ
要检查表达式是否在 WHNF 中，您必须将其视为句法树。让我们考虑上面的两个示例，并用 明确表示应用程序$。请记住，该应用程序f x y等效于(f x) y.
在第一种情况下，表达式是：
|
+-------------$-----------+
| |
+---- $ ---- +---(+)---+
| | | |
λx λt 6 7
| |
λy +-(+)-+
| | |
+---$---+ t 4
| |
x 3
如您所见，树的根是 a $，因此我们必须执行应用程序。为了做到这一点，我们必须首先减少左侧，这也是 a$所以必须首先减少它，获得：
|
+-------------$-----------+
| |
| +---(+)---+
| | |
| 6 7
|
λy
|
+---$---+
| |
λt 3
|
+-(+)-+
| |
t 4
现在在左边我们有一个λ所以我们可以减少最外面的应用程序$：
|
+---$---+
| |
λt 3
|
+-(+)-+
| |
t 4
现在根仍然是 a$所以我们也必须减少它：
|
+-(+)-+
| |
3 4
根是 a +，所以我们再次归约得到：
|
7
现在我们完成了。
在第二种情况下，我们有(λz . λk. ((λt. t) z)) x变成树的表达式：
|
+-------$-----------------+
| |
λz x
|
λk
|
+----$----+
| |
λt z
|
t
再次根是 a$所以我们必须减少它：
λk
|
+----$----+
| |
λt x
|
t
现在我们有一棵树，它的根是λ，这意味着表达式在 WHNF 中，所以我们停止。
于 2016-06-20T10:30:59.757 回答