Lambda calculus -reducing expression

Question

I have following expression to reduce:

$(λmnfx.mf(nfx) λfx.fx λzy.zzy)$

After some substitutions i get the result:

$(λfx. f(f(f x)))$

Is it correct answer? If not, please tell me what is correct one so i could try to get into it. Thanks in advance.

Answer 1

In order to keep the variables straight, I'm going to do an alpha conversion to the first abstraction, replacing f with a and x with b which leaves me with...

\mnab.ma(nab) \fx.fx \zy.zzy

Note the third abstraction contains no parenthesis and is therefore equivalent to \zy.(zz)y but is not equivalent to \zy.z(zy)

The second abstraction will replace the m variable and the third abstraction will replace the n variable. The a and b variables are going to be part of the solution abstraction.

\ab.(\fx.fx)a((\zy.zzy)ab)

Now I resolve the \fx abstraction, replacing f with a and x with ((\zy.zzy)ab).

\ab.a((\zy.zzy)ab)

Finally, I resolve \zy, replacing z with a and y with b.

\ab.a(aab)

This is not the same as the answer you have provided because the parenthetical portion is equivalent to "((aa)b)", not "(a(ab))" which would make it a Church Numeral. The variables in Church Numeral abstractions are right associative. Are you certain the problem is stated correctly?