Partitions

Recently I got someone asking about a “pluscal puzzle”:

I need an operator to generate all partitions of a set S. S is a constant/model variable.

Each Partition is a set of Parts (and each Part is a set), such that:

/\ Part \in SUBSET S
/\ \A part1, part2 \in Partition:
  part1 # part2 => part1 \intersect part2 = {}
/\ UNION Partition = S

In other words:

Partitions(3) =
{
  { {1,2,3} },
  { {1,2}, {3} },
  { {1,3}, {2} },
  { {1}, {2,3} },
  { {1}, {2}, {3} }
}

Let’s implement this operator. To make things more general, I’m going to instead say that Partitions takes a set of values instead of a number.

The Operator

First, let’s imagine for a second that instead of the elements being sets of sets, they were sequences of sets. So instead of { {a,c}, {b} }, the element was << {a, c}, {b} >>. Now notice that we can encode the same information as a :> 1 @@ b :> 2 @@ c :> 1: “a” is in the first set, “b” is in the second set, etc.

And that’s just a function in the function set [{a, b, c} -> 1..3]! Every function in that set can be read as a mapping between values and the set in the partition they belong to. We just need an operator to go the other way, and convert “map of values to indices” to “indices to set of values”.

EXTENDS Integers, TLC, Sequences, FiniteSets

PartitionsV1(set) ==
  LET F == [set -> 1..Cardinality(set)]
    G(f) == [i \in 1..Cardinality(set) |-> {x \in set: f[x] = i}]
  IN
    {G(f): f \in F}

>> PartitionsV1({"a", "b"})
{<<{}, {"a", "b"}>>, <<{"a"}, {"b"}>>, <<{"b"}, {"a"}>>, <<{"a", "b"}, {}>>}

Now it’s just a matter of converting it back to sets. We can do this with a set map and a Range helper. Note that Range to <<{1, 2}, {}>> gives us the set {{1, 2}, {}}, which is why we have to set diff out the empty set.

Range(f) == {f[x] : x \in DOMAIN f}

Partitions(set) ==
    {Range(P) \ {{}}: P \in PartitionsV1(set)}

Performance Notes

This operator is pretty inefficient, as a lot of the partitions are redundant: <<{1, 2}, {}>> is the same partition as <<{}, {1, 2}>>. [1..n -> 1..n] has n^n elements,1 so the function set for 1..4 has 256 elements, while there are only 15 possible partitions. That’s an overhead of over 10x!

In this case, though, I don’t think the overhead matters too much. The main reason you’d want to generate a set of partitions is to use them as different configurations in your spec, in which case the cost of computing a 256-element set will be washed out by the cost of 15xing your state space.

(The number of partitions of a set follow the bell numbers.)

1

Sometimes n^n is referred to as “tetration” and written as ²n. In this notation, ³n is n^(n^n).