patternMinor
Find a lambda term satisfying two equations
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:
(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.
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.
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.