# Lambda term satisfying two equations using Bohm Trees

Hi I'm trying to solve this exercise but I can't find any material online, it's not an homework I actually have sort of a solution (it looks incomplete though), but from that I can't really understand much about how to tackle the problem. Anyway we're asked to find a term $$\Delta$$ such that: $$\left\{\begin{matrix} \Delta(\lambda x y. x (y(\lambda u.yuy)x)x)=y_1 \\ \Delta(\lambda xy.x(y(\lambda u.yu(\lambda abc.cab))x)x) = y_2 \end{matrix}\right.$$

I looked at a similar exercise where the idea was to define $$\Delta$$ to be an abstraction of the type $$\lambda x. x R_3$$ where $$R_3$$ is the ROTATION operation on Bohm Trees (takes the leftmost child of a tree with k+1 subtrees and makes it the new root).

Could someone please explain me how to solve these type of problems? thanks

First, $$\Delta$$ should obviously be a function applying its argument to at least two terms (because it's $$\lambda x y.$$). So let's set $$\Delta = \lambda f.fXY$$, which gives $$X(Y(\lambda u.YuY)X)X=y_1 \\ X(Y(\lambda u.Yu(\lambda abc.cab))X)X = y_2$$ Now we see that $$Y$$ is mostly applied to other terms that seem complex enough to solve this task for themselves, so why not just set $$Y=I(=\lambda t.t)$$?
This leads us to $$X(XI)X=y_1 \\ X(X(\lambda abc.cab))X = y_2$$ $$X$$ is now an abstraction of at least two variables, but we see that the second one (it's always $$X$$ in the first application) can probably be ignored. Setting $$X=\lambda p q.Mp$$: $$M(\lambda q.MI)=y_1 \\ M(\lambda q.M(\lambda abc.cab)) = y_2$$ The same ways we did with $$\Delta$$, we see that M takes an argument with at most three abstractions, so we make $$M=\lambda f.(f P Q R)$$. Doing several beta reductions, this yields $$PQRQR=y_1 \\ RPQQR = y_2$$ with the obvious solutions $$P=\lambda a b c d.y_1$$ and $$R=\lambda a b c d.y_2$$ and the free parameter $$Q$$.
Now finally, we can insert these terms back into $$M$$, $$X$$ and $$\Delta$$ to yield the solution $$\Delta=\lambda f.f(\lambda p q.p(\lambda a b c d.y_1)I(\lambda a b c d.y_2))I$$ (setting $$Q=I$$ for brevity's sake).