Combinatory logic - Evaluation exercise (abstraction and weak reduction)

165 Views Asked by At

I am going through the book "Lambda-Calculus and Combinators: An Introduction".

I am trying to solve the following exercise: evaluation of $[x,y,z].xzy$

The result should be, according to solutions: $\mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{S})(\mathbf{S}(\mathbf{K}\mathbf{K})\mathbf{S}))(\mathbf{K}\mathbf{K})$

My attempt is the following:

$[x,y,z].xzy \\ \equiv [x].([y].([z].xzy)) \\ \equiv [x].([y].\mathbf{S} x(\mathbf{K} y))\\ \equiv [x].(\mathbf{S}([y].\mathbf{S} x)([y].\mathbf{K} y)) \\ \equiv [x].(\mathbf{S}(\mathbf{K}\mathbf{S}x)\mathbf{K})\\ \equiv \mathbf{S}([x].\mathbf{S}(\mathbf{K}\mathbf{S}x))([x].\mathbf{K}) \\ \equiv \mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{S})([x].\mathbf{K}\mathbf{S}x))(\mathbf{K}\mathbf{K}) \\ \equiv \mathbf{S}(\mathbf{S}(\mathbf{K}\mathbf{S})(\mathbf{K}\mathbf{S}))(\mathbf{K}\mathbf{K}) $

but it does not match the solution.