lambda - Lambda 演算减少

Question

全部，

下面是我发现难以减少的 lambda 表达式，即我无法理解如何解决这个问题。

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

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

将上述表达式视为： (λm.E) M 等于
E= (λn λa λb. m (nab) b)
M = (λf x. x)(λ f x. fx)

=> (λn λa λb. (λ f x. x) (λ f x. fx) (nab) b)

将上述表达式视为 (λn. E)M 等于
E = (λa λb. (λ f x. x) (λ f x. fx) (nab) b)
M = ??

..我迷路了！！

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

Answer 1

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

1. 将表达式完全括起来以避免错误并使函数应用发生的位置更加明显。
2. 查找函数应用程序，即查找可以是任何有效标识符并且可以是任何有效表达式的模式(λX. e1) e2的出现。Xe1e2
3. (λx. e1) e2通过替换来应用函数e1'where是将ine1'的每个自由出现替换为 的结果。xe1e2
4. 重复 2 和 3，直到模式不再出现。请注意，这可能会导致非规范化表达式的无限循环，因此您应该在 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)并得到：

(λa. (λb. b))

现在我们完成了。

Answer 2

你错在哪里，在第一步，你不能有

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

因为原始表达式不包括该应用程序表达式。为了清楚起见，您可以按照应用程序是左关联的规则放入隐式括号（使用 [ 和 ] 作为新括号并放入一些缺失的“.”）：

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

从这里，找到形式(λv.E) Msome where inside 的表达式，并通过替换v为Min来减少它E。请注意，它确实是函数对 M 的应用：如果你有类似的东西，则不是 N (λv.E) M，因为那时 N 应用于函数，M 作为两个参数。

如果您仍然卡住，请尝试为每个 lambda 加上括号 - 基本上每个“。”之后都有一个新的“（”，以及一个匹配的“）”，它尽可能向右移动，同时仍然匹配新的“ （“。作为一个例子，我在这里做了一个（使用 [ 和 ] 使它们脱颖而出）：

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

Answer 3

只需用一个东西代替它对应的东西：

(λm λn λa λb . m          (n            a b) b) (λ f x. x) (λ f x. f x)
= ~            ^________                        ~~~~~~~~~~
   (λn λa λb . (λ f x. x) (n            a b) b)            (λ f x. f x)
=    ~                     ^__________                     ~~~~~~~~~~~~
      (λa λb . (λ f x. x) ((λ f x. f x) a b) b)
=                 ~       ~~~~~~~~~~~~~~~~~~
      (λa λb .   (λ x. x)                    b)
=                   ~  ^                     ~
      (λa λb .         b                      )

就这些。