Are there any techniques for solving functional equations for unknown functions in lambda calculus?
Suppose I have the identity function defined extensionally as such:
$I x = x$
(that is, by writing down an equation for the expected behaviour of that function) and now I want to solve it for $I$ by doing some algebraical transformation to get the intensional formula for that function:
$I = \lambda x.x$
that tells how exactly does the function do what was expected (that is, how to implement it in lambda calculus).
Of course the identity function is used just as an example. I'm interested in more general methods of solving such equations. In particular, I would like to find a function $B$ that satisfies the following requirement:
$B\;f\;(\lambda x.M) = (\lambda x.f M)$
that is, "injects" the given function $f$ into the given lambda function $(\lambda x.M)$ before its "body" $M$ (which is some arbitrary lambda expression), possibly by taking it apart and constructing a new one, so that it became a parameter the function $f$ is applied to.