Lambda演算归约

Question

全,

下面是我发现很难简化的lambda表达式，即我不能理解如何处理这个问题。

(λmλnλaλb.M (n A b) b) (λf x.x) (λf x. f x)

这是我尝试过的，但我被卡住了：

将上面的表达式视为：(λm.E) M等于

E= (λnλaλb. m (n A b) b)

M= (λf x. x)(λf x. f x)

=> (λnλaλb. (λf x. x) (λf x. f x) (n A b) b)

将上面的表达式视为(λn.e)M等于

E= (λaλb. (λf x. x) (λf x. f x) (n A b) b)

M= ?？

。。我迷路了！

谁能帮我理解一下，对于任何lambda演算表达式，执行归约的步骤应该是什么？

Answer 1

您可以按照以下步骤减少lambda表达式：

1. 将表达式完全括起来以避免错误，并使函数应用程序发生的位置更明显。
2. 查找函数应用程序，即查找模式(λX. e1) e2的匹配项，其中X可以是任何有效标识符，e1和e2可以是函数的任何有效标识符，方法是将(λx. e1) e2替换为e1'，其中e1'是用e2.
3. Repeat 2和3替换e1中每个自由出现的x直到该模式不再出现的结果。注意，这可能会导致非规范化表达式的无限循环，因此您应该在1000次左右的迭代后停止;-)

因此，对于您的示例，我们从表达式开始

((λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))) (λf. (λx. (f x)))

在这里，子表达式(λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x))适合我们使用X = m、e1 = (λn. (λa. (λb. (m ((n a) b)) b))))和e2 = (λf. (λx. x))的模式。因此，在替换之后，我们得到了(λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b)))，这使得我们的整个表达式：

(λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))) (λf. (λx. (f x)))

现在，我们可以使用X = n、e1 = (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))和e2 = (λf. (λx. (f x)))将该模式应用于整个表达式。因此，在替换之后，我们得到：

(λa. (λb. ((λf. (λx. x)) (((λf. (λx. (f x))) a) b)) b))

现在，((λf. (λx. (f x))) a)符合我们的模式，并成为(λx. (a x))，这导致：

(λa. (λb. ((λf. (λx. x)) ((λx. (a x)) b)) b))

这一次，我们可以将该模式应用于((λx. (a x)) b)，它简化为(a b)，从而导致：

(λa. (λb. ((λf. (λx. x)) (a b)) b))

现在将该模式应用于((λf. (λx. x)) (a b))，它简化为(λx. x)和get：

(λa. (λb. b))

现在我们完成了。

Answer 2

你的错误之处在于，在第一步，你不能

M = (λf x. x)(λ f x. f x)   

因为原始表达式不包括该应用程序表达式。为了清楚地说明这一点，您可以按照应用程序是左关联的规则将其放入隐式括号中(使用and表示新的括号，并在其中添加一些缺少的"."s)：

[ (λm . λn . λa . λb . m (n a b) b) (λ f x. x) ] (λ f x. f x)

在这里，找到一个形式为(λv.E) M的表达式，并在E中用M替换v来减少它。注意，它实际上是函数对M的应用:如果您有像N (λv.E) M这样的东西，它就不是，因为N被应用于函数，而M作为两个参数。

如果你仍然卡住了，试着把每个lambda的括号也放进去--基本上就是在每个".“之后加上一个新的"(”，和一个匹配的")“，它尽可能地向右移动，同时仍然匹配新的"(”。作为一个例子，我在这里做了一个例子(使用和使它们脱颖而出)：

( (λm . λn . λa . [λb . m (n a b) b]) (λ f x. x) ) (λ f x. f x)