如何解决如何在 Coq 中实现联合查找不相交集数据结构？
我对 Coq 很陌生，但是对于我的项目，我必须在 Coq 中使用 union-find 数据结构。 Coq 中是否有联合查找（不相交集）数据结构的任何实现？
如果没有，有人可以提供实现或一些想法吗？它不必非常有效。 （无需进行路径压缩或所有花哨的优化）我只需要一个可以保存任意数据类型（如果太难，则为 nat）并执行的数据结构：union 和 查找。
提前致谢
解决方法
如果您只需要一个数学模型，而不考虑实际性能，我会选择最直接的一个：功能映射（有限偏函数），其中每个元素都可以选择链接到另一个元素合并。
- 如果一个元素没有链接，那么它的规范代表就是它自己。
- 如果一个元素链接到另一个元素，则其规范代表就是该其他元素的规范代表。
注意：在本答案的其余部分中，作为 union-find 的标准，我将假设元素只是自然数。如果您想要其他类型的元素，只需使用另一个映射将所有元素绑定到唯一编号即可。
然后您将定义一个函数 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 .
[关于性能的旁注：保持不变意味着你不能根据它们的等级充分选择一对分区中的哪一个合并到另一个；但是，如果您愿意，您仍然可以实现路径压缩！]
至于地图确切使用哪种数据结构：有几种可用。 standard library（查看标题FSets）有几个满足接口FMapInterface 的实现（FMapList、FMapPositive 等）。 stdpp 库有 gmap。
同样，如果性能不是问题，只需选择最简单的编码，或者更重要的是，选择使您的证明最简单的编码。我只想到一个自然数列表。 列表的位置是逆序的元素。 列表的值是偏移量，即为了到达链接的目标而向前跳过的位置数。
- 对于链接到
i(j) 的元素i > j，偏移量为i − j。 - 对于规范代表，偏移量为零。
以我最好的伪 ASCII 艺术技能，这里有一张地图，其中链接是 { 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 实际上可以通过结构归纳来定义（在列表的结构上），并且可以免费终止。
它描述了在 ML 中实现一个高效的 union-find 数据结构，从用户的角度来看是持久的，但在内部使用了变异。对你来说更有趣的是，他们在 Coq 中证明了它是正确的，这意味着他们有一个 Coq 模型用于联合查找。然而，这个模型反映了他们试图证明正确的命令式程序的内存存储。我不确定它是否适用于您的问题。
,Maëlan 有一个很好的答案，但对于更简单和效率更低的不相交集合数据结构，您可以使用函数来 nat 来表示它们。这避免了任何终止粘性。本质上，任何全函数的原像形成域上的不相交集。另一种看待这个的方式是将任何不相交集 G 表示为柯里化应用程序 find_root G : nat -> nat，因为 find_root 是不相交集提供的基本接口。
这也类似于在 Coq 中使用函数来表示 Maps，就像在 Software Foundations 中一样。 https://softwarefoundations.cis.upenn.edu/lf-current/Maps.html
Require Import Arith.
Search eq_nat_decide.
(* disjoint set *)
Definition ds := nat -> nat.
Definition init_ds : ds := fun x => x.
Definition find_root (g : ds) x := g x.
Definition in_same_set (g : ds) x y :=
eq_nat_decide (g x) (g y).
Definition union (g : ds) x y : ds :=
fun z =>
if in_same_set g x z
then find_root g y
else find_root g z.
你也可以像这样在不相交集合中的类型上使其泛型
Definition ds (a : Type) := a -> nat.
Definition find_root {a} (g : ds a) x := g x.
Definition in_same_set {a} (g : ds a) x y :=
eq_nat_decide (g x) (g y).
Definition union {a} (g : ds a) x y : ds a :=
fun z =>
if in_same_set g x z
then find_root g y
else find_root g z.
要为特定的 a 初始化不相交集，您基本上需要一个类型为 a 的 Enum 实例。
Definition init_bool_ds : ds bool := fun x => if x then 0 else 1.
根据您的证明风格和需要，您可能想用 eq_nat_decide 换取 eqb 或其他一些大致相当的东西。
版权声明：本文内容由互联网用户自发贡献，该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务，不拥有所有权，不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容， 请发送邮件至 dio@foxmail.com 举报，一经查实，本站将立刻删除。