Determining equality of non-well-founded sets

A place to discuss the science of computers and programs, from algorithms to computability.

Formal proofs preferred.

Moderators: phlip, Prelates, Moderators General

Determining equality of non-well-founded sets

Postby Calumnia » Wed Nov 30, 2011 6:50 am UTC

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?
Calumnia
 
Posts: 13
Joined: Fri Jun 04, 2010 9:23 pm UTC

Re: Determining equality of non-well-founded sets

Postby mfb » Wed Nov 30, 2011 11:07 am UTC

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).
mfb
 
Posts: 827
Joined: Thu Jan 08, 2009 7:48 pm UTC

Re: Determining equality of non-well-founded sets

Postby philoctetes » Wed Nov 30, 2011 12:31 pm UTC

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?
philoctetes
 
Posts: 35
Joined: Tue Feb 19, 2008 3:26 pm UTC

Re: Determining equality of non-well-founded sets

Postby jaap » Wed Nov 30, 2011 2:37 pm UTC

philoctetes wrote: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.
User avatar
jaap
 
Posts: 1789
Joined: Fri Jul 06, 2007 7:06 am UTC

Re: Determining equality of non-well-founded sets

Postby philoctetes » Wed Nov 30, 2011 2:54 pm UTC

My mistake, you're right.
philoctetes
 
Posts: 35
Joined: Tue Feb 19, 2008 3:26 pm UTC

Re: Determining equality of non-well-founded sets

Postby lightvector » Thu Dec 01, 2011 12:59 am UTC

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.
lightvector
 
Posts: 194
Joined: Tue Jun 17, 2008 11:04 pm UTC

Re: Determining equality of non-well-founded sets

Postby Calumnia » Thu Dec 01, 2011 7:01 am UTC

mfb wrote: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?

lightvector wrote: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!):

Image
Calumnia
 
Posts: 13
Joined: Fri Jun 04, 2010 9:23 pm UTC

Re: Determining equality of non-well-founded sets

Postby Yakk » Thu Dec 01, 2011 9:48 pm UTC

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".
One of the painful things about our time is that those who feel certainty are stupid, and those with any imagination and understanding are filled with doubt and indecision - BR

Last edited by JHVH on Fri Oct 23, 4004 BCE 6:17 pm, edited 6 times in total.
User avatar
Yakk
Poster with most posts but no title.
 
Posts: 10324
Joined: Sat Jan 27, 2007 7:27 pm UTC
Location: E pur si muove

Re: Determining equality of non-well-founded sets

Postby letterX » Fri Dec 02, 2011 3:43 am UTC

Yakk wrote: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.
letterX
 
Posts: 523
Joined: Fri Feb 22, 2008 4:00 am UTC
Location: Ithaca, NY

Re: Determining equality of non-well-founded sets

Postby jareds » Fri Dec 02, 2011 12:12 pm UTC

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.
jareds
 
Posts: 375
Joined: Wed Jan 03, 2007 3:56 pm UTC

Re: Determining equality of non-well-founded sets

Postby Calumnia » Sat Dec 03, 2011 3:33 am UTC

jareds wrote: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?

Yakk wrote: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".


jareds wrote: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.)
Calumnia
 
Posts: 13
Joined: Fri Jun 04, 2010 9:23 pm UTC

Re: Determining equality of non-well-founded sets

Postby jareds » Sat Dec 03, 2011 6:02 am UTC

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

jareds wrote: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.)
jareds
 
Posts: 375
Joined: Wed Jan 03, 2007 3:56 pm UTC

Re: Determining equality of non-well-founded sets

Postby Yakk » Sat Dec 03, 2011 3:01 pm UTC

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.
One of the painful things about our time is that those who feel certainty are stupid, and those with any imagination and understanding are filled with doubt and indecision - BR

Last edited by JHVH on Fri Oct 23, 4004 BCE 6:17 pm, edited 6 times in total.
User avatar
Yakk
Poster with most posts but no title.
 
Posts: 10324
Joined: Sat Jan 27, 2007 7:27 pm UTC
Location: E pur si muove


Return to Computer Science

Who is online

Users browsing this forum: No registered users and 1 guest