0

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!

Chris
  • 151

1 Answers1

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.

Ted
  • 33,788
  • So you can just replace z with y and that's how it reduces fully to y? I was under the impression that you need a variable z bound to lambda z to be able to replace it? or can you just replace lambda z even if there's no bound variable z? – Chris Oct 09 '16 at 19:05
  • For example (λz.zy)y -> (λz.zy) [z:=y] -> β yy – Chris Oct 09 '16 at 19:09
  • You are not replacing $z$ with $y$. If you have an expression $(\lambda z.e)f$, the $\beta$ rule says to replace the free occurrences of $z$ in $e$ with $f$. In your case, $z$ does not occur in $e$, so the result is just $e$ again: $(\lambda z.e)f \rightarrow_\beta e$ if $e$ does not contain any free occurrences of $z$. – Ted Oct 10 '16 at 06:41
  • Ah okay, that makes sense. Thanks very much! – Chris Oct 10 '16 at 22:16