3
$\begingroup$

Consider the 3 symmetric interaction combinator nets below:

equiv

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:

other nets

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?

$\endgroup$
3
  • $\begingroup$ Just a note, a fast algorithm would be to "readback" a λ-term on every possible "mirroring" of the graph, and then use a "visited" map to avoid the exponential blowup, but I'm afraid that's way too contrived and I'm missing the simple / obvious way to do it. $\endgroup$
    – MaiaVictor
    May 24 at 18:10
  • $\begingroup$ i.imgur.com/B3vdo96.png $\endgroup$
    – MaiaVictor
    May 27 at 2:31
  • $\begingroup$ I've posted a separate question for the original notion of equivalence described by Mazza (i.e., not my altered notion). I've answered with an initial algorithm that, to my surprise, can be easily adapted to also answer this question. $\endgroup$
    – MaiaVictor
    May 31 at 3:20

1 Answer 1

3
$\begingroup$

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:

enter image description here

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.

$\endgroup$
0

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge that you have read and understand our privacy policy and code of conduct.

Not the answer you're looking for? Browse other questions tagged or ask your own question.