OpenMath

OpenMath is an extensible standard for representing the semantics of mathematical objects.

https://openmath.org

OpenMath Content Dictionary: permutation1

Canonical URL:
http://www.win.tue.nl/~amc/oz/om/cds/permutation1.ocd
CD File:
permutation1.ocd
CD as XML Encoded OpenMath:
permutation1.omcd
Defines:
action, are_distinct, cycle, cycle_type, cycles, domain, endomap, endomap_left_compose, endomap_right_compose, fix, inverse, is_bijective, is_endomap, is_list_perm, is_permutation, left_compose, length, list_perm, listendomap, order, permutation, permutationsn, right_compose, sign, support
Date:
2004-06-01
Version:
1 (Revision 7)
Review Date:
2006-06-01
Status:
experimental

This CD defines permutations with finite support.

In order to make available permutations of arbitrary objects, permutations are defined as sets of cycles.

The set on which the permutation acts is not specified. To this end, cycles of length 0 or 1 do not occur in permutations.

When viewed as the set of cycles which are its arguments, the symbol permutation has a normal form constructor.

All symbols defined in this CD may appear as the head of an application. For such symbols, we distinguish between functions and constructors. A function is thought of as a mathematical function, which can be evaluated on its arguments, a constructor uses its arguments as fields of a structure. (In principle, the arguments of a constructor should be accessible; we have not introduced separate symbols to enable access because the `destruction' of the mathematical object can take place in phrasebooks.)

The constructors in this CD are cycle, permutation, list_perm, and endomap.

The operations inverse, left_compose, right_compose are also defined in this CD, although the most general purpose version already occurs in fns1, fns2. The reasons is two-fold: first, strictly speaking, our permutations are not maps, and so these notions havfe to redefined. A more practical reason is that with dynamical loading, it is easier to encode and decode a new symbol in the CD at hand rather than a symbol in a CD that is previously dealt with.

Revision 0.1: fix added; error in support example corrected. Revision 0.2: added endomap. Help of Henny Wilbrink.

endomap

Description:

This symbol is an n-ary constructor. Its arguments should be positive integers. When applied to arguments a_1,...,a_n, the resulting value is the map sending i to a_i for i=1,...,n.

Example:
The following expression represents the map on on {1,2,3,4,5} sending 1, 2, and 5 to 2, and 3 and 4 to 1.
endomap ⁡ ( 2 , 2 , 1 , 1 , 2 )
Example:
The following expression evaluates to true.
( endomap ⁡ ( 5 , 1 , 3 , 2 , 4 ) ) ⁡ ( 4 ) = 2
Signatures:
sts

[Next: list_perm] [Last: permutationsn] [Top]

list_perm

Description:

This symbol is an n-ary constructor. Its arguments should be distinct positive integers in the interval [1,n]. When applied to arguments a_1,...,a_n, the resulting value is the permutation mapping i to a_i for i=1,...,n.

Example:
The following two expressions represent the same permutation of {1,2,3,4,5}.
list_perm ⁡ ( 2 , 3 , 1 , 5 , 4 )
permutation ⁡ ( cycle ⁡ ( 1 , 2 , 3 ) , cycle ⁡ ( 4 , 5 ) )
Example:
The following expression evaluates to true.
( list_perm ⁡ ( 5 , 1 , 3 , 2 , 4 ) ) ⁡ ( 4 ) = 2
Signatures:
sts

[Next: is_endomap] [Previous: endomap] [Top]

is_endomap

Description:

This symbol is an n-ary function. Its arguments should be positive integers. When applied to arguments a_1,...,a_n, the resulting value is true if a_i is at most n for all i, otherwise it is false.

Example:
The following expression evaluates to true
is_endomap ⁡ ( 1 , 3 , 1 )
Example:
The following expression evaluates to false
is_endomap ⁡ ( 2 , 3 , 5 )
Signatures:
sts

[Next: is_list_perm] [Previous: list_perm] [Top]

is_list_perm

Description:

This symbol is an n-ary function. Its arguments should be positive integers. When applied to arguments a_1,...,a_n, the resulting value is true if a_i is at most n for all i and all a_i are distinct, otherwise it is false.

Example:
The following expression evaluates to false
is_list_perm ⁡ ( 1 , 3 , 1 )
Example:
The following expression evaluates to false
is_list_perm ⁡ ( 2 , 3 , 5 )
Example:
The following expression evaluates to true
is_list_perm ⁡ ( 2 , 3 , 1 )
Signatures:
sts

[Next: domain] [Previous: is_endomap] [Top]

domain

Description:

This symbol is a function with one argument which is a endomap. When applied to a endomap whose arguments are a_1,...,a_n, it represents the set {1,...,n}.

Example:
The following expression represents the set {1,2,3,4,5}.
domain ⁡ ( endomap ⁡ ( 4 , 3 , 5 , 5 , 5 ) )
Signatures:
sts

[Next: is_bijective] [Previous: is_list_perm] [Top]

is_bijective

Description:

This symbol has one argument which should be a endomap p. It returns true if {a_1,...,a_n}={1,...,n} where a_1,...a_n are the arguments of p and false otherwise.

Example:
The following expression evaluates to true.
is_bijective ⁡ ( endomap ⁡ ( 1 , 3 , 2 ) )
Example:
The following expression evaluates to false.
is_bijective ⁡ ( endomap ⁡ ( 2 , 3 , 5 ) )
Signatures:
sts

[Next: endomap_left_compose] [Previous: domain] [Top]

endomap_left_compose

Description:

This symbol is a binary function. Its arguments should be endomaps with identical domain D. When applied to arguments P1 and P2, the resulting value is the endomap which maps x in D to P1(P2(x)).

Signatures:
sts

[Next: endomap_right_compose] [Previous: is_bijective] [Top]

endomap_right_compose

Description:

This symbol is a binary function. Its arguments should be endomaps with identical domain D. When applied to arguments P1 and P2, the resulting value is the endomap which maps x in D to P2(P1(x)).

Signatures:
sts

[Next: cycle] [Previous: endomap_left_compose] [Top]

cycle

Description:

This symbol is an n-ary constructor. It marks a relation on the set of its arguments a_1, a_2,...,a_n consisting of the pairs (a_i,a_{i+1}) for i=1,...,n-1 and the pair (a_n,a_1). The arguments a_i should all be distinct. The number n is referred to as the length of the cycle.

Commented Mathematical property (CMP):
for i = 1,..., n cycle(a_i, a_{i+1},...,a_n,a_1,...,a_{i-1}) = cycle(a_1, a_2,...,a_n).
Example:
The following expression represents the relation on the set {"jan","piet","klaas"} whose members are ("jan","piet"), ("piet","klaas"), and ("klaas","jan").
cycle ⁡ ( jan , piet , klaas )
Signatures:
sts

[Next: length] [Previous: endomap_right_compose] [Top]

length

Description:

This symbol is a function with one argument, which must be a cycle. When applied to cycle(a_1,a_2,...,a_n), it returns the number n. This number is referred to as the length of the cycle.

Example:
The following expression should evaluate to 3.
length ⁡ ( cycle ⁡ ( 2 , 4 , 3 ) )
Signatures:
sts

[Next: permutation] [Previous: cycle] [Top]

permutation

Description:

This symbol is an n-ary constructor whose arguments are cycles of length at least 2 with the property that all entries of all cycles are mutually distinct. The permutation symbol constructs a bijective map from the set X of entries of the cycles to X. The map is defined as follows: if E occurs as an entry of a cycle, then the permutation maps E to the entry following E in the same cycle if it exists and to the first entry in the same cycle otherwise.

When applied to an element y outside X, the constructed permutation is considered to fix y.

Commented Mathematical property (CMP):
For valid arguments A and B both left_compose and right compose of permutation(A) and permutation(B) are permutations again (that is, evaluate to permutation(C) and permutation(D), respectively, for suitable C and D).
Commented Mathematical property (CMP):
For a valid argument A the inverse of permutation(A) is a permutation again (that is, evaluates to permutation(C) for suitable argument C).
Commented Mathematical property (CMP):
permutation() is the identity.
Formal Mathematical property (FMP):
permutation ⁡ ( ) = Id
Example:
The permutation (1,5,4)(6,7) sending 1 to 5, 5 to 4, 4 to 1, 6 to 7, 7 to 6, is given by
permutation ⁡ ( cycle ⁡ ( 1 , 5 , 4 ) , cycle ⁡ ( 6 , 7 ) )
Signatures:
sts

[Next: is_permutation] [Previous: length] [Top]

is_permutation

Description:

This symbol is a boolean function with one argument. If the argument is not a set of cycles of length at least 2, the boolean value is false. Otherwise it is true if and only if the cycles are disjoint (that is, all entries of all cycles in the argument are mutually distinct.

Commented Mathematical property (CMP):
If is_permutation(A) is true then permutation(A) is well defined.
Example:
The following value is the boolean false
is_permutation ⁡ ( { cycle ⁡ ( 5 , 4 , 4 , 2 , 1 ) } )
whereas the following value is true
is_permutation ⁡ ( { cycle ⁡ ( 5 , 4 , 3 , 2 , 1 ) } )
Signatures:
sts

[Next: support] [Previous: permutation] [Top]

support

Description:

This symbol is a function with one argument which is a permutation. When applied to a permutation whose arguments are the cycles A1,...,An, it represents the set A which is the union of the entries of all Ai for i=1,...,n.

Example:
The following expression represents the set {jan,piet,klaas,3,4,5}.
support ⁡ ( permutation ⁡ ( cycle ⁡ ( jan , 4 , klaas ) , cycle ⁡ ( 3 , klaas ) , cycle ⁡ ( piet , 5 ) ) )
Signatures:
sts

[Next: fix] [Previous: is_permutation] [Top]

fix

Description:

This symbol is a function with two arguments. The first argument should be a permutation, the second argument a set. When applied to a permutation g and a set X, it represents the subset A of X all points that do not belong to the support of g.

Example:
The following expression represents the set {1,2}.
support ⁡ ( permutation ⁡ ( cycle ⁡ ( jan , 4 , klaas ) , cycle ⁡ ( 3 , klaas ) , cycle ⁡ ( piet , 5 ) ) , { [ 1 , 5 ] } )
Signatures:
sts

[Next: cycles] [Previous: support] [Top]

cycles

Description:

This symbol has one argument which should be a endomap p. It returns the list of cycles of p.

Example:
The following two objects represent the same list.
cycles ⁡ ( endomap ⁡ ( 2 , 3 , 4 , 2 , 5 ) )
( cycle ⁡ ( 2 , 3 , 4 ) )
Signatures:
sts

[Next: listendomap] [Previous: fix] [Top]

listendomap

Description:

This symbol is a function with one argument which is a permutation whose support consists of positive integers. When applied to such a permutation P, it represents the list of length n whose i-th entry is the image of i under P, where n is the maximum of the support of P.

Example:
The following two expressions represent the same list.
listendomap ⁡ ( permutation ⁡ ( cycle ⁡ ( 1 , 4 ) ) )
( 4 , 2 , 3 , 1 )
Signatures:
sts

[Next: cycle_type] [Previous: cycles] [Top]

cycle_type

Description:

This symbol is a function with one argument, which is a permutation. When applied to a permutation P, it represents the multiset of lengths of cycles occurring as arguments of P.

Formal Mathematical property (FMP):
∀   P , Q . is_permutation ⁡ ( P ) ∧ is_permutation ⁡ ( Q ) ⇒ cycle_type ⁡ ( apply_to_list ⁡ ( left_compose , ( Q , P , Q -1 ) ) ) = cycle_type ⁡ ( P )
Example:
The cycle type of the permutation (4,3,2,1)(5,6)("jan","piet") equals {4,2,2}:
cycle_type ⁡ ( permutation ⁡ ( cycle ⁡ ( 4 , 3 , 2 , 1 ) , cycle ⁡ ( 5 , 6 ) , cycle ⁡ ( jan , piet ) ) ) = multiset ⁡ ( 4 , 2 , 2 )
Signatures:
sts

[Next: order] [Previous: listendomap] [Top]

order

Description:

This symbol is a function with one argument which should be a permutation. When applied to a permutation P, it represents the least positive integer n for which composition of n copies of P represents the identity (that is, a permutation with empty support). Note: in this definition of the order, it does not matter whether left_compose or right_compose is being used.

Commented Mathematical property (CMP):
The order of a permutation is the least common multiple of the elements of its cycle type.
Formal Mathematical property (FMP):
∀   P . is_permutation ⁡ ( P ) ⇒ order ⁡ ( P ) = apply_to_list ⁡ ( lcm , cycle_type ⁡ ( P ) )
Example:
The order of the permutation (4,3,2,1)(5,6)("jan","piet") equals 4:
order ⁡ ( permutation ⁡ ( cycle ⁡ ( 4 , 3 , 2 , 1 ) , cycle ⁡ ( 5 , 6 ) , cycle ⁡ ( jan , piet ) ) ) = 4
Signatures:
sts

[Next: are_distinct] [Previous: cycle_type] [Top]

are_distinct

Description:

This symbol is an n-ary boolean function. When applied to a_1, ..., a_n, it is true if and only if the arguments are mutually distinct (that is, a_i and a_j are equal only if i=j).

Commented Mathematical property (CMP):
If are_distinct(a_1,...,a_n) is true then a_1,...,a_n is a valid argument sequence of cycle.
Example:
The following expression evaluates to false.
are_distinct ⁡ ( 1 , 3 , 2 , 3 )
Signatures:
sts

[Next: sign] [Previous: order] [Top]

sign

Description:

This symbol is a function with one argument which should be a permutation. When applied to a permutation P, it represents the sign of P, which is equal to -1 if P is an odd permutation and equal to 1 otherwise.

Commented Mathematical property (CMP):
If the cycle type of a permutation P equals [a_1,...,a_m], then the sign is equal to (-1)^(s-m) where s = a_1+...+a_m.
Formal Mathematical property (FMP):
∀   P . sign ⁡ ( permutation ⁡ ( P ) ) = -1 apply_to_list ⁡ ( list ⁡ ( x + 1 | x ∈ ) + cycle_type ⁡ ( permutation ⁡ ( P ) ) )
Example:
The sign of the permutation (4,3,2,1)(5,6)("jan","piet") equals -1:
sign ⁡ ( permutation ⁡ ( cycle ⁡ ( 4 , 3 , 2 , 1 ) , cycle ⁡ ( 5 , 6 ) , cycle ⁡ ( jan , piet ) ) ) = -1
Signatures:
sts

[Next: inverse] [Previous: are_distinct] [Top]

inverse

Description:

This symbol is a unary function. Its argument should be a permutation. When applied to argument P, the resulting value is the inverse permutation of P.

Example:
The following two expressions represent the same permutation of {1,2,3,4,5}.
permutation ⁡ ( cycle ⁡ ( 1 , 3 , 2 ) , cycle ⁡ ( 4 , 5 ) ) -1
permutation ⁡ ( cycle ⁡ ( 1 , 2 , 3 ) , cycle ⁡ ( 4 , 5 ) )
Signatures:
sts

[Next: left_compose] [Previous: sign] [Top]

left_compose

Description:

This symbol is a binary function. Its arguments should be permutations. When applied to arguments P1 and P2, the resulting value is the permutation which maps x in Support(P1) union Support(P2) to P1(P2(x)).

Example:
Left and right composition of two permutations may lead to distinct results:
left_compose ⁡ ( permutation ⁡ ( cycle ⁡ ( 1 , 2 ) ) , permutation ⁡ ( cycle ⁡ ( 1 , 2 , 3 ) ) ) = permutation ⁡ ( cycle ⁡ ( 2 , 3 ) )
Signatures:
sts

[Next: right_compose] [Previous: inverse] [Top]

right_compose

Description:

This symbol is a binary function. Its arguments should be permutations. When applied to arguments P1 and P2, the resulting value is the permutation which maps x in Support(P1) union Support(P2) to P2(P1(x)).

Example:
Left and right composition of two permutations may lead to distinct results. Compare the following with the corresponding example in the definition of left_compose.
right_compose ⁡ ( permutation ⁡ ( cycle ⁡ ( 1 , 2 ) ) , permutation ⁡ ( cycle ⁡ ( 1 , 2 , 3 ) ) ) = permutation ⁡ ( cycle ⁡ ( 1 , 3 ) )
Signatures:
sts

[Next: action] [Previous: left_compose] [Top]

action

Description:

This symbols is a binary function whose first argument is a permutation (or a endomap) and whose second argument is a point. When applied to permutation or endomap p and point x, it represents the image of the point x under the permutation p.

Example:
The permutation (1,5,4)(6,7) sends 1 to 5, so
action ⁡ ( permutation ⁡ ( cycle ⁡ ( 1 , 5 , 4 ) , cycle ⁡ ( 6 , 7 ) ) , 1 ) = 5
Signatures:
sts

[Next: permutationsn] [Previous: right_compose] [Top]

permutationsn

Description:

This symbol is a unary function. Its argument should be a positive integer. When applied to argument n, the resulting value is the set of all permutations of the set {1,..., n}.

Example:
Both sides of the following equality represent the two permutations on {1,2}.
permutationsn ⁡ ( 2 ) = { permutation ⁡ ( ) , permutation ⁡ ( cycle ⁡ ( 1 , 2 ) ) }
Signatures:
sts

[First: endomap] [Previous: action] [Top]