<p>This does not answer your main question but concerns the following point:</p>
<blockquote>
<p>I'm looking for an equivalence on interaction nets that implies lambda calculus read-back equivalence, but that also identifies the 3 nets above</p>
</blockquote>
<p>The three nets in your example are <em><span class="math-container">$\eta$</span>-equivalent</em>, a notion introduced originally in Lafon't <a href="https://core.ac.uk/download/pdf/81113716.pdf" rel="nofollow noreferrer">paper on the interaction combinators</a> and in a <a href="https://www.sciencedirect.com/science/article/pii/S0304397502006370" rel="nofollow noreferrer">later paper</a> by Fernández and Mackie.  This equivalence in the (symmetric) interaction combinators plays a similar role as <span class="math-container">$\eta$</span>-equivalence in the <span class="math-container">$\lambda$</span>-calculus, where it gets its name.  For example, a result similar to Böhm's theorem holds: for any two non-<span class="math-container">$\eta$</span>-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 <span class="math-container">$\varepsilon$</span> cells.  This implies, in particular, that no non-trivial congruence on nets may equate two reduced non-<span class="math-container">$\eta$</span>-equivalent nets.</p>
<p>In the interaction combinators, <span class="math-container">$\eta$</span>-equivalence is the contextual closure of the following equations:</p>
<p><a href="https://i.sstatic.net/Sgmsf.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/Sgmsf.png" alt="enter image description here" /></a></p>
<p>In the symmetric interaction combinators, <span class="math-container">$\eta$</span>-equivalence is defined by the above rules where <span class="math-container">$\gamma$</span> is replaced everywhere by <span class="math-container">$\zeta$</span>, and the top-left rule for the <span class="math-container">$\zeta$</span> combinator is identical to that of the <span class="math-container">$\delta$</span> combinator.</p>
<p>I don't know whether <span class="math-container">$\eta$</span>-equivalence includes readback-equivalence, but it might be worth checking.</p>

CC BY-SA 4.0
2023-05-26T08:30:59.433Z
2023-05-28T12:09:37.480Z
2023-05-28T12:09:37.480Z
Damiano Mazza
<p>Consider the 3 <a href="https://core.ac.uk/download/pdf/81113716.pdf" rel="nofollow noreferrer">symmetric interaction combinator</a> nets below:</p>
<p><a href="https://i.sstatic.net/ZF1ff.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/ZF1ff.png" alt="equiv" /></a></p>
<p>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 (<code>λf. λx. (f (f (f (f x))))</code>). 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.</p>
<p>Now, consider the following net instead:</p>
<p><a href="https://i.sstatic.net/POksQ.png" rel="nofollow noreferrer"><img src="https://i.sstatic.net/POksQ.png" alt="other nets" /></a></p>
<p>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.</p>
<p>A solution would be to use Damiano Mazza's <a href="https://arxiv.org/pdf/0906.0380.pdf" rel="nofollow noreferrer">axiom-equivalence</a>, 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 <em>consisting of only constructor nodes</em>. 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:</p>
<p><strong>Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?</strong></p>

CC BY-SA 4.0
2023-05-24T18:10:20.577Z
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.
MaiaVictor
CC BY-SA 4.0
2023-05-27T02:31:14.267Z
https://i.imgur.com/B3vdo96.png
MaiaVictor
CC BY-SA 4.0
2023-05-31T03:20:35.717Z
I've posted a [separate question](https://cstheory.stackexchange.com/questions/52889/what-is-an-efficient-algorithm-to-check-for-equivalence-on-symmetric-interaction/52901#52901) 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.
MaiaVictor
CC BY-SA 4.0
2023-07-11T16:00:28.920Z
https://github.com/VictorTaelin/Interaction-Type-Theory
MaiaVictor
<type-theory><interaction-nets><equivalence><interaction-combinators>
Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?
MaiaVictor
# Is there an efficient algorithm to check for duplicator-invariant equivalence on symmetric interaction combinators?

(Asked by: username_0 on 2023-05-24)

Consider the 3 [symmetric interaction combinator](https://core.ac.uk/download/pdf/81113716.pdf) nets below:

[![equiv](https://i.sstatic.net/ZF1ff.png)](https://i.sstatic.net/ZF1ff.png)

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](https://i.sstatic.net/POksQ.png)](https://i.sstatic.net/POksQ.png)

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](https://arxiv.org/pdf/0906.0380.pdf), 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?**

**Tags:** type-theory, interaction-nets, equivalence, interaction-combinators
> **Comments:**
> **username_0**: 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.  
> **username_0**: https://i.imgur.com/B3vdo96.png  
> **username_0**: I've posted a [separate question](https://cstheory.stackexchange.com/questions/52889/what-is-an-efficient-algorithm-to-check-for-equivalence-on-symmetric-interaction/52901#52901) 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.  
> **username_0**: https://github.com/VictorTaelin/Interaction-Type-Theory  

---

## 1 answers

### Answer by username_1 on 2023-05-26. Score: 3 | Accepted answer

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](https://core.ac.uk/download/pdf/81113716.pdf) and in a [later paper](https://www.sciencedirect.com/science/article/pii/S0304397502006370) 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](https://i.sstatic.net/Sgmsf.png)](https://i.sstatic.net/Sgmsf.png)

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.


---

