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

Question

对于自动机算法,我需要一种功能语言的快速Union-Find数据结构.由于我需要正式证明数据结构的正确性,我宁愿选择一个简单的结构.

我想要做的是计算一组S关系中元素的等价类R ? S × S.我想最终得到的是一些函数f: S ? S,它将任何元素映射S到其R等价类的(规范)代表.通过"规范",我的意思是我不关心它是什么代表,只要它对于一个等价类的所有元素都是相同的,即我想要f x = f y ? (x,y) ? R持有.

在函数式语言中,最好的数据结构和算法是什么？我应该补充一点,我真的需要"正常"的功能代码,即没有可变性/状态变换器monad.

编辑:与此同时,我提出了这个算法:

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)选项",因此迭代超过{t |(s,t)∈R} - 这是对该结构的廉价操作.)

Answer 1

AFAIK(以及快速搜索并没有使我失望),没有已知的纯函数等价的传统的不相交集数据结构具有可比较的渐近性能(摊销的逆阿克曼函数).(传统的数据结构不是纯粹的功能,因为它需要破坏性的更新来执行路径压缩)

如果您没有确定功能纯度,您可以使用破坏性更新,并实现传统的数据结构.

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

如果您希望最大限度地简化以进行验证,并且在上述任何一个方面都没有设置,则可以使用可更新数组并删除逐个级别的优化.IIRC产生O(log N)摊销的最坏情况性能,但实际上可以提高实际执行速度(因为不再需要存储或管理等级).