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.


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.