Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?

Question

Consider the 3 symmetric interaction combinator nets below:

Despite being different nets, they are equal, in the sense that, if we view white nodes as lambdas and applications, and black nodes as duplicators, then, the corresponding sharing graph reads back to the same λ-term, which is the Church Encoded number 4 (λf. λx. (f (f (f (f x))))). As such, we could propose an equivalence relation on nets, based on whether they read back to the same λ-term. Moreover, there is an efficient algorithm to check for equivalence: just convert the net to a λ-term, and compare.

Now, consider the following net instead:

In this case, the notion of equivalence I outlined doesn't apply, because these nets aren't valid λ-terms. I'm looking for an equivalence on interaction nets that implies lambda calculus read-back equivalence, but that also identifies the 3 nets above; or, in other words, one that isn't dependent on the λ-calculus.

A solution would be to use Damiano Mazza's axiom-equivalence, but, while this notion equates all nets above, it doesn't necessarily imply same λ-term read-back. We could, though, adjust it to be duplicator-invariant: two nets µ and ν are considered constructor-axiom-equivalent (µ ≃ ν) if they develop the same observable axioms in any context consisting of only constructor nodes. If my line of thought is correct, this weaker equivalence would, indeed, imply λ-calculus read-back equivalence. The problem is: how do we check for equivalence efficiently? The naive algorithm I thought of is exponential, so I fear I am missing something. Thus, my question is:

Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?

Answer 1

This does not answer your main question but concerns the following point:

I'm looking for an equivalence on interaction nets that implies lambda calculus read-back equivalence, but that also identifies the 3 nets above

The three nets in your example are $\eta$-equivalent, a notion introduced originally in Lafon't paper on the interaction combinators and in a later paper by Fernández and Mackie. This equivalence in the (symmetric) interaction combinators plays a similar role as $\eta$-equivalence in the $\lambda$-calculus, where it gets its name. For example, a result similar to Böhm's theorem holds: for any two non-$\eta$-equivalent reduced nets (no active pair, no vicious circle) with the same number of free ports, there exists a context sending one to a wire and the other to two $\varepsilon$ cells. This implies, in particular, that no non-trivial congruence on nets may equate two reduced non-$\eta$-equivalent nets.

In the interaction combinators, $\eta$-equivalence is the contextual closure of the following equations:

In the symmetric interaction combinators, $\eta$-equivalence is defined by the above rules where $\gamma$ is replaced everywhere by $\zeta$, and the top-left rule for the $\zeta$ combinator is identical to that of the $\delta$ combinator.

I don't know whether $\eta$-equivalence includes readback-equivalence, but it might be worth checking.