可證明正確的置換小於爲O（n^2）

寫在Haskell，這裏是證明了一個列表是另一個置換的數據類型：可證明正確的置換小於爲O（n^2）

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，具體取決於與之交流的感覺。

來源

2017-03-04 Andrew Thaddeus Martin

在cs.stackexchange.com上問你可能會更好一些 –

我不經常使用這樣的解除代碼，因此無法推理上述問題，但我想知道是否有情況下GHC能夠檢查但在編譯時不會完全評估所有內容。 – jberryman

也許我們需要一個O（1）相關數組'Array [k]'來實現這一點。無論如何，在一個完全依賴的系統中，你將能夠保持排列（作爲一個位置數組）並且證明它與兩個列表相關。要應用排列，可以使用您提到的簡單O（n）算法。也許人們可以用GADT，類型級別的nats和單身。 – chi

更簡單的解決方案是比較排列的排序排列。

鑑於置換A和B.
則存在已排序的置換，

正如=排序（A） BS =排序（B）
As是A和B的置換是B的置換。
如果As == Bs，那麼A是B的置換。

因此該算法的順序是O（n LOG（n））的< O（N²）

而這是導致最優解。

使用不同的存儲排列的產生爲O（n）

使用從上面的語句中，我們正在改變每個排列的存儲格式轉換成

排序的數據
的原始未排序數據

要確定列表是否是另一個列表的排列，排序數據的比較是必要的 - > O（n）。

這正確回答了問題，但是在創建雙倍數據存儲時隱藏了努力^^所以如果這是一個真正的優勢，它將取決於使用情況。

來源

2017-05-01 10:47:12 bebbo

可證明正確的置換小於爲O（n^2）

回答

相關問題