0
$\begingroup$

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.

$\endgroup$
0
$\begingroup$

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?

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.