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,具体取决于与之通信的感觉.
一个更快简单的解决方案是比较排列的排序排列。
\n\n给定排列 A 和 B。
那么存在排序排列,
\n\nAs = 排序(A)\n Bs = 排序(B)
As 是 A 的排列,Bs 是 B 的排列。
如果 As == Bs 则 A 是 B 的排列。
因此该算法的阶数为 O(n log(n)) < O(n\xc2\xb2)
\n\n这将导致最优解决方案。
\n\n使用不同的排列存储会产生 O(n)
\n\n使用上面的语句,我们将每个排列的存储格式更改为
\n\n要确定一个列表是否是另一个列表的排列,需要对排序数据进行简单比较 -> O(n)。
\n\n这正确地回答了问题,但是努力隐藏在创建双倍数据存储中 ^^ 因此,这是否是真正的优势将取决于使用情况。
\n| 归档时间: |
|
| 查看次数: |
909 次 |
| 最近记录: |