сокращения Lambda доказать S K = K I

Question

Привет У меня возникли проблемы, подтверждающие эти комбинаторы S K = K I

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

что я пробовал до сих пор сокращение 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 ZZ.) и λy. λx.x Может кто-нибудь, пожалуйста, объясните мне, что я сделал не так? Спасибо.

Answer 1

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