Hypothesis: interaction-based model for λKβη

Question

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

Hypothesis. In interaction calculus $\langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \downarrow \langle \varnothing\ |\ x_1 = x_1, \dots, x_n = x_n \rangle$, where the $\Gamma$ mapping is defined in a compact encoding for $\lambda$-terms, $M, N \in \Lambda_0$ are combinators, and $n \geq 1$, if and only if $\lambda K\beta\eta \vdash M = N$.

In the case if the hypothesis holds true, we have an effective model for the $\lambda K\beta\eta$ equational theory.

Answer 1

One counterexample for the forward implication ($\not\Rightarrow$) is $M \equiv \lambda x.x\ I\ I$ and $M \equiv \lambda x.x\ I\ F$. Indeed,

$$ \langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \rightarrow^* \langle \varnothing\ |\ x = x\rangle, $$

but $M$ and $N$ are different $\beta\eta$-normal forms.

Another counterexample ($\not\Leftarrow$) is an equation $M \equiv I = K\ I\ \Omega \equiv N$ which is valid in $\lambda K\beta\eta$. Indeed, $$ \langle \varnothing\ |\ \Gamma(M, x) \cup \Gamma(N, x)\rangle \rightarrow^* \langle \varnothing\ |\ x = x, \Gamma(\Omega, \epsilon) \rangle, $$ while the subnet $\langle \varnothing\ |\ \Gamma(\Omega, \epsilon)\rangle$ does not have a normal form.

On the other hand, the hypothesis might still be provable for $\lambda I\beta\eta$-calculus.