HiveBrain v1.2.0
Get Started
← Back to all entries
patternMinor

Find a lambda term satisfying two equations

Submitted by: @import:stackexchange-cs··
0
Viewed 0 times
equationssatisfyingtermtwofindlambda

Problem

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

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

  • $\Delta\Delta=K$



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

Solution

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.

Context

StackExchange Computer Science Q#102137, answer score: 5

Revisions (0)

No revisions yet.