在小于O(n ^ 2)的情况下可以校正正确的排列

And*_*tin 17 algorithm haskell permutation agda dependent-type

写在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
Run Code Online (Sandbox Code Playgroud)

有了a 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)
Run Code Online (Sandbox Code Playgroud)

这很好用.但是,置换是O(n^2)这里n是记录的长度.我想知道是否有办法通过使用不同的数据类型来表示排列,使其更快.

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

我不认为O(n)在更严格的类型设置中可以进行排列.但似乎O(n*log(n))有可能.我感谢任何反馈,如果我需要澄清任何事情,请告诉我.此外,答案可以使用Haskell,Agda或Idris,具体取决于与之通信的感觉.

beb*_*bbo 3

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

\n\n
    \n
  1. 给定排列 A 和 B。

  2. \n
  3. 那么存在排序排列,

    \n\n

    As = 排序(A)\n Bs = 排序(B)

  4. \n
  5. As 是 A 的排列,Bs 是 B 的排列。

  6. \n
  7. 如果 As == Bs 则 A 是 B 的排列。

  8. \n
\n\n

因此该算法的阶数为 O(n log(n)) < O(n\xc2\xb2)

\n\n

这将导致最优解决方案。

\n\n

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

\n\n

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

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

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

\n\n

这正确地回答了问题,但是努力隐藏在创建双倍数据存储中 ^^ 因此,这是否是真正的优势将取决于使用情况。

\n