λ-calculus: When is it possible to split a term into two or more expressions, so that each can be used in separate β-reductions?

Question

In the $\lambda$-calculus expression:

$$ (\lambda x.\lambda y.xy)(f(f(a))) $$

Can the subexpression $(f(f(a))$ be split into two terms, $M$ and $N$? (Maybe, via $\alpha$-conversion?) If so, what could those two terms be? $f$ and $fa$? $ff$ and $a$?

---

Suppose it is possible. Then we'd have $(\lambda xy.xy)(MN)$. Are the following steps valid?:

\begin{align} (\lambda xy.xy)(MN) \\ (\lambda xy.xy)MN \\ ((\lambda xy.xy)[x:=M])N \\ (\lambda y.My)N \\ (\lambda y.My)[y:=N] \\ MN \end{align}

Is the second step above valid? I.e. is it valid to go from $(\lambda xy.xy)(MN)$ to $(\lambda xy.xy)MN$?

Answer 1

You're almost right in above comment. Application is left-associative so to be ensured one can arrive at a normal form (but in some cases may not be necessary). "$λxy.xy$ is shorthand for $λx.(λy.xy)$" this is what I mean a "curried function abstraction". Yes, the result should be $λy.(MN)y$, which is $λy.((MN)y)$ strictly speaking for your example. If you're new, you'd better always add default parenthesis when confused, never delete though.