permutation of a totally ordered index type i which yield a bijection pmt on i. They are constructed using

• make of a valid PermutationForm, which defines also the validity for the constructed permutation.
• swap and the Multiplicative structure for permutations.
• permuteBy for PermutableSequence.
• xPermutation to generate randomly permutations.

In the following the total right operation <* of a permutation on several types of sequences will be defined to achieve the permutation of there items.

Definitions

List

Let xs be in [x] with ConstructableSequence [] r [x] and p a permutation in Permutation r, then xs <* p is given by sqcIndexMap is (pmt p) xs, where is is the image of the support of xs under the inverse of p.

CSequence

Let xs be in CSequence x with ConstructableSequence CSequence N x and p a permutation in Permutation N, then xs <* p is given by sqcIndexMap is (pmt p) xs, where is is the image of the support of xs under the inverse of p.

PSequence

Let xs be in PSequence i x with ConstructableSequence (PSequence i) i x and p a permutation in Permutation i, then xs <* p is given by sqcIndexMap is (pmt p) xs, where is is the image of the support of xs under the inverse of p.

Permutation

Let xs, p be in Permutation i, then xs <* p is given by *.

Note The given definitions are not very efficient and only terminate for finite sequences (in fact, a more efficient implementation has been chosen that also terminates for infinite sequences (see example below)). However, they serve on the one hand to define the semantic and to 'prove' the properties for TotalOpr and on the other hand to verify the chosen implementation for finite sequences (see prpOprPermutation).

Examples

>>> "abcdef" <* (swap 2 5 :: Permutation N)
"abfdec"

the support of a sequence and the relevant image of a permutation may be disjoint which will leave the sequence untouched

>>> "abcdef" <* (swap 7 10 :: Permutation N)
"abcdef"

the intersection of the support of a sequence with the relevant image of a permutation may be a non empty proper sub set

>>> "abcdef" <* swap 2 10 :: Permutation N)
"abdefc"

the result can be interpreted as: first, put c at position 10 and Nothing (which is the item at position 10) at position 2. Second, strip all nothings form it.

Although the given definition of the permutation of sequences dose not terminate for infinite sequences, its implementation will terminate

>>> takeN 5 $ (([0..] :: [N]) <* (swap 1 2 :: Permutation N)
[0,2,1,3,4]

the bijection on i for a given permutation and is defined via restrict pmf.

swapping.

Property Let p = swap n (i,j), then holds: If i,j < n then p is the permutation given by swapping i with j, otherwise a exception will be thrown.

total right operations of permutations on sequences, admitting the following properties:

Property Let s, i, x be an instance of PermutableSequence s i x, then holds:

1. Let xs be in s x, p in Permutation i with image z p <<= support z xs for some z in z i, then holds: (xs <* p) ?? i == ((xs ??) . pmt p) i for all i in support z xs.

2. Let xs be in s x, w in x -> w, c in w -> w -> Ordering and z in z i, then holds: Let (xs',p) = permuteBy z c w xs in

   1. xs' == xs <* p.
   2. xs' is ordered according to c by applying w to its items.
   3. image z p <<= support z xs.

Examples

>>> fst $ permuteBy nProxy compare isUpper "abCd1eFgH"
"abd1egCFH"

as False < True

>>> fst $ permuteBy nProxy (coCompare compare) isUpper "abCd1eFgH"
"CFHabd1eg"

which orders it in the reverse ordering.

orders the permutable sequence according to the given ordering an delivers the resulting permutation form.

form of a permutation from i to i which is given by pmf.

Property Let p = PermutationForm jis be in PermutationForm i, then holds: support z p == image z p for some proxy z in z i.

The partial sequence ijs is called the relevant part of p.

the associated function i to i and is given by:

Definition Let p = PermutationForm jis be in PermutationForm i then pmf p i is defined by: If there exists an (j,i') in psqxs jis with i' == i then pmf p i = j else pmf p i = i.

Note

1. If the partial sequence ijs is valid, then for all i in i there exists at most one (_,i') in psqxs jis such that i' == i. As such, the function pmf p is well defined.
2. If the permutation form p itself is valid than pmf p is a bijection and as such a permutation of i.
3. The behavior of pmf differs from ?? as its evaluation will not end up in a IndexOutOfSupport-exception.

random variable of permutations.

random variable of permutations within the given bounds.

random variable of permutations of the index set [0..prd n].

random variable for validating the Multiplicative structure.

validity of the functionality of the module Permutation.

validity for PermutableSequence.

validity of the total right operation <* of permutations on sequences.