data-structures - 如何在 Coq 中实现联合查找(不相交集)数据结构？

Question

我是 Coq 的新手，但对于我的项目，我必须在 Coq 中使用联合查找数据结构。 Coq 中是否有 union-find(不相交集)数据结构的实现？

如果没有，有人可以提供实现或一些想法吗？它不必非常有效。 (不需要进行路径压缩或所有花哨的优化)我只需要一个可以容纳任意数据类型的数据结构(或者 nat 如果它太难了)并执行:union 和找到。

提前致谢

Answer 1

如果您只需要一个数学模型，而不关心实际性能，我会选择最直接的模型:函数映射(有限偏函数)，其中每个元素都可以选择链接到另一个元素合并。

• 如果一个元素链接到任何东西，那么它的规范代表就是它自己。
• 如果一个元素链接到另一个元素，则其规范代表就是该其他元素的规范代表。

注意:在这个答案的其余部分，作为 union-find 的标准，我将假设元素只是自然数。如果您想要其他类型的元素，只需使用另一个将所有元​​素绑定(bind)到唯一编号的映射即可。

然后您将定义一个函数 find : UnionFind → nat → nat 返回给定元素的规范代表，尽可能长时间地跟踪链接。请注意，该函数将使用递归，其终止参数并非微不足道。要做到这一点，我认为最简单的方法是保持一个数字只链接到一个较小的数字的不变性(即如果 i 链接到 j，那么 i > j).然后递归终止，因为当跟随链接时，当前元素是递减的自然数。

定义函数 union : UnionFind → nat → nat → UnionFind 更简单:union m i j 简单地返回一个更新后的映射 max i' j' 链接到 min i' j'，其中 i' = find m i 和 j' = find m j。

[关于性能的旁注:保持不变量意味着您不能根据它们的等级充分选择一对分区中的哪一个合并到另一个；但是，如果需要，您仍然可以实现路径压缩!]

至于 map 究竟使用哪种数据结构:有几种可用。standard library (查看标题 FSets)有几个实现(FMapList、FMapPositive 等)满足接口(interface) FMapInterface .stdpp 库有 gmap .

同样，如果性能不是问题，只需选择最简单的编码，或者更重要的是，选择使您的证明最简单的编码。我想的只是一个自然数列表。列表的位置是倒序的元素。列表的值是偏移量，即为了到达链接的目标而向前跳过的位置数。

• 对于链接到 j 的元素 i (i > j)，偏移量是 i − j .
• 对于规范代表，偏移量为零。

凭借我最好的伪 ASCII 艺术技能，这是一张 map ，其中链接为 { 6↦2, 4↦2, 3↦0, 2↦1 }，规范代表为 { 5, 1, 0 } :

  6   5   4   3   2   1   0   element
  ↓   ↓   ↓   ↓   ↓   ↓   ↓
               /‾‾‾‾‾‾‾‾‾↘
[ 4 ; 0 ; 2 ; 3 ; 1 ; 0 ; 0 ] map
   \       \____↗↗ \_↗
    \___________/

动机是上面讨论的不变量然后在结构上被强制执行。因此，希望 find 实际上可以通过结构归纳(在列表的结构上)来定义，并且可以免费终止。

---

相关论文是:Sylvain Conchon and Jean-Christophe Filliâtre. A Persistent Union-Find Data Structure. In ACM SIGPLAN Workshop on ML.

它描述了 ML 中高效联合查找数据结构的实现，从用户的角度来看是持久的，但在内部使用变异。你可能更感兴趣的是，他们在 Coq 中证明了它是正确的，这意味着他们有一个联合查找的 Coq 模型。然而，这个模型反射(reflect)了他们试图证明正确的命令式程序的内存存储。我不确定它是否适用于您的问题。