# Reducing Lambda to Normal Form

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.

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.