5
$\begingroup$

I'm just looking for the general idea on how to approach the following problem:

Find a term $\Delta=\lambda x.xUV$ such that:

  1. $\Delta\Delta=K$
  2. $\Delta K=S$

(it's a system of 2 equations, I didn't know how to format it properly)

Where $K=\lambda xy.x$ and $S=\lambda xyz.xz(yz)$

I think I need to use Bohm theorem but I don't know exactly how.

$\endgroup$
5
$\begingroup$

This is not directly a consequence of Böhm's theorem. Böhm's theorem states that for any strongly normalizing $A$ and $B$ that are not $\beta\eta$-convertible, there exists $\Gamma$ such that $\Gamma A = K$ and $\Gamma B = S$. You don't get to constrain $\Gamma = A$ or the required form $\lambda x. x U V$. There may be a way to use Böhm's theorem on a different term, but this particular system of equations can easily be solved manually.

If such a term exists then $\Delta K = K U V = U$, so to satisfy the second equation it is necessary that $U = S$.

Then $\Delta \Delta = (\lambda x. x S V) (\lambda x. x S V) = S S V V = S V (V V) = \lambda y. V y (V V y)$. To satisfy the first equation, $V y (V V y) = K y = \lambda z. y$. One way to satisfy this is to take $V = \lambda y z z'. y$.

Finally, verify that $\Delta = \lambda x. x S (\lambda y z z'. y)$ satisfies the two equations.

$\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.