如何编写双层循环Set Comprehension实现特定笛卡尔积式集合构造？

问题描述 #

给定由有限集合组成的有限集合S，需要构造一个集合的集合，满足：

• 每个内层集合包含若干配对(s, v)，其中s ∈ S且v ∈ s
• 每个内层集合恰好包含S中每个集合对应的一个配对

示例代码：

definition s1 :: "nat set" where 
  "s1 = {1, 2}"
definition s2 :: "nat set" where
  "s2 = {4, 5}"
definition S :: "nat set set" where 
  "S = {s1, s2}"

value "{{(s, v) | s. s ∈ S} | v. v ∈ s}"

期望输出：

{{({1, 2}, 1), ({4, 5}, 4)}, {({1, 2}, 1), ({4, 5}, 5)}, {({1, 2}, 2), ({4, 5}, 4)}, {({1, 2}, 2), ({4, 5}, 5)}}

实际得到错误结果：

"(λu. {({1, 2}, u), ({4, 5}, u)}) ` s"
  :: "(nat set × 'a) set set"

核心问题：无法为每个配对中的v绑定到其所属的集合s ∈ S，导致所有配对共用同一个v。

解决方案 #

你的写法逻辑错误在于外层推导试图用单一变量v对应所有s ∈ S，正确思路是构造函数集合：每个函数f为每个s ∈ S分配一个属于s的元素，再将函数转换为对应的配对集合。

通用实现方式 #

对于任意有限集合S，使用函数空间Π s ∈ S. s来表示所有合法的选择函数，再将每个函数映射为配对集合：

value "{{(s, f s) | s ∈ S} | f. f ∈ (Π s ∈ S. s)}"

针对固定大小S的直观写法 #

如果S的元素数量固定（比如示例中的2个集合），可以直接展开笛卡尔积逻辑：

value "{{(s1, v1), (s2, v2)} | v1 ∈ s1, v2 ∈ s2}"

逻辑解释 #

• Π s ∈ S. s是Isabelle中表示依赖笛卡尔积的函数空间，每个成员f都是满足∀s∈S. f s ∈ s的函数，正好对应从每个s ∈ S中选一个元素的操作
• 外层集合推导遍历每个这样的函数f，将其转换为{(s, f s) | s ∈ S}，每个转换结果就是你需要的内层集合——包含每个s ∈ S与其对应选中元素的配对。

运行上述通用实现代码，就能得到你期望的输出结果。

内容的提问来源于stack exchange，提问作者Alicia M.