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.
1 Answer 1
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.