1
$\begingroup$

I encountered an example in lambda calculus:

$$(\lambda x.(\lambda y.(xy))x)(\lambda z.w)$$

Now, can I apply the second parenthesis to $\lambda x$? Then

$$(\lambda x.(\lambda y.(xy))x)(\lambda z.w) \rightarrow^{\beta} (\lambda y.(xy))(\lambda z.w)$$ But should I also change the $x$ in the other expression? It's free in this expression and I don't know if this is completely different $x$ and I should rename it or it's the $x$ from the first one.

If I do this the other way:

$$(\lambda x.(\lambda y.(xy))x)(\lambda z.w) \rightarrow^{\beta} (\lambda x.(xx))(\lambda z.w) \rightarrow^{\beta} ...$$

Still don't know about the $x$.

$\endgroup$
0

1 Answer 1

3
$\begingroup$

Your first attempt of $\beta$-step is not correct. Indeed, in the term $$ (\color{red}{\lambda x}.(\lambda y.(\color{red}{x}y))\color{red}{x})(\lambda z.w) $$

the binder $\lambda x$ binds all the free occurrences of $x$ in the body of the abstraction, i.e., in $\lambda y.(\color{red}{x}y)\color{red}{x}$, which means that both occurrences of $x$ in $\mathrm{\color{red}{red}}$ are bound to $\lambda x$. As a consequence, when you fire the $\beta$-redex $(\lambda x. ...)(\lambda z.w)$, both occurrences of $x$ in $\lambda y.(\color{red}{x}y)\color{red}{x}$ must be replaced by $\lambda z.w$. Summing up, a correct $\beta$-step is the following:

$$(\lambda x.(\lambda y.(xy))x)(\lambda z.w) \rightarrow_{\beta} (\lambda y.( (\lambda z.w)y))(\lambda z.w)$$

Your second $\beta$-step is actually correct. If you keep on reducing $\beta$-redexes in whatever order you prefer, you eventually obtain the same term. This property holds in general for the $\lambda$-calculus and it is known as confluence or Church-Rosser. In your example, your final term (obtained by performing $\beta$-reduction with any order) is $w$.

$\endgroup$

You must log in to answer this question.

Start asking to get answers

Find the answer to your question by asking.

Ask question

Explore related questions

See similar questions with these tags.