Let $A$ and $B$ be $\lambda$-terms. Given the application $(AB)$ is there a way to get back $A$? Is there a way to get back $B$?
It's not as simple as $(\lambda xy.x)(AB) \rightarrow_\beta \lambda y.(AB)$ because that's not equal to $((\lambda xy.x)A)B = A$. Similarly for $(\lambda xy.y)(AB) \not \rightarrow_\beta ((\lambda xy.x)A)B$.
Alternatively,
Is there a function $f$ such that:
$$f(AB) = (fA)B$$
Or are there functions $f$ and $g$ such that:
$$f(AB) = (gA)B$$
I'm trying to undo an application $AB$ to get back the constituent parts, $A$ and $B$, separately. I read that for Church numbers $\bar b$ and $\bar e$, the application $\bar e \bar b$ is the Church number $\overline{b^e}$, so in some sense an application is like exponentiation whose "inverse" is to take the logarithm - it's not really an inverse though and you have to know $b$ to get back $e$ as $log_b(b^e) = e$. I don't know if this is relevant though.
There is no way to get $B$ back - consider the term $A = \lambda y . \lambda x . x$. Then $AB = \lambda x . x$ for all $B$.
There is no way to get $A$ back either. Let $B = \lambda x . x$, $A_1 = \lambda y . \lambda x . x$, and $A_2 = \lambda x . x$. Then $A_1 B = A_2 B$ but $A_1 \neq A_2$.