lambda calculus beta reduction and normalisation

Question

I have a question that asks me whether the following expression is weakly and/or stronly beta normalised.

(λz.y)((λx.xx)(λx.xx))
 ____________________

Apparently this expression beta reduces to y. How so? and how does that make it weakly normalising compared to strongly normalising?

Note: I understand that the following is not strongly normalising because it never terminates.

(λz.y)((λx.xx)(λx.xx))
        ____________

Thanks for the help!

Answer 1

Check your definitions of weakly normalizing vs. strongly normalizing. They differ in the order of normalization.

If you normalize the outside first, then you get $$(\lambda z.y)\,(\ldots) \rightarrow y$$ where the stuff in "$\ldots$" doesn't matter because there are no z's in y in which to substitute "$\ldots$". (Why? Recall that the $\beta$ reduction rule says that starting from $(\lambda z.(***))\,(\ldots)$, you replace all occurrences of $z$ in "***" with "$\ldots$".)

But if you normalize the inside first, then (as you point out), you would start by processing the $((\lambda x.xx)(\lambda x.xx))$ first, which results in an infinite loop.