Lambda微积分减少 [英] Lambda Calculus reduction

问题描述

全部

下面是我很难减少的lambda表达式，即我无法理解该问题的解决方法.

Below is the lambda expression which I am finding difficult to reduce i.e. I am not able to understand how to go about this problem.

(λ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) (λ f x. f x)

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

This is what I tried, but I am stuck:

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

Considering the above expression as : (λm.E) M equates to
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 λ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 = ??

Considering the above expression as (λn. E)M equates to
E = (λa λb. (λ f x. x) (λ f x. f x) (n a b) b)
M = ??

..我迷路了！！

任何人都可以帮助我理解，对于任何lambda演算表达式，执行约简的步骤应该是什么?

Can anyone please help me understand that, for ANY lambda calculus expression, what should be the steps to perform reduction?

推荐答案

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

You can follow the following steps to reduce lambda expressions:

1. 在表达式中加上括号，以免出现错误，并使在函数应用发生的地方更明显.
2. 查找功能应用程序，即找到模式(λX. e1) e2的出现，其中X可以是任何有效的标识符，而e1和e2可以是任何有效的表达式.
3. 通过用e1'替换(λx. e1) e2来应用该功能，其中e1'是用e2替换e1中每个x的自由出现的结果.
4. 重复2和3，直到不再出现图案.请注意，这可能会导致非规范化表达式的无限循环，因此您应该在1000次迭代后停止;-)

1. Fully parenthesize the expression to avoid mistakes and make it more obvious where function application takes place.
2. Find a function application, i.e. find an occurrence of the pattern (λX. e1) e2 where X can be any valid identifier and e1 and e2 can be any valid expressions.
3. Apply the function by replacing (λx. e1) e2 with e1' where e1' is the result of replacing each free occurrence of x in e1 with e2.
4. Repeat 2 and 3 until the pattern no longer occurs. Note that this can lead to an infinite loop for non-normalizing expressions, so you should stop after 1000 iterations or so ;-)

因此，在您的示例中，我们从表达式开始

So for your example we start with the expression

((λ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)))，它使我们的整个表达式变为

Here the subexpression (λm. (λn. (λa. (λb. (m ((n a) b)) b)))) (λf. (λx. x)) fits our pattern with X = m, e1 = (λn. (λa. (λb. (m ((n a) b)) b)))) and e2 = (λf. (λx. x)). So after substitution we get (λn. (λa. (λb. ((λf. (λx. x)) ((n a) b)) b))), which makes our whole expression:

(λ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)))将模式应用于整个表达式.因此，替换后，我们得到:

Now we can apply the pattern to the whole expression with X = n, e1 = (λa. (λb. ((λf. (λx. x)) ((n a) b)) b)) and e2 = (λf. (λx. (f x))). So after substituting we get:

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

现在((λf. (λx. (f x))) a)符合我们的模式，并变为(λx. (a x))，从而导致:

Now ((λf. (λx. (f x))) a) fits our pattern and becomes (λx. (a x)), which leads to:

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

这一次，我们可以将模式应用于((λx. (a x)) b)，该模式将减小为(a b)，从而导致:

This time we can apply the pattern to ((λx. (a x)) b), which reduces to (a b), leading to:

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

现在将模式应用于((λf. (λx. x)) (a b))，该模式将减小为(λx. x)并得到:

Now apply the pattern to ((λf. (λx. x)) (a b)), which reduces to (λx. x) and get:

(λa. (λb. b))

现在我们完成了.

这篇关于Lambda微积分减少的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！