1
$\begingroup$

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

$\endgroup$
2
$\begingroup$

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.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.