如何在 TLA+ 中的 n 元素集中生成 k 组合？答案

【问题标题】：How to generate a k-combination in a n-element set in TLA+?如何在 TLA+ 中的 n 元素集中生成 k 组合？
【发布时间】：2023-01-12 01:49:02
【问题描述】：

在数学中，k-combination of an n-element set 是包含 n 元素集中的 k 个元素的所有集合的集合。

但是，我如何在 TLA+ 中进行计算？

由于我的算法知识不足，我不知道如何计算(n, k)。

但是，我找到了一种丑陋的方法，可以使用笛卡尔积来计算(n, 2)。

假设 n 元素集是X，那么下面的CombinationSeq2(X) 计算X 和X 的笛卡尔积。如果X是{1, 2}，那么结果就是{<<1,1>>, <<1,2>>, <<2,1>>, <<2,2>>}，所以我们必须用s[1] < s[2]来过滤重复的集合，从而得到最终的结果{<<1,2>>}。

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

然后我将内部元组转换为通过以下设置

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

然而，上面的解决方案是丑陋的：

不支持任意k。
它要求集合的元素有顺序。但是，我们这里不需要顺序，告诉是否相等就足够了。
我想知道有什么解决办法吗？我在这个问题上添加了算法标签，因为我相信如果 TLA+ 不支持这个，应该有一些算法方法来做到这一点。如果是这样，我需要一个想法，这样我就可以将它们翻译成 TLA+。

【问题讨论】：

“它要求集合的元素有顺序。但是，我们这里不需要顺序，告诉是否相等就足够了。”<< 非常有趣的观察。我见过的每个组合的实现都隐含地使用了顺序；但是，任何顺序都可以，并且由于集合是有限的，您可以将其元素排列成任意顺序。实际上，考虑生成有限序列组合的算法比生成有限集组合更容易。
我不熟悉 tla+，但一种方法是使用递归公式：如果 S 是一个至少有一个元素的集合，并且 x 是 S 的一个特定元素，那么 Combinations(S, k) = Combinations(S \ {x}, k) union {c union {x} : c in Combinations(S \ {x}, k-1)}（其中 S \ {x} 表示“集差” S 和 {x}”，或等同于 {y in S: y != x})
@Stef给定{ Tiger, Cat, Whale }的集合，这个集合中元素的类型不支持排序，这意味着我们无法比较Tiger是大于还是小于Cat，但我们可以知道@987654341 @ 不等于 Cat。我认为这里“不等于”就足够了。
是的我明白。我的意思是，我所知道的所有算法无论如何都会隐式地对元素进行排序，调用 x_0 = Tiger、x_1 = Cat、x_2 = Whale，并始终返回符合该顺序的组合。
例如我上面给出的递归公式，如果你想把它变成一个实际的算法，你需要一种方法来选择一个集合的任意元素并将其删除；实际上，为序列编写递归会更容易：调用Combinations(n, k)序列的 k 组合 (x_1, ..., x_n)，我们得到：Combinations(n, k) = Combinations(n-1, k) union {c union {x_n} : c in Combinations(n-1, k-1)}

标签： algorithm tla+ pluscal

【解决方案1】：

如果效率不是问题，那么 {s in SUBSET X: CARDINALITY s = k} 应该是正确的。（我说“类似”是因为我在猜测语法。但是CARDINALITY 应该在FiniteSet 中。）

我所知道的所有相当有效的算法都会以某种隐式顺序处理集合。

【讨论】：

【解决方案2】：

在Community Modules中，kSubset被定义为

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

如果纯粹在 TLA+ 中完成，这将在找到子集之前生成 2^S 个元素。 community 模块还有一个 Java override 来更有效地实现计算。有关如何使用覆盖的说明，请参阅 readme。

【讨论】：

【解决方案3】：

我们可以通过编写一个递归函数来生成给定集合的 k 种组合，该函数采用两个参数，i（集合中的当前位置）和k（当前组合中还剩下多少元素）。该函数返回具有k 元素的所有组合的集合。

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.

我们可以从f(1, k) 得到 n 元素集的 k 组合的答案。

注意：如您所见，该函数的工作与给定集合中元素的顺序无关。

我不知道 TLA+，但这是 implementation in C++。

【讨论】：

很想知道为什么我被否决，只是简单地否决而不解释为什么是毫无意义的活动 imo，尤其是在像 stackoverflow 这样的技术网站上。
您不能在 TLA+ 中以这种方式实现 ksubsets。集合是无序的，不能被索引，递归解决方案几乎总是一个坏主意。
我没有投反对票，但我认为这是因为 C++ 实现不能轻易转换为 TLA+——一种是编程语言，另一种是逻辑。