I have the following lambda calculus:
( x ( λyz.xz ) ( λxy.zyx )) (( λyx.xyz ) ( λy.xz ))
which I already reduced:
alpha => ( x ( λyz.xz ) ( λxy.zyx )) (( λyx1.x1yz )) ( λy.xz ))
beta => ( x ( λyz.xz ) ( λxy.zyx )) ( λx1.x1 ( λy.xz ) z )
My question: Why are the following reductions wrong? They seem to simplify the expression to me:
beta1 => ( x ( λyz.xz ) ( λxy.zyx )) ( λx1.x1 ( xz ))
beta2 => ( x ( λy.x ( λxy.zyx ))) ( λx1.x1 ( xz ))
To avoid confusion I would suggest to alpha-rename a bit more.
So it would appear you have x and z in "scope" (they are not bound by any λ in your term), it is a good idea to make sure if you are referring to them or not.
I would rewrite your term like this:
(x (λy1,z1. x z1) (λx2,y2. z y2 x2)) ((λy3,x3. x3 y3 z) (λy4. x z))
I went quite far in renaming (this is unnecessary of course, but like this, we are sure which is which).
This term beta-reduces to
(x (λy1,z1. x z1) (λx2,y2. z y2 x2)) ((λx3. x3 (λy4. x z) z))
And then
(x (λy1,z1. x z1) (λx2,y2. z y2 x2)) ((λx3. x3 (λy4. x z) z))
This is indeed alpha-equivalent to what you wrote.
What you want to do then is apply (λy4. x z) to z.
This is not how you should be reading x3 (λy4. x z) z which could be also written with more parentheses like this (x3 (λy4. x z)) z.
Somehow this term is stuck because its head is a variable.
There isn't much you can do about it because this term is also involved in an application you can't reduce.
Perhaps you could also rewrite (λy1,z1. x z1) into (λy1. x) by eta-reduction.
So you cannot get (x (λyz.xz) (λxy.zyx)) (λx1.x1 (x z)) and for the same reason, you can't beta-reduce it to (x (λy.x (λxy.zyx))) (λx1.x1 (x z)) because you got the parenthesizing wrong.
f x y is read from left to right, you take f and you apply it to x, then you apply the result to y.
I would keep this answer very simple.
To reduce to beta1 or beta2, notice that you have reduce ( λy.xz ) z in "x1 ( λy.xz ) z" like "x1 ( ( λy.xz ) z ) ", so you can reduce., i.e, parenthesize/group last two expressions ( λy.xz ) and z together, which is wrong.
This is not how it should work. While reducing lambda expressions you should maintain left associativity., i.e., always group leftmost expressions together like " ( x1 ( λy.xz ) ) z" instead of "x1 ( ( λy.xz ) z )" [which is wrong].
With left associativity,if there are expressions like E1 E2 E3 E4,
you should group it like ( ( (E1 E2) E3 ) E4 )
Thus, for the beta2, you can not reduce x1 ( λy.xz ) z to "x1 ( xz )". Same logic goes for beta1.
I hope that makes sense to you.
