証明可能正しい順列Haskellで書かれた（N^2）

Question

、ここでは1つのリストは、別の順列であることを証明しているデータ型は次のとおりです。Permutationで

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 

、我々は並び替えるできるようになりましたレコード：

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) 

これは問題なく動作します。ただし、permuteはO(n^2)です。ここで、nはレコードの長さです。順列を表現するために別のデータ型を使用することで、それをもっと速くする方法があるのだろうかと思います。可変と型なしの設定では比較のために

、（私が知っている 確かに非常に異なる設定です）、私たちは O(n)時にこのような異種のレコードに並べ替えを適用することができます。レコードは値の配列として表現し、置換は新しい位置の配列として表します（重複は許されず、すべての数字は0とnの間でなければなりません）。順列を適用することは、その配列を繰り返し、それらの位置を持つレコードの配列にインデックスを付けることです。

より厳密に型指定された設定でO(n)の順列が可能であるとは思っていません。でも、O(n*log(n))のように見えるかもしれません。私はフィードバックを感謝し、私は何かを明確にする必要がある場合はお知らせください。また、これに対する答えは、コミュニケーションがより簡単に感じられることに応じて、Haskell、Agda、またはIdrisを使用することができます。

Answer 1

より簡単な解決策は、並べ替えられた順列の並べ替えを比較することです。

1. 考える順列AおよびB

2. よう次いでソート順列が

   よう=ソート（A） 旅館=ソート（B）

3. 、存在AおよびBsの順列はBの順列である。

4. もしAs == Bsならば、AはBの順列である。

したがって、このアルゴリズムの順序はO（N）（ログ）< O（n²）

あり、これは最適解につながるされます。順列の異なるストレージを使用

を上方からステートメントを使用してO（N）

をもたらす、我々は

• に各順列の格納形式を変更するソートされたデータ
• 元のソートされていないデータ

リストが別のものの置換であるかどうかを判断するには、単純ソートされたデータの比較が必要です - > O（n）。

これは質問に正しく答えていますが、倍精度データストレージを作成する際には努力が隠されています^^したがって、これが本当の利点であるかどうかは、使用に依存します。