# Scope of the first x in $(\lambda x. (\lambda x. x x) \ (\lambda x. x x))$

I want to reduce this to normal form. I think it's already in normal form, but that one can get the same expression infinitely.

But that necessarily means the first $$x$$ does not bind any of the inner $$x$$ variables? I am struggling to get rules for binding clear when its the same variable

• Maybe relevant: math.stackexchange.com/questions/118298/…. – Martín-Blas Pérez Pinilla Mar 12 at 9:40
• I'm not very well versed in $\lambda$-calculus conventions, but $\lambda x.(\lambda x.xx)$ looks very ambiguous to me. Does the outer $\lambda$ expression take in an $x$ and feed back the function which applies its argument to itself, the function which applies $x$ to the argument, the function which applies the argument to $x$, or the function that applies $x$ to itself? I don't know. – Arthur Mar 12 at 9:45
• You're correct: the first bounded $x$ is not binding the inner $x$'s. – Berci Mar 12 at 10:02

The term is not in normal form, because it contains a redex: $$(\lambda x.xx)(\lambda x.xx)$$. However, beta-reducing this redex yields just the same term again: $$(\lambda x. (\lambda x.xx)(\lambda x.xx)) \to_\beta (\lambda x. (\lambda x.xx)(\lambda x.xx))$$ Since this is the only beta-reduction possible, $$(\lambda x. (\lambda x.xx)(\lambda x.xx))$$ is not normalizable (= does not have a $$\beta$$ normal form).
You are partially right in your assumption that the outermost abstraction $$\lambda x$$ does, in a way, not affect the variables in the inner subterms: Just like in predicate logic with quantifiers binding variables, an outermost binding of variables will get "overwritten" by a new abstraction in a subterm.
This is due to the definition of substitution and free and bound variables: $$\lambda x.M$$ binds any free occurrence of $$x$$ in $$M$$. But since every occurrence $$x$$ is already bound by another abstraction in $$M$$, there are no occurrences of variables that are bound by the outermost abstraction. To find the free variables in $$(\lambda x. (\lambda x.xx)(\lambda x.xx))$$, you would recursively go down the structure of the lambda term and look for the free occurences of $$x$$ in each of the subterms $$(\lambda x.xx)$$ and $$(\lambda x.xx)$$. Since all occurrences $$x$$ belong to a subterm of the inner $$\lambda x.M$$ respectively and are therefore already bound by other abstractions, there are no free occurrences of $$x$$ in any of the subterms and thus none in the term as a whole, so the outer $$\lambda x$$ does not effectively bind anything.
If you were to apply the term $$(\lambda x. (\lambda x.xx)(\lambda x.xx))$$ to some term $$P$$ and performed beta reduction, the operational semantics would tell you to substitute every free occurrence of $$x$$ by $$P$$. The recursive definition of substitution first passes down the substitution $$[P/x]$$ to each of the subterms in the application $$(\lambda x.xx)(\lambda x.xx)$$, but then for each of the two subterms $$(\lambda x.xx)$$ would state that nothing happens, because there are no free occurrences of $$x$$ in these terms. So the inner abstractions take operational precedence over the outermost abstraction due to the way free vs. bound variables and substitution are defined; they are "new" abstractions that are independent of the first $$\lambda x$$.
This also means that the $$x$$'s in the two subterms of the form $$(\lambda x.xx)$$ are independent: The $$x$$'s belong to different bindings and therefore behave as different varialbes, in the same way that the outermost $$\lambda x$$ is a different abstraction from the ones in the respective subterms.
Nevertheless, I sand only "partially right" because the outermost abstraction techincally does have scope over the entire subterm $$((\lambda x.xx)(\lambda x.xx))$$. If there were free occurences of $$x$$ in any of the subterms, then these variables would be bound. It just so happens that all of none variables that are in the scope of the outer $$\lambda x$$ are free, so the abstraction is vacuous and doesn't have an actual effect. Still, the scope of $$\lambda x$$ is the entire suberm $$((\lambda x.xx)(\lambda x.xx))$$.