Lambda微积分减少

Question

所有,

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

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

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

将上述表达式考虑为:(λm.E)M等于
E = (λnλaλb.m (nab)b)
M =(λfx.x )(λfx.fx)

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

考虑到上述表达式为(λn.E)M等于
E =(λaλb.(λfx.x)(λfx.fx)(nab)b)
M = ??

..而我迷路了!!

任何人都可以帮助我理解,对于任何lambda演算表达式,执行还原的步骤应该是什么？

Answer 1

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

1. 完全括起表达式以避免错误,并使函数应用程序发生的地方更加明显.
2. 查找函数应用程序,即查找模式的出现,(?X. e1) e2其中X可以是任何有效的标识符,e1并且e2可以是任何有效的表达式.
3. 通过替换应用功能(?x. e1) e2与e1'其中e1'是替换的每个自由发生的结果x在e1与e2.
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))

现在我们完成了.