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

数学中，n元集合的k组合是从该集合中选取k个元素组成的所有子集的集合。以下是针对该需求的通用实现思路及TLA+代码方案。

现有局限方案 #

你当前通过笛卡尔积实现了k=2的组合计算：
首先定义笛卡尔积并过滤有序元组：

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

再将元组转换为集合：

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

但该方案存在两个明显不足：

• 仅支持k=2，无法处理任意k值
• 依赖元素的有序性（<操作），而组合本质只需要判断元素是否唯一

通用解决方案思路及TLA+实现 #

思路1：基于子集大小筛选（最简洁方案） #

组合的本质是原集合中所有大小为k的子集，可以直接利用TLA+的集合表达式定义：

Combination(X, k) == { S \in SUBSET X : Cardinality(S) = k }

这个实现完全符合组合的数学定义，无需依赖元素的有序性，支持任意合法的k值（0 ≤ k ≤ Cardinality(X)）。

思路2：递归式实现（体现算法逻辑） #

如果需要直观体现组合的生成过程，可以用递归思路：

• 当k=0时，仅返回空集的集合：{{}}
• 当k等于集合大小n时，仅返回原集合本身的集合：{X}
• 当0 < k < n时，任选一个元素x∈X，组合分为两类：包含x的组合（从X{x}中选k-1个元素并加入x）和不包含x的组合（从X{x}中选k个元素）

对应的TLA+递归定义（需在模块中声明递归）：

RECURSIVE CombinationRec(_, _)
CombinationRec(X, k) == 
  IF k = 0 THEN {{}}
  ELSIF k = Cardinality(X) THEN {X}
  ELSE 
    LET x == CHOOSE x \in X : TRUE
    IN { S \union {x} : S \in CombinationRec(X \ {x}, k-1) } 
       \union CombinationRec(X \ {x}, k)

注：CHOOSE操作会任选X中的一个元素，TLA+的非确定性不影响最终结果的正确性，因为所有可能的选择都会覆盖到所有组合。

方案对比 #

• 子集筛选式实现：最简洁高效，直接利用TLA+的集合原生操作，适合大多数场景
• 递归式实现：更直观体现组合的生成逻辑，适合需要理解算法过程的场景

内容的提问来源于stack exchange，提问作者calvin