Application of lambda function in Simply Typed Lambda Calculus 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.
The term

(λx. x(λx. x)) (u r)


parses as

(λx. M) N
where M=(x (λx. x)) and N=(u r)


so, we can perform a $\beta$ step and obtain

M{N/x}
= (x (λx. x)){(u r) / x}
= (x{(u r) / x}   (λx. x){(u r) / x})
= ((u r)   (λx. x){(u r) / x})
= ((u r)   (λx. x))


The last term is also usually written as (u r) (λx. x) or even u r (λx. x).

A tricky part of this step is the substitution (λx. x){(u r) / x} = (λx. x). This derives from the general rule stating that for any terms A,B:

(λx. A){B / x} = (λx. A)


Indeed, the intuition here is that a substitution {B / x} only substitutes the free occurrences of x, and there are no free occurrences of x in (λx. A). This is coherent with the fact that the bound variable x in (λx. A) could be $\alpha$-converted to any fresh variable name y, obtaining (λy. A{y / x}), where x is no longer present at all (free or bound).



By comparison, this step is wrong

(λx. x(λx. x)) (u r) --&gt; (λx. λz. z) (u r) 


First, when you apply a $\beta$ step, the $\lambda x$ disappears. So, we can not have both $\lambda x$ and $\lambda z$ in the residual term. If we change the term, modifying the parentheses, we get

((λx. x)(λx. x)) (u r) --&gt; (λz. z) (u r) 


but the starting term is completely different from the original one, where
(λx. x(λx. x)) (u r) is read as ((λx. (x(λx. x))) (u r)) instead.