algorithm - 可证明正确的排列小于 O(n^2)

Question

用 Haskell 编写，这是证明一个列表是另一个列表的排列的数据类型:

data Belongs (x :: k) (ys :: [k]) (zs :: [k]) where
  BelongsHere :: Belongs x xs (x ': xs)
  BelongsThere :: Belongs x xs xys -> Belongs x (y ': xs) (y ': xys)

data Permutation (xs :: [k]) (ys :: [k]) where
  PermutationEmpty :: Permutation '[] '[]
  PermutationCons :: Belongs x ys xys -> Permutation xs ys -> Permutation (x ': xs) xys

有了Permutation，我们现在可以排列记录:

data Rec :: (u -> *) -> [u] -> * where
  RNil :: Rec f '[]
  (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)

insertRecord :: Belongs x ys zs -> f x -> Rec f ys -> Rec f zs
insertRecord BelongsHere v rs = v :& rs
insertRecord (BelongsThere b) v (r :& rs) = r :& insertRecord b v rs

permute :: Permutation xs ys -> Rec f xs -> Rec f ys
permute PermutationEmpty RNil = RNil
permute (PermutationCons b pnext) (r :& rs) = insertRecord b r (permute pnext rs)

这很好用。但是，置换是 O(n^2)，其中 n 是记录的长度。我想知道是否有一种方法可以通过使用不同的数据类型来表示排列来使其更快。

为了比较，在可变和无类型的设置中(我知道这确实是一个非常不同的设置)，我们可以在 O(n) 中对这样的异构记录应用排列 时间。您将记录表示为值数组，将排列表示为新位置数组(不允许重复，所有数字必须介于 0 和 n 之间)。应用排列只是迭代该数组并使用这些位置索引到记录的数组中。

我不认为 O(n) 排列在更严格类型的设置中是可能的。但似乎 O(n*log(n)) 是可能的。我感谢任何反馈，如果我需要澄清任何事情，请告诉我。此外，这个问题的答案可以使用 Haskell、Agda 或 Idris，具体取决于感觉更容易交流的内容。

Answer 1

一个更快的简单解决方案是比较排列的排序排列。

1. 给定排列 A 和 B。

2. 然后存在排序的排列，

   作为 = 排序(A) Bs = 排序(B)

3. As 是 A 的排列，Bs 是 B 的排列。

4. 如果 As == Bs 则 A 是 B 的排列。

因此这个算法的阶数是 O(n log(n)) < O(n²)

这导致了最优解。

使用不同的排列存储方式产生 O(n)

使用上面的语句，我们将每个排列的存储格式更改为

• 排序后的数据
• 原始未排序数据

要确定一个列表是否是另一个列表的排列，需要对排序后的数据进行简单的比较 -> O(n)。

这正确地回答了问题，但是在创建双倍数据存储中隐藏了努力^^所以这是否是一个真正的优势将取决于使用。