用 α 减少的 lambda 演算减少

Question

我正在尝试完成 lambda 演算减少，但在某个点之后我无法继续。我必须减少“二二”的值，其中“二 = λ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)))

在这一步之后，我开始变得非常困惑，我不知道如何继续。我是否必须将第二个 lambda 项应用于第一个 lambda 项的 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