功能语言中的等价类和联合/查找

Question

对于自动机算法，我需要函数式语言中的快速 Union-Find 数据结构。由于需要形式化证明数据结构的正确性，所以我更喜欢简单的结构。

我要做的是计算集合S w.r.t 中元素的等价类。关系R ⊆ S × S。我最终想要得到的是一些函数f: S → S，它将S 的任何元素映射到其R-equivalence 类的（规范）代表。通过“规范”，我的意思是我不在乎它是哪个代表，只要它对于一个等价类的所有元素都是相同的，即我希望 f x = f y ⟺ (x,y) ∈ R 保持不变。

函数式语言中最好的数据结构和算法是什么？我应该补充一点，我真的需要“正常”的功能代码，即没有可变性/状态转换器单子。

编辑：与此同时，我想出了这个算法：

m := empty map
for each s ∈ S do
  if m s = None then
    for each t in {t | (s,t) ∈ R}
      m := m[t ↦ s]

这将创建一个映射，将S 的任何元素映射到其等价类的代表，其中代表是通过S 的迭代到达的第一个元素。我认为这实际上具有线性时间（如果地图操作是恒定的）。但是，我仍然对其他解决方案感兴趣，因为我不知道这在实践中的效率如何。

（我的关系在内部表示为“S → (S Set) option”，因此在 {t | (s,t) ∈ R} 上的迭代 - 这是对该结构的廉价操作。）

Answer 1

AFAIK（快速搜索并没有让我感到厌烦），没有已知的与传统 disjoint-set datastructure 等效的纯函数等效项，它具有可比的渐近性能（摊销逆阿克曼函数）。 （传统的数据结构不是纯功能的，因为它需要破坏性更新来执行路径压缩）

如果您对功能纯度没有死心，您可以使用破坏性更新，并实现常规数据结构。

如果您不关心匹配渐近性能，您可以用persistent associative map 替换常规数据结构的随机访问数组，代价是额外的 O(log N) 性能因子，并且需要验证它的正确性。

如果您希望最大程度地简化验证，并且不拘泥于上述任何一项，您可以使用可更新数组并放弃按等级联合优化。 IIRC 这会产生 O(log N) 摊销的最坏情况性能，但实际上可能会提高实际执行速度（因为不再需要存储或管理排名）。