Determining equality of non-well-founded sets

[Calumnia]

I have a program that needs to determine if two sets of objects are equal. (We don't care about the order of elements within a set.) These sets may contain primitive elements (ints, strings, etc.), or possibly other sets.

If both sets we're comparing are well-founded (i.e., they don't contain links back to themselves), then we say they are equal iff they have the same elements. It's not hard to write a recursive function that tests this (pseudocode):

Code: Select all

function equals(A,B):
   if A and B are primitives: return (A==B)
   if A is a set and B is a primitive, or vice-versa: return False
   if A and B are sets:
      for all x in A:
         if not(∃y∈B: equals(x,y)): return False
         else: remove x from B
      if B is nonempty: return False
      else: return True

But what if the sets are not well-founded? Then the above procedure will never finish, but we can still understand an intuitive notion of equality. (The following definition might not be completely rigorous, but I think you'll understand what I'm getting at here.)

1. If A and B are both primitives or well-founded sets, use the above definition.
2. If A is a primitive or well-founded set, and B is a non-well-founded set (or vice-versa), then A≠B.
3. If A and B are both non-well-founded sets, then A=B iff it is possible to assume that A=B without contradicting (1) and (2).

For example, if A = { 3, { 4, B } } and B = { 3, {4, A} }, then A=B. But if A = { B } and B = { 2, A }, then A≠B (because assuming A=B leads to a contradiction).

So, the question is, what's the best algorithm to test for equality, without ending up in an infinite loop?

[mfb]

I am note sure if this is safe in a mathematical way, but looking at your examples:

A=(something1 with B somewhere)
B=(something2 with A somewhere)

In that case, A==B iff something1 and something 2 and the position of B and A are the same. So you can replace B in A and A in B with a new symbol and check them like a well-founded set. In a similar way, it should be possible to replace A in A and B in B with another new symbol (check that).

[philoctetes]

I may be looking wrong at your examples, but I don't see any way in which the two are different.

In the second example, taking A = B = {2,{2,{2,..} } } is no contradiction.Or if there's something wrong with that, why isn't the first example bad too?

[jaap]

I may be looking wrong at your examples, but I don't see any way in which the two are different.

In the second example, taking A = B = {2,{2,{2,..} } } is no contradiction.Or if there's something wrong with that, why isn't the first example bad too?

Given that A = { B } and B = { 2, A }, then A has 1 element (namely B), and B must have two elements (namely 2 and A).
If you substitute once, you get
A = { B } = { { 2, A } }.
Note that there are two sets of brackets here - A still contains only one element, which in turn is a set with two elements in it. This is completely different to A = { 2, A }, which you seem to be arriving at.

[philoctetes]

My mistake, you're right.

[lightvector]

I might be mistaken, but it seems like in general this problem is essentially equivalent to determining whether two directed graphs with colored vertices are isomorphic (where "isomorphic" in this case requires exact matching of colors, rather than being allowed to map the colors).

The sets and primitive objects are vertices. Set membership is a directed edge. Each primitive object vertex gets a color different from the colors of any other object, and all set vertices get the same color, except for the two sets that you are asking if they are equal or not.

For instance, in the case A = { 3, { 4, B } } and B = { 3, {4, A} }, you have a directed graph with nodes A, B, 3, 4, X, Y and edges A -> 3, A -> X, X -> 4, X -> B, B -> 3, B -> Y, Y -> 4, Y -> A. The vertices 3 and 4 are given special colors, and all the other sets are given the same color. Then asking whether A and B are equal in the sense you described is equivalent to asking whether there is an isomorphism from this graph where A is recolored to another special distinct color (but B, X, Y are still the same color) to the same graph where instead B is recolored to that special distinct color (but A, X, Y are still the same color).

I think you will have to resort to some variant of a graph isomorphism algorithm if you want to solve this problem in general. In fact, it seems like ordinary directed graph isomorphism and this problem can both be easily reduced to one another, so they're almost the same problem in terms of algorithmic difficulty.

[Calumnia]

In that case, A==B iff something1 and something 2 and the position of B and A are the same. So you can replace B in A and A in B with a new symbol and check them like a well-founded set. In a similar way, it should be possible to replace A in A and B in B with another new symbol (check that).

This works in the simple case where the definitions of the sets share the same form; but what about trickier cases such as A={A} and B={{B}}? Would this procedure be able to tell that A=B?

I think you will have to resort to some variant of a graph isomorphism algorithm if you want to solve this problem in general. In fact, it seems like ordinary directed graph isomorphism and this problem can both be easily reduced to one another, so they're almost the same problem in terms of algorithmic difficulty.

This seems like a good way to approach the problem. However, I'm not sure if I understand you completely. How would this handle A={A} and B={{B}}? Can this kind of "isomorphism" apply between graphs with different numbers of nodes? The graph picture of A and B in this case would look like this (disclaimer: MS Paint!):

[Yakk]

Each "set" is a node in a directed graph. Primitive elements are also nodes in this graph.

Sets are only defined by their contents.

The contents of a set are the nodes you can reach from the node.

So A={B} and B={{A}} first implicitly creates a new name of a node C = {A}

This leads to transitions as follows:
B -> C -> A -> B

In the above case, would A = B? Well, yes! The two are isomorphic.

The "leaf" nodes, and the branching factors, determine if they aren't equal.

Interestingly, now that we have proven that A=B=C, it means the graph is just A->A instead of the above more complicated one.

This matters, because if I define E = {A,B} and D={A,A}, a without the above reduction we'd end up saying that E!=D, when actually E=D.

So it isn't just graph a isomoprhism problem in a sense -- it is 'reachable' graph isomorphism, where you can collapse a given set of nodes. I'm not sure how to characterize this reduction. It isn't as simple as homotopy or homology, because A->B->C->{D,E}, D->E->A results in A!=B due to counting of inclusion despite A and B being "the same shape".

[letterX]

So it isn't just graph a isomoprhism problem in a sense -- it is 'reachable' graph isomorphism, where you can collapse a given set of nodes. I'm not sure how to characterize this reduction. It isn't as simple as homotopy or homology, because A->B->C->{D,E}, D->E->A results in A!=B due to counting of inclusion despite A and B being "the same shape".

Would just like to point out that the formal name for this relation is a bisimulation. It's a pretty well understood problem in the context of when two different finite automata are really the same. The Wiki page doesn't give an algorithm for deciding bisimilarity, but I seem to recall that it's not terribly difficult to come up with one.

Also, this notion of "non-well-founded sets" is an example of a coinductively defined datastructure. This is the dual to the usual idea of building terms up by constructors -- for a coinductive datastructure, any term can be destructed (the equivalent of a case... match statement) but not all terms can be constructed by iteratively applying constructors from some atomic terms, like the usual terms that come up in most programming languages.

Interestingly enough, some languages like Ocaml will happily let you type in

Code: Select all

let rec x = 1 :: x;;

It will print [1; 1; 1; 1; ...] for a few lines, and then give up having reached its pretty-printing depth. However, asking it if x = x will put it into an infinite loop, since in general there's no way to establish that two co-terms are bisimilar if they're not given to you as finite-state machines.

[jareds]

This is interesting. I will go ahead and point to some algorithms: Kanellakis and Smolka give a fairly straightforward O(mn) algorithm, where there are n nodes and m edges, and Paige and Tarjan give an O(m log n) algorithm that, frankly, looks like it took some work to come up with.

The idea with both algorithms is to compute a partitioning that defines the bisimilarity (by equivalence classes), by starting with everything in the same equivalence class (although in your case you would start off with the primitives separately partitioned by their natural equivalence), and then breaking up equivalence classes as required under the current relation until it stabilizes.


Edit: Oddly, the example letterX quotes by Yakk ("A->B->C->{D,E}, D->E->A results in A!=B") is not consistent with bisimilarity. The interpretation of the OP that I had in mind originally (as I read the thread on Wednesday) was consistent with bisimilarity. The OP says that if it is consistent for non-well-founded sets to be equal, they are equal. It is consistent for A=B=C=D=E. In this case {D,E}={E,E}={E}=...={A}=E=...=A. Indeed, it is consistent for any set that doesn't contain, directly or indirectly, a well-founded set or a primitive, to be equal to A={A}. I guess it's perfectly coherent to treat things as multisets, but if that's what the OP wants then we still don't know what the relation is called.

[Calumnia]

This is interesting. I will go ahead and point to some algorithms: Kanellakis and Smolka give a fairly straightforward O(mn) algorithm, where there are n nodes and m edges, and Paige and Tarjan give an O(m log n) algorithm that, frankly, looks like it took some work to come up with.

These journals require registration -- any chance you could give a summary of the O(mn) algorithm?

It isn't as simple as homotopy or homology, because A->B->C->{D,E}, D->E->A results in A!=B due to counting of inclusion despite A and B being "the same shape".

Edit: Oddly, the example letterX quotes by Yakk ("A->B->C->{D,E}, D->E->A results in A!=B") is not consistent with bisimilarity. The interpretation of the OP that I had in mind originally (as I read the thread on Wednesday) was consistent with bisimilarity. The OP says that if it is consistent for non-well-founded sets to be equal, they are equal. It is consistent for A=B=C=D=E. In this case {D,E}={E,E}={E}=...={A}=E=...=A. Indeed, it is consistent for any set that doesn't contain, directly or indirectly, a well-founded set or a primitive, to be equal to A={A}. I guess it's perfectly coherent to treat things as multisets, but if that's what the OP wants then we still don't know what the relation is called.

I think what Yakk is saying that A should be counted as equal to B, but approaching it as a simple homotopy or homology incorrectly says that A≠B. (Yakk, is that a correct interpretation?)

Indeed, it was a theorem of Peter Aczel in his book "Non-Well-Founded Sets" that any set that never reaches bottom is equivalent to the so-called "Quine atom", which is defined as Ω={Ω}. (This text is available online somewhere, I think, although I don't think it says much about algorithms to test equality.)

[jareds]

These journals require registration -- any chance you could give a summary of the O(mn) algorithm?

The idea with both algorithms is to compute a partitioning that defines the bisimilarity (by equivalence classes), by starting with everything in the same equivalence class (although in your case you would start off with the primitives separately partitioned by their natural equivalence), and then breaking up equivalence classes as required under the current relation until it stabilizes.

With the first algorithm, you break up the equivalence classes in any order (the authors call it the naive method), and you're bounded by O(mn) because you can perform at most n-1 break-ups. When you break up an equivalence class, you partition such that two nodes are the same if their sets of equivalence classes of the destination of their edges are the same. You need to do a little work to do this in O(m) time, in particular sorting the edges by equivalence class so the comparison is linear in the number of edges of the node.

Actually, nevermind. I found an online chapter of a book (on the author's web page) that presents both algorithms. (It was also a paper of his that pointed me to the two papers I cited, so it is no major coincidence that I now found a summary of both algorithms by him.)

[Yakk]

Nope, I missed the "everything equals each other, which equals A={A}". To enforce a split where I want it you'd have to force a tuple.

ie:
A = {B}
B = {C}
C = { D, E }
D = {{},E}
E = {{{}},A}
where I force C to be a tuple by indexing its elements.

Then the graph looks like this:

Code: Select all

                 1
                 ^
                 |
  A -> B -> C -> E -> A
            |    ^
            |    |
            \--> D -> 0


... which then leads to the correct conclusion, because the above prevents everything from being A={A}.

In any case, it appears that "bisimilarity" is the keyword that is being looked for.