# Lambda Calculus - free vs. bound variables

While I am reducing the following term, I encountered a little Problem:

$$(\lambda w x. w x)(\lambda w x. w x) \rightarrow_\beta (\lambda x.(\lambda w x. w x) x)$$

Now my first question: Why is it possible to reduce further after doing alpha conversion? Isn't the last x bound be the first lambda?

Second Question: In my Lectures notes there is mentioned that $(\lambda y . a )b$ -> a. Why can we do this? Shouldn't the result be b? Because we apply b to all free occurrences of y in a, but there are none so our expression reduces to b.

Iterated abstraction uses abstraction to the right:

\begin{align} LHS &= (\quad \lambda wx.wx \space\space\space)\space(\lambda wx.wx) \\ &= (\lambda w.(\lambda x.wx))\space(\lambda wx.wx) \end{align}

The beta reduction axiom is $(\lambda x. M[x])N = M[x := N]$.

To satisfy your original equation, replace all occurences of $x$ in the beta reduction axiom, with $w$. Then, substitute the following values into the beta reduction axiom: $$M[w] = (\lambda x.wx)$$ $$N = (\lambda wx.wx)$$

The beta reduction axiom with substituted values is $$(\lambda w.(\lambda x .wx))(\lambda wx.wx) = M[w:=(\lambda wx.wx)]$$

where $M[w:=(\lambda wx.wx)]$ means "substitute all occurences of $w$ in $M$ with $(\lambda wx.wx)$". So we get:

$$(\lambda w.(\lambda x .wx))(\lambda wx.wx) = (\lambda x.(\lambda wx.wx)x)$$

as expected.

For the $(\lambda y.a)b \rightarrow a$ equation, $y$ is a bound variable, while $a$ is a free variable. We apply $b$ to all occurences of $y$, but there are none so our expression doesn't change (no $y$ is converted to $b$). The result is still $a$, unchanged.

Source, really well written and accessible if you give it enough time.