Removing "equivalents" from a set

[Jam]

Hello. I have a small problem that I haven't been able to solve:

What I'm trying to achieve is given a set of numbers, I want to partition it into smaller sets(in this case with size 2), and eliminate equivalent partitions to save resources.

6 hours later, I have arrived at this result, which is almost what I want:

s == { {{1}},
     {{2}},
     {{3}},
     {{4}},
     {{1, 2}},
     {{1, 3}},
     {{1, 4}},
     {{2, 3}},
     {{2, 4}},
     {{3, 4}},
     {{1}, {2, 3}},
     {{1}, {2, 4}},
     {{1}, {3, 4}},
     {{2}, {1, 3}},
     {{2}, {1, 4}},
     {{2}, {3, 4}},
     {{3}, {1, 2}},
     {{3}, {1, 4}},
     {{3}, {2, 4}},
     {{4}, {1, 2}},
     {{4}, {1, 3}},
     {{4}, {2, 3}},
     {{1, 2}, {3, 4}},
     {{1, 3}, {2, 4}},
     {{1, 4}, {2, 3}} }

What I am trying to do is to remove elements of this set, if the element's UNION is already contained in the set, giving me the following set:

{ {{1}},
     {{2}},
     {{3}},
     {{4}},
     {{1, 2}},
     {{1, 3}},
     {{1, 4}},
     {{2, 3}},
     {{2, 4}},
     {{3, 4}},
     {{1}, {2, 3}},
     {{1}, {2, 4}},
     {{1}, {3, 4}},
     {{2}, {3, 4}},
     {{1, 2}, {3, 4}} }

How could this be done? I have not found any way asserting that a predicate is true for every pair of elements in a set. 

[Leslie Lamport]

In constructing the second set, you have removed from s the element {{3}, {2,4}}  the union of the elements of that set is the set {2,3,4}.  That set is not in s, since s has no 3-element sets, so it does not satisfy your condition for an element to be removed from s.  Therefore, what you have written makes no sense to me.  

You seem to want to define an operator Op such that Op(s) equals the second set.  By talking about "removing elements", I presume you meant that Op(s) should be a subset of s.  Hence, I believe that the definition you want should be expressible as

    Op(t) == CHOOSE u \in SUBSET t : P(t, u)

for some formula  P(t, u).  This definition of Op may not satisfy you because to evaluate it, TLC must compute all elements of SUBSET t and evaluate P(t,u) for all the elements u of SUBSET t until it finds one that evaluates to TRUE.  However, it will at least tell people what operator Op you want.

[sgl...@sglaser.com]

I think you want something like:

RECURSIVE union_set2(_, _)

union_set2(x, y) == 

    IF x = {}

        THEN y

        ELSE CHOOSE a \in x :

           IF \E b \in y : UNION a = UNION b

               THEN union_set2(x \ a, y)

               ELSE union_set2(x \ a, y \cup {a})

   

union_set(x) == union_set2(x, {})

---

Steve Glaser
sgl...@sglaser.com

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Jam]

Thank you for the reply! I actually didn't think of SUBSET because I never really thought of using it for anything else than a set of numbers! I tried it on a very small set derived from 1..3, but I haven't got a result in a couple of minutes. I have decided that the of couple extra elements will not hurt my model as much as this heavy computation. I still appreciate the answer, I'm sure it will help me down the road. Also I think you missed that my resulting set contains element {{2}, {3, 4}}  which has the union {2, 3, 4}.

[Jam]

Hi, thanks for the answer! I haven't been able to get your solution to work, and I don't know hot to troubleshoot it yet. I have decided to abandon this part of the model for simplicity. I hope you didn't spend too much time on this! I will take another look at it after i get more familiar with recursive actions.

On Friday, April 19, 2019 at 12:12:07 AM UTC+2, Steve Glaser wrote:

I think you want something like:

RECURSIVE union_set2(_, _)

union_set2(x, y) == 

    IF x = {}

        THEN y

        ELSE CHOOSE a \in x :

           IF \E b \in y : UNION a = UNION b

               THEN union_set2(x \ a, y)

               ELSE union_set2(x \ a, y \cup {a})

   

union_set(x) == union_set2(x, {})

---

Steve Glaser
sgl...@sglaser.com

On Apr 18, 2019, 3:01 PM -0700, Leslie Lamport <tlap...@gmail.com>, wrote:

In constructing the second set, you have removed from s the element {{3}, {2,4}}  the union of the elements of that set is the set {2,3,4}.  That set is not in s, since s has no 3-element sets, so it does not satisfy your condition for an element to be removed from s.  Therefore, what you have written makes no sense to me.  

You seem to want to define an operator Op such that Op(s) equals the second set.  By talking about "removing elements", I presume you meant that Op(s) should be a subset of s.  Hence, I believe that the definition you want should be expressible as

    Op(t) == CHOOSE u \in SUBSET t : P(t, u)

for some formula  P(t, u).  This definition of Op may not satisfy you because to evaluate it, TLC must compute all elements of SUBSET t and evaluate P(t,u) for all the elements u of SUBSET t until it finds one that evaluates to TRUE.  However, it will at least tell people what operator Op you want.

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.