How to reduce a term to normal form

Question

I need to reduce (λx.λy.xy)y(xλz.zz) and I have done so and reached y(xλz.zz) as a normal form, however, I checked interpreters online https://lambdacalc.io/ and https://lambster.dev/ and they reduce to (xy), and I don't understand the steps they take to reach that normal form.

This is my working out:

$((\lambda x.\lambda y. xy)[a/y])y)(x \lambda z.zz)$
$((\lambda x.\lambda a. xa)y)(x \lambda z.zz)$
$(\lambda a. ya)(x \lambda z.zz)$
$y(x \lambda z.zz)$

Any help would be so appreciated, thanks

Answer 1

Your reductions are correct. The way you pass this into the online calculators is not. You need a space between variables.

If you type (λx.λy.xy)y(xλz.zz), 'xy' is interpreted as its own variable and not two variables 'x' and 'y'. In that case, the term indeed reduces to xy.

Try using (λx.λy.x y)y(x λz.z z) as input and it should work.

• pleaseandthankyou: thanks! that's so so helpful, but I was wondering, even if I interpret 'xy' as its own variable, I do not end up reducing to 'xy'. I think I end up with (xλz.zz), would you be able to explain the reduction steps to end in xy? Thanks so much
• Vanessa: hmm how do you end up with (xλz.zz)? interpreting 'xy' as its own variable, (λx.λy.xy)y(xλz.zz) will take two arguments, throw both of them away, and return xy. First alpha-rename like you did (λx.λa.xy)y(xλz.zz). Now replace every occurrence of 'x' with 'y', but there are none so you get (λa.xy)(xλz.zz). Now replace every occurrence of 'a' with (xλz.zz). Again, there are none so you get xy. Remember the term 'xy' is completely different from having the term 'x' next to the term 'y'.