Reducing Lambda to Normal Form

Question

I'm having issues trying to reduce (λx. (λy. y x) (λz. x z)) (λy. y y) to its normal form. I get to (λy. y (λy. y y) (λz. (λy. y y) z) then get kind of lost. I don't know where to go from here.

Answer 1

Let's write $\omega \equiv \lambda y. y \: y$.

So your term is $(\lambda x. (\lambda y . y \: x)(\lambda z . x \: z))\: \omega$.

We know that leftmost reduction will always find the $\beta$-normal form, so let's do that. The reduction sequence we get is:

\begin{align*} (\lambda x. (\lambda y . y \: x)(\lambda z . x \: z))\: \omega &\to_{\beta} (\lambda y . y \: \omega)(\lambda z . \omega \: z)\\ &\to_{\beta} (\lambda z . \omega \: z) \: \omega \\ &\to_{\beta} \omega \: \omega \end{align*}

Now what happens when we reduce $\omega \: \omega \equiv (\lambda y. y \: y) \: \omega$?

There's only one reduction we can make, and it's $(\lambda y. y \: y) \: \omega \to_{\beta} (y \: y)[\omega/y] \equiv \omega \: \omega$.

So the term $\omega \: \omega$ only reduces to itself! Now it's clear that we can keep repeating this reduction forever, so our original term has no normal form.

The term $\omega \: \omega$ is known as $\boldsymbol{\Omega}$, and it's one of the simplest terms with no $\beta$-normal form.