Simplyfing $(\lambda y. z)((\lambda x. x x)(\lambda x. x x))$

Question

I need to simplify this expression.

$(\lambda y. z)((\lambda x. x x)(\lambda x. x x))$

However, what's interesting to me are two things:

1. Should I start simplifying $((\lambda x. x x)(\lambda x. x x))$ first because they fall under the same pair of brackets? This sort of reminds me of $2+(3+4)$ but of course we know that addition is associative

2. What do I do with $((\lambda x. x x)(\lambda x. x x))$? This is an irreducible form using alpha, beta and eta reductions.

What I tried doing is first simplifying $(\lambda x.xx)(\lambda x.xx)$, but I just get the same expression all over again. This is because this is irreducible using alpha, beta and eta rules. Right now, I am not sure if I should already call this simplified as much as possible, or is there something else I am not aware of.

Answer 1

You are right. The expression $(\lambda x.xx)(\lambda x.xx)$ can't be reduced any more. It is a famous example of a lambda expression that doesn't have a normal form.

In the untyped lambda calculus we can do beta reduction on any redex. By Church-Rosser theorem order of beta reductions is not important.

Therefore, it is better to do a beta reduction of outer redex $(\lambda y.z) M \rightarrow_\beta z$. Result is, of course, in a normal form.

But as you can see, you would get the same result even if you did $n$ reductions of inner redex and then do a reduction of outer redex. This is a demonstration of Church-Rosser theorem.

Answer 2

1. As answered by @Nikola Ubavić, the Church-Rosser theorem allows you to β-reduce the redexes in any order, so you should indeed reduce the outer redex if you want the reduction to terminate.
2. However,

   — What do I do with $((λx.xx)(λx.xx))$? This is an irreducible form using alpha, beta and eta reductions.

   — You are right. The expression $(λx.xx)(λx.xx)$ can't be reduced any more.

let me stress that $(\lambda x.xx)(\lambda x.xx)$ is not irreducible: as you observed, it can be reduced — to itself. It's not just a matter of talking, there are actual (and valid) infinite reductions starting from your term, and what you look for is not “the” reduction but “a good” reduction strategy.

---

(SE didn't want me to post this as comment, so I wrote an answer...)