How to find a simple function in Lambda Calculus? I was doing this exercise :
Find the function $$exchange$$ such that:
   $$(exchange)t \simeq \lambda p(p)t_2 t_1$$
where $$t= \lambda p(p)t_1 t_2.$$
I found $$ exchange= \lambda p(p) (\lambda c (S \ \textit{FALSE} 
 \ \textit{TRUE} (c))) $$
where $$\textit{TRUE} = \lambda x \lambda y x$$
             $$\textit{FALSE}= \lambda x \lambda y y$$
             $$S= \lambda x \lambda y \lambda z(xz(yz))$$
Is it correct?
Thank you,
Alessandro.
 A: Your proposal for the term $exchange$ does not seem to work. Let's see the $\beta$-conversion step by step.
Notations: $\to_\beta$ stands for one $\beta$-reduction step, $\to_\beta^*$ stands for several $\beta$-reduction steps (i.e. some $\beta$-reduction steps are left implicit). The terms $TRUE$ and $FALSE$ are denoted by $T$ and $F$, respectively.
First, note that
$$S F T c \to_\beta^* (F c)(T c) \to_\beta (\lambda y y) (T c) \to_\beta T c \to_\beta \lambda y c.$$
Therefore, taking your definition of $exchange$, we have
$$(exchange)t \to_\beta (\lambda p (p) t_1 t_2) (\lambda c S F T c) \to_\beta (\lambda c S F T c) t_1 t_2 \to_\beta^* (\lambda c \lambda y c)t_1 t_2 \to_\beta^* t_1 \neq  \lambda p (p) t_2 t_1.$$
But, if we set
$$\tag{1}
exchange = \lambda z (z)(\lambda x \lambda y \lambda p (p) y x)
$$
then,
$$
(exchange)t \to_\beta (\lambda p (p) t_1 t_2)(\lambda x \lambda y \lambda p (p) y x) \to_\beta (\lambda x \lambda y \lambda p (p) y x) t_1 t_2 \to_\beta^* \lambda p (p) t_2 t_1
$$
which is exactly what we are looking for!

Edit: There is no general strategy to answer questions like this, intuition is always your best friend. Anyway, I can try to explain how I found the answer. I hope you can follow my intuition.
First, since I have to switch the position of $t_1$ and $t_2$ in the argument $t$, one of the most simple (for me) idea is: let's try if I can solve the problem by moving the argument $t$ in head position (any term can be written in a unique way as $\lambda x_1 \dots \lambda x_n (s) r_1 \dots r_m$, for some $n, m \geq 0$: $s$ is the head position of this term). Under this assumption (and there is no guarantee that it will work), $exchange$ should be of the form 
$$ \tag{2}
exchange = \lambda z \, zM
$$
where $M$ is a term to define. 
Indeed, according to this definition of $exchange$, we have
$$
(exchange)t \to_\beta tM \,.
$$
Since $t = \lambda p (p) t_1 t_2$, then 
$$
tM \to_\beta M t_1 t_2\,.
$$
Now, we have to define $M$ in order to get $$M t_1 t_2 \to_\beta^* \lambda p (p) t_2 t_1\,.$$
It is simple to find such a $M$! 
It should have a $p$ in head position and swap the two arguments $t_1$ and $t_2$ under the abstraction $\lambda p$. Thus, it is enough to set $$M =  \lambda x \lambda y \lambda p (p) y x\,.$$
Going back to the definition $(2)$, we get (1).
