How to generate a k-combination in a n-element set in TLA+?

Question

In math, a k-combination of an n-element set is a set of all sets that take k element of the n-element set.

However, how can I compute this in TLA+?

I don't know how to compute (n, k), due to my poor algorithm knowledge.

However, I find an ugly way that can compute (n, 2) by using cartesian product.

Suppose the n-element set is X, so the following CombinationSeq2(X) computes the cartesian product of X and X. If X is {1, 2}, then the result is {<<1,1>>, <<1,2>>, <<2,1>>, <<2,2>>}, so we must use s[1] < s[2] to filter repeated sets, thus yielding the final result {<<1,2>>}.

CombinationSeq2(X) == {s \in X \X X: s[1] < s[2]}

Then I convert inner tuple to set by the following

Combination2(X) == { { s[1], s[2] } : s \in CombinationSeq2(X) }

However, the above solution is ugly:

1. it do not support arbitrary k.
2. it requires element of the set to have order. However, we don't need order here, telling equal or not is already enough.

I wonder is there any solution to do this? I added algorithm tag to this question because I believe if TLA+ don't support this, there should be some algorithm way to do this. If so, I need an idea here, so I can translate them into TLA+.

Answer 1

We can generate k-combinations of the given set by writing a recursive function, that takes two parameters, i(current position in the set) and k(how many elements are left in the current combination). The function returns the set of all combinations that have k elements.

f(i, k) = {prepend X[i] to all sets returned by f(i + 1, k - 1)} and f(i + 1, k)
f(n + 1, _) = {}
f(_, 0) = {}

Here, '_'(underscore) refers to any possible value.

We can get the answer for k-combinations of n-elements set from f(1, k).

Note: As you can see the function works irrespective of the order of the elements in the given set.

I don't know TLA+, but here's an implementation in C++.

Answer 2

If efficiency is not a concern, then something like {s \in SUBSET X: CARDINALITY s = k} should be correct. (I say "something like" because I'm kind of guessing at the syntax. But CARDINALITY is supposed to be in FiniteSet.)

All reasonably efficient algorithms that I'm aware of do process the set in some kind of implicit order.

Answer 3

In the Community Modules, kSubset is defined as

kSubset(k, S) == 
   { s \in SUBSET S : Cardinality(s) = k }

If done purely in TLA+, this will generate 2^S elements before finding the subsets. The community module also has a Java override to implement the calculation more efficiently. See the readme for instructions on how to use the override.