11

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

我想要做的是计算一个集合中元素的等价S类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} 上的迭代 - 这是对该结构的廉价操作。）

4

1 回答 1

8

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

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

如果您不关心匹配渐近性能，您可以用持久关联映射替换传统数据结构的随机访问数组，但代价是额外的 O(log N) 性能因子，并且需要验证其正确性。

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

于 2013-03-28T21:46:38.597 回答