1
$\begingroup$

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.

$\endgroup$
1
$\begingroup$

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.

$\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.