Beta Reduction Constraints The definition of $β$ reduction is the following :
$$(λx.M)N \rightarrow_{β} Μ[x∶=N] $$
So basically we stop treating $x$ as a bound variable and we perform substitution of the now free variable $x$ in the $M$ term under the constraint that the free variables of $N$ are still free. I was browsing the Internet for some examples to solve and I came across the following Stack Overflow Question
I mostly care about the first 2 terms of the $λ$ expression which are :
$$λz.(λm.λn.m)(z)$$
When it comes to the evaluation of this expression we start from the $λm$ term and the result according to the answer to the posted question will be :
$$λz.λn.z$$
Before the evaluation $N$ was $(z)$ and $FV(N)={z}$.
However after the evaluation the constraint is broken and now $z$ is bound in the expression  $λz.λn.z$.
Maybe there is some correlation between the parenthesis before the $λm$ and the scope of $λz$.
Any help would be appreciated.
 A: The point is that the $\beta$-rule
$$
(\lambda x.M)N \to_\beta M[x:= N]
$$
can be applied in any context. This means that, in a term $P$, if there is a subterm of the form $(\lambda x.M)N$, you can apply the $\beta$-rule to that subterm, leaving the rest of $P$ unchanged.
In your example, the context is $\lambda z.\langle\,\rangle$, which means that the term $\lambda z.(\lambda m.\lambda n. m)z$ is obtained as the plugging of the subterm $(\lambda m.\lambda n. m)z$ into the hole $\langle\,\rangle$ of the context $\lambda z. \langle\,\rangle$. Often this is denoted by $\lambda z. \langle(\lambda m.\lambda n.m)z\rangle$.
The $\beta$-rule acts inside the hole $\langle\,\rangle$ of the context, and stuff outside the hole is left unchanged.
Therefore, the $\beta$-step is
\begin{align}\tag{1}
\lambda z. (\lambda m.\lambda n.m)z &= \lambda z. \langle(\lambda m. \lambda n.m)z\rangle \\
&\to_\beta \lambda z. \langle(\lambda n. m)[m := z]\rangle = \lambda z. \langle\lambda n.z\rangle = \lambda z. \lambda n.z
\end{align}
The constraint about free variables holds for the subterm where you apply the $\beta$-rule (in this case, $(\lambda m.\lambda n.m)z$ where $z$ is free and it is still free after the $\beta$-step), but not for the whole term that is evaluated (in this case $\lambda z. (\lambda m .\lambda n.m)z$). Plugging a term into a context can bind some free variables (in this case, it happens for $z$), but this is irrelevant for the $\beta$-rule, since the $\beta$-rule is carried out inside the hole. Note that in $(1)$, if you consider the whole terms, the variable $z$ is bound before and after the $\beta$-step.
