# 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.

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.

• From what I understand it is all about the context that the beta reduction takes place and we demand that the constraints hold inside that context. However how can one determine what the context is? Jan 25 '21 at 20:29
• @RookieCookie - Your understanding is correct! Once you identified the subterm of the form $(\lambda x.M)N$ that you want to fire by the $\beta$-rule, the context is automatically identified too, it is all the rest of the term. Jan 25 '21 at 20:31
• This might be a silly question but by looking at the definition I see that it makes use of parentheses and could this be used as a rule of thumb for context? Like in $(λx.λy.xy)(z)$ context is $λx.λy.xy$ while in $λx.(λy.xy)(z)$ context is $(λy.xy)$ Jan 25 '21 at 20:39
• @RookieCookie - I'm not sure to understand. In the term $(λx.λy.xy)(z)$, the context is nothing, i.e. the hole $\langle \, \rangle$, because the subterm where you apply the $\beta$-rule is the whole term. In the term $λx.(λy.xy)(z)$, the context is $\lambda x.\langle \,\rangle$ because the subterm where you apply the $\beta$-rule is $(λy.xy)(z)$. The context is what is outside the subterm fired by the $\beta$-rule. Jan 25 '21 at 20:55
• To rephrase how would one know where to apply beta - reduction? In my first example $(λx.λy.xy)(z)$ we would care about the constraints holding in the context of the whole term while in $λx.(λy.xy)(z)$ we would care about the constraints holding in the context of the subterm $(λy.xy)$ Jan 25 '21 at 21:12