Lambda reductions prove S K = K I

379 views Asked by At

Hello I am having trouble proving these combinators S K = K I

The steps with the brackets [] are just telling you the step i am doing. For example [λxy.x / x] in λyz.x z(y z) means I am about to substitute (λxy.x) for every x in the expression λyz.x z(y z)

what I have tried so far is reducing S K and I got this:

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)

and then reducing K I and I got this:

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

though the two answers do not seem to be equal to me (λyz. z z) and λy. λx.x can someone please explain to me what I did wrong? Thank you.

1

There are 1 answers

3
jwodder On BEST ANSWER

(λy.z) (y z) reduces to just z, not z z, so (λyz. (λy.z) (y z)) is λyz. z, which is the same as λy. λx. x.