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

  • $\begingroup$ Maybe relevant: math.stackexchange.com/questions/118298/…. $\endgroup$ – Martín-Blas Pérez Pinilla Mar 12 at 9:40
  • $\begingroup$ 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. $\endgroup$ – Arthur Mar 12 at 9:45
  • $\begingroup$ You're correct: the first bounded $x$ is not binding the inner $x$'s. $\endgroup$ – 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))$.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.