уменьшение лямбда-исчисления с уменьшением α

Question

Я пытаюсь завершить сокращение лямбда-исчисления, но не могу продолжить после точки.Я должен уменьшить значение «два два», где «два = λfx.f (fx)»

Я начинаю писать следующее:

(λ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