MHB Β reduce a redex - Lambda Calculus.

[JamesBwoii]

As far as I understand it to reduce the formula is:

$(\lambda x.M)N -> β M[N\x]$

Where:

$β M[N\x]$ means M with every free x replaced by N.

I'm stuck on this one though.

$(\lambda x. \lambda y.yx)(\lambda x.xy)$

I know that the answer should be $\lambda z.z(\lambda x.xy)$ but I can't get it.

 

[Evgeny.Makarov]

The substituted term $\lambda x.\,xy$ has a free variable $y$. If it is substituted into $\lambda y.\,yx$ instead of $x$, that free $y$ would become bound, which is wrong. Therefore, the bound $y$ in $\lambda y.\,yx$ has to be renamed first, say, to $z$; then $x$ can be replaced with $\lambda x.\,xy$.

See Wikipedia for the definition of substitution and an example where renaming is necessary. Here are two other examples (renaming is required at some point in finding the normal form, not necessarily during the first reduction).

\((\lambda x.xx)(\lambda yz.yz)\)
\(\lambda xy.(\lambda z.(\lambda x.zx)(\lambda y.zy))(xy)\)

Edit: Does your course really use backslash to denote substitutions? If so, use the [m]\backslash[/m] command in math mode, e.g., $(\lambda x.\,M)N\to_{\beta} M[N\backslash x]$.

 

[JamesBwoii]

The substituted term $\lambda x.\,xy$ has a free variable $y$. If it is substituted into $\lambda y.\,yx$ instead of $x$, that free $y$ would become bound, which is wrong. Therefore, the bound $y$ in $\lambda y.\,yx$ has to be renamed first, say, to $z$; then $x$ can be replaced with $\lambda x.\,xy$.

See Wikipedia for the definition of substitution and an example where renaming is necessary. Here are two other examples (renaming is required at some point in finding the normal form, not necessarily during the first reduction).

\((\lambda x.xx)(\lambda yz.yz)\)
\(\lambda xy.(\lambda z.(\lambda x.zx)(\lambda y.zy))(xy)\)

Edit: Does your course really use backslash to denote substitutions? If so, use the [m]\backslash[/m] command in math mode, e.g., $(\lambda x.\,M)N\to_{\beta} M[N\backslash x]$.

Thank you, I understand it now. :)