Лямбда-сокращения доказывают S K = K I

Question

Здравствуйте, у меня возникли проблемы с доказательством этих комбинаторов S K = K I

Шаги с квадратными скобками [] просто показывают вам шаг, который я делаю. Например, [λxy.x / x] в λyz.x z(y z) означает, что я собираюсь заменить (λxy.x) на каждый x в выражении λyz.x z(y z)

то, что я пробовал до сих пор, это уменьшение SK, и я получил это:

S K
(λxyz.x z(y z)) (λxy.x)
[λxy.x / x] in λyz.x z(y z) 
(λyz. (λxy.x) z(y z))
[z/x] in λy.x
(λyz. (λy.z) (y z))
[y/y] in λy.z
(λyz. z z)

а потом уменьшив KI и я получил это:

K I
(λxy.x) (λx.x)
[λx.x / x] in λy.x
λy. λx.x

хотя два ответа не кажутся мне равными (λyz. z z) и λy. Может ли кто-нибудь объяснить мне, что я сделал не так? Спасибо.

Answer 1

(λy.z) (y z) сводится к просто zне z z, так (λyz. (λy.z) (y z)) является λyz. z, который так же, как λy. λx. x,