Rules for beta conversion passing abstraction as parameter

Question

Can you tell me why the following reduction is true?

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

I'm not quite sure about the rules to follow when abstraction $(\lambda y.xy)$ is applied to $(\lambda x.yx)$.

Thanks.

Answer 1

It's because

$$ \lambda y.xy \to_\eta x $$

So rightly

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

Answer 2

The rule for $\beta$-reduction is unique and always the same: $$ (\lambda x. M)N \to_\beta M[N/x] $$ where $M[N/x]$ is the term obtained from $M$ by substituting $N$ for each free occurrence of the variable $x$ in $M$.

In your example, $M = yx$ and $N = \lambda y. xy$, hence $M[N/x] = y(\lambda y. xy)$ because in $yx$ the free variable $x$ is replaced with $\lambda y. xy$.

Summing up, the correct $\beta$-reduction in your example is $$ (\lambda x.yx)(\lambda y.xy) \to_\beta y(\lambda y. xy) $$