I'm just getting started with STLC (Simply Typed Lambda Calculus) and I'm trying to understand an evaluation rule I've been given in some lecture notes by my professor. What it says is the following:
(λx. x(λx. x)) (u r) evaluates to (u r) (λx. x)
I don't really get this at all. Can someone point out which step I'm misunderstanding in my evaluation;
(λx. x(λx. x)) (u r) // Start state, not evaluated (λx. λz. z) (u r) // Replacing occurences of x in first lambda function with the // second lambda function, and then renaming the input variable x // in the second lambda function (this is allowed, right?) r // x gets replaced by u (no occurences) and z gets replaced by r // - resulting in the final result r.