如何在TLA+中构造形如{{a,b,c}|a∈S,b∈T,c∈U}的集合？

要生成形如{{a, b, c} : a ∈ S, b ∈ T, c ∈ U}的集合，直接使用TLA+的集合推导语法即可，核心是把集合构造符内的表达式替换为你需要的集合元素：

DesiredSet == {{a, b, c} : a ∈ S, b ∈ T, c ∈ U}

关键说明 #

• TLA+的集合推导语法{ e : x ∈ X, y ∈ Y, ... }会遍历所有变量的取值组合，将每个组合代入表达式e，最终收集所有结果形成集合。这里的e就是单个集合元素{a, b, c}。
• 由于集合的特性：
  • 无序性：{a, b, c}和{b, a, c}会被视为同一个集合，最终结果里只会保留一份。
  • 唯一性：如果从S、T、U中取的元素存在重复（比如a = b），那么{a, b, c}会自动简化为{a, c}，最终集合里不会包含重复的元素。
• 对比笛卡尔积：笛卡尔积S × T × U生成的是有序序列<<a, b, c>>，即使元素重复也会保留不同的序列；而上述构造生成的是无序集合，自动去重合并。

示例 #

假设S = {1, 2}，T = {3, 4}，U = {5, 6}，那么DesiredSet的结果为：

{{1, 3, 5}, {1, 3, 6}, {1, 4, 5}, {1, 4, 6}, {2, 3, 5}, {2, 3, 6}, {2, 4, 5}, {2, 4, 6}}

如果S = {1, 1}（集合内重复元素会自动去重，实际等价于{1}），T = {2}，U = {1}，那么DesiredSet的结果为{{1, 2}}，因为{1,2,1}会简化为{1,2}。

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