# What is an efficient algorithm to check for equivalence on symmetric interaction combinators?

Symmetric interaction combinators are a graph-rewriting model of deterministic computation derived from Lafont's interaction nets. In the paper "Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators" [1], a notion of observational equivalence is defined, identifying two interaction nets when they produce the same set of observable axioms in any context. Interestingly, and as on the λ-calculus, this notion admits a set of η-equivalence rules:

Unlike the λ-calculus, though, η-equivalence isn't trivial, and can demand a complex series of rewrites to equate two sides. For example, both nets below are η-equivalent, even though it isn't immediately obvious:

Is there an efficient algorithm for determining whether two normalized symmetric interaction nets are observationally equivalent?

[1] Mazza, D. (2012). Observational Equivalence and Full Abstraction in the Symmetric Interaction Combinators. Logical Methods in Computer Science, Volume 5, Issue 4, lmcs:1150. link

• Note: I've previously asked if there is an algorithm to check if two nets are equivalent, under a specific and incomplete equivalence relation that I defined on the post. Now, I realize that even the standard notion is lacking a published algorithm. Since the original thread was, admittedly, not very well written, and given it already received a great answer in the way it was asked, believe it is best to post this as a separate question. This is central problem that other people could need to solve a future. May 27, 2023 at 15:14
• github.com/VictorTaelin/Interaction-Type-Theory Jul 11, 2023 at 16:00

This is NOT a complete answer yet, as I provide no proof. But, my rough understanding right now is that we can check if two ports are identical by moving a "signal" forward until the root node is reached, and checking if the paths traversed are the same. This (should?) correspond computationally to Mazza's notion of observational equivalence, where 2 nets are equal if they produce the same observable axioms under any context.

The way a signal moves is similar to the machine described by Lafont in the original paper. When entering an aux port, the signal moves to the main port and adds the entered direction to a deque. When entering a main port, it pops a direction from the deque, and moves to it. If there is no direction to pop, it instead moves to both directions, and prepends them to the other argument's deque. For example, if the signal 'a' is entering a main port, and if its deque is empty, then it splits, recurses towards both aux ports, and prepends the chosen direction to the 'b' deque. This creates a "debt" that forces 'b' to follow the same path as 'a', and vice-versa. When reaching the root, the deques (i.e., unconsumed paths) are compared for equality. For example, below are 2 equivalent nets:

Highlighted in red are signals traversing through the nets, starting from the same port, and ending on the root. On the left net, the signal splits and traverses two paths. On the right, it traverses only one path. Regardless, the unconsumed paths are the same. This is true for all possible signals, thus, these nets are equivalent. Here is another example:

In this case, in both nets the signal splits, yet the leftover paths on both branches are still identical. Note I'm not drawing the complete path, I'm stopping at the first aux port, but it should extend towards root. Also keep in mind there are actually two roots: where the signal started (local root), and the network global root. Reaching the local root is akin to reaching the top of the terms you want to compare. Reaching the global root is akin to finding a free variable.

Here is a pseudocode of how the algorithm would look like:

Equality on Interaction Combinators

A Path is a deque of aux slots (1 or 2)

> type Slot = 1 | 2
> type Path = [Slot]

A cursor has a root port, a prev port, and a map of paths

> type Cursor = { root: Port, prev: Port, path: Map<Kind, Path> }

The equality function returns if two nets are equal

> eq : INet -> Cursor -> Cursor -> Bool

If we're on root, compare both deque maps

> eq a am b bm = am == bm

If main port, non-empty deque: pop_back a slot from this deque, and move to it

> eq ak#[*a0 a1 a2] {[ak]:(1,ap),..am} b bm = eq a1 {[ak]:ap,..am} b bm
> eq ak#[*a0 a1 a2] {[ak]:(2,ap),..am} b bm = eq a2 {[ak]:ap,..am} b bm

If main port, empty deque: push_front [1,2] slots to the other deque, and move to both

> eq ak#[*a0 a1 a2] {[ak]:ap,..am} b {[ak]:bs,..bm} = eq a1 ap b {[ak]:(bs,1),..bm}
& eq a2 ap b {[ak]:(bs,2),..bm}

If aux port, push_back it to this deque, and move to main port

> eq ak[a0 *a1 a2] {[ak]:ap,..am} b bm = eq a1 {[ak]:(1,ap),..am} b bm
> eq ak[a0 a1 *a2] {[ak]:ap,..am} b bm = eq a1 {[ak]:(2,ap),..am} b bm

The rules above that match on 'a' are repeated for 'b'.


In the notation above, k#[a b c] stands for an interaction combinator node with label k and ports a, b, c, with a being the main port. The * stands for the port we're entering from on the recursive call. The {...} notation represents a map of deques, using a JS-like spread operator notation. I use (1,ad) to prepend 1 to the deque ad, and (ad,1) to append 1 to it. A complete implementation of interaction combinators, including this equality function, is available on this Rust file.

Also, I suspect this is essentially just constructing an edifice, so, there is nothing new here - but I don't understand edifices well enough to say for sure. Yet, by moving both signals alternatively, we can attempt to synchronize them and "untie the knot" to check equality on fixed points (example). Moreover, this algorithm can be made more flexible by simply considering only the deques with a specific label (ex: 0) on the base case. This allows us to have "duplication-invariant" equality, which is interesting because it imples same λ-calculus read-back, answering my earlier question.

Again, keep in mind this is an initial idea and could be wrong. I provide no proof yet, but it seems to work in initial tests, and make logical sense.

Edit: since the explanation above is a little bit confusing, here is a simplified algorithm in pseudocode:

def equal(a: Cursor, b: Cursor) -> Bool:
s = a.target_slot()
k = a.target_kind()

// If both loops are complete, compare deques
if a.done() && b.done():
return a.deque[0] == b.deque[0] // [0] for con equality

// if 'a' loop is complete, swap (to move 'b')
if a.done():
return equal(b, a)

// If 'a' on main and deque is empty, split the signal
if s == 0 && a.deque[k].empty():
a1 = a.clone().move(1)
a2 = a.clone().move(2)
b1 = b.clone()
b2 = b.clone()
b.deque[k].prepend(1)
b.deque[k].prepend(2)
return equal(a1, b1) && equal(a2, b2)

// If 'a' on main and deque is full, pop and move down
if s == 0 && !a.deque[k].empty():
a.move(a.deque[k].pop())
return equal(a, b)

// If 'a' is an aux port, push and move up
if s > 0:
a.deque[k].push(s)
a.move(0)
return equal(a, b)


For discussions on how this can be done, please check https://discord.com/channels/912426566838013994/915345481675186197/1109236255662821457

• whoever from the future is here, please make the world a better place Jun 2, 2023 at 17:37