Lambda term satisfying two equations using Bohm Trees

Question

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

Answer 1

This task can be solved very well by observation and inserting simple functions.

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).
There could very well be a smaller solution, but I think the derivation process is the simplest you can get with this one.