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?