用α归约对lambda演算进行归约

Question

我正在尝试完成lambda演算的简化，但是在一个点之后我不能继续。我必须减少值"two two“，其中"two =λfx.f (f x)”

我开始写以下内容：

(λfx.f (f x) two) = λx.two (two x)
                  = λa.two(λfx.f(f x) a)
                  = two(λx.a(a x))
                  = (λfx.f (f x) (λx.a(a x)))

在这一步之后，我开始变得非常困惑，我不知道如何继续下去。我是否必须将第二个λ项应用于第一个λ项的f变量？我试过了，但是没有结果。

Answer 1

让2 := λfx.f (f x)注意

 2 a    = λx.a (a x)     (i)
(2 a) b = a (a b)        (ii)

因此

2 2 
= λx.2 (2 x)             by (i), a = 2
= λxy.(2 x) ((2 x) y)    by (i), a = (2 x)
= λxy.(2 x) (x (x y))    by (ii)
= λxy.x (x (x (x y)))    by (ii)
= λfx.f (f (f (f x)))
=: 4