Safe Haskell | None |
---|---|
Language | Haskell98 |
Agda.Utils.Permutation
- data Permutation = Perm {}
- permute :: Permutation -> [a] -> [a]
- idP :: Int -> Permutation
- takeP :: Int -> Permutation -> Permutation
- droppedP :: Permutation -> Permutation
- liftP :: Int -> Permutation -> Permutation
- composeP :: Permutation -> Permutation -> Permutation
- invertP :: Permutation -> Permutation
- compactP :: Permutation -> Permutation
- reverseP :: Permutation -> Permutation
- expandP :: Int -> Int -> Permutation -> Permutation
- topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation
- data Drop a = Drop {}
- class DoDrop a where
Documentation
data Permutation
Partial permutations. Examples:
permute [1,2,0] [x0,x1,x2] = [x1,x2,x0]
(proper permutation).
permute [1,0] [x0,x1,x2] = [x1,x0]
(partial permuation).
permute [1,0,1,2] [x0,x1,x2] = [x1,x0,x1,x2]
(not a permutation because not invertible).
Agda typing would be:
Perm : {m : Nat}(n : Nat) -> Vec (Fin n) m -> Permutation
m
is the size
of the permutation.
permute :: Permutation -> [a] -> [a]
permute [1,2,0] [x0,x1,x2] = [x1,x2,x0]
More precisely, permute indices list = sublist
, generates sublist
from list
by picking the elements of list as indicated by indices
.
permute [1,3,0] [x0,x1,x2,x3] = [x1,x3,x0]
Agda typing:
permute (Perm {m} n is) : Vec A m -> Vec A n
idP :: Int -> Permutation
Identity permutation.
takeP :: Int -> Permutation -> Permutation
Restrict a permutation to work on n
elements, discarding picks >=n
.
droppedP :: Permutation -> Permutation
Pick the elements that are not picked by the permutation.
liftP :: Int -> Permutation -> Permutation
liftP k
takes a Perm {m} n
to a Perm {m+k} (n+k)
.
Analogous to liftS
,
but Permutations operate on de Bruijn LEVELS, not indices.
composeP :: Permutation -> Permutation -> Permutation
permute (compose p1 p2) == permute p1 . permute p2
invertP :: Permutation -> Permutation
compactP :: Permutation -> Permutation
Turn a possible non-surjective permutation into a surjective permutation.
reverseP :: Permutation -> Permutation
permute (reverseP p) xs == reverse $ permute p $ reverse xs
Example:
permute (reverseP (Perm 4 [1,3,0])) [x0,x1,x2,x3]
== permute (Perm 4 $ map (3-) [0,3,1]) [x0,x1,x2,x3]
== permute (Perm 4 [3,0,2]) [x0,x1,x2,x3]
== [x3,x0,x2]
== reverse [x2,x0,x3]
== reverse $ permute (Perm 4 [1,3,0]) [x3,x2,x1,x0]
== reverse $ permute (Perm 4 [1,3,0]) $ reverse [x0,x1,x2,x3]
expandP :: Int -> Int -> Permutation -> Permutation
expandP i n π
in the domain of π
replace the ith element by n elements.
topoSort :: (a -> a -> Bool) -> [a] -> Maybe Permutation
Stable topologic sort. The first argument decides whether its first argument is an immediate parent to its second argument.
Drop (apply) and undrop (abstract)
class DoDrop a where
Things that support delayed dropping.
Minimal complete definition
Methods
Arguments
:: Drop a | |
-> a | Perform the dropping. |
Instances
DoDrop Permutation | |
DoDrop [a] |