We are looking for a proof or counter-examples for the following hypothesis.

Two combinators $M$ and $N$ are solvable and equivalent in the HP-complete sensible $\lambda$-theory iff either $$ \exists n \in \mathbb N: \langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \rightarrow^* \langle\varnothing\ |\ x_1 = x_1,\dots, x_n = x_n\rangle, $$ or $$ \forall n \in \mathbb N: \langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \rightarrow^* \langle\varnothing\ |\ x_1 = x_1,\dots, x_n = x_n, \Delta\rangle, $$ where $\Gamma(M, x)$ and $\Gamma^*(N, x)$ are defined in a compact encoding for $\lambda$-terms in interaction calculus.

Any help would be appreciated.


One counterexample for the forward implication ($\not\Rightarrow$) is solvable $M \equiv N \equiv \lambda x.x\ \Omega$. Indeed, $$ \langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \not\rightarrow^* \langle\varnothing\ |\ x_1 = x_1, x_2 = x_2, \Delta\rangle. $$

Another counterexample ($\not\Leftarrow$) is based on $I = J$ demonstrated in arXiv:1304.2290. Specifically, if $M \equiv \lambda x.x\ I\ I$ and $N \equiv \lambda x.x\ J\ \Omega$, then $$ \forall n \in \mathbb N: \langle\varnothing\ |\ \Gamma(M, x) \cup \Gamma^*(N, x)\rangle \rightarrow^* \langle\varnothing\ |\ x_1 = x_1,\dots, x_n = x_n, \Delta\rangle. $$ However, $M\ F = I$ is solvable while $N\ F = \Omega$ is not, which contradicts sensibility.


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.