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:

are_distinct, cycle, cycle_type, is_perm, length, listperm, order, perm, permutation, sign, support

Date:

2002-10-21

Version:

1.3

Review Date:

2003-07-27

Status:

experimental

Uses CD:

arith1, fns1, fns2, list1, logic1, multiset1, nums1, quant1, relation1, set1

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.

cycle

Description:

This symbol is an n-ary function, with n at least 1. 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").

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
  <OMA> <OMS cd="permutation1" name="cycle"/>
        <OMSTR>jan</OMSTR>
	<OMSTR>piet</OMSTR>
	<OMSTR>klaas</OMSTR>
  </OMA>
</OMOBJ>

cycle ( "jan" , "piet" , "klaas" )

$$\mathrm{cycle}(\text{jan},\text{piet},\text{klaas})$$

Signatures:

sts

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.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">  <OMA><OMS cd="permutation1" name="length"/>
              <OMA><OMS cd="permutation1" name="cycle"/>
                   <OMI>2</OMI>	<OMI>4</OMI> <OMI>3</OMI>
              </OMA>
         </OMA>
  </OMOBJ>

length (cycle (2, 4, 3) )

$$\mathrm{length}\left(\mathrm{cycle}(2,4,3)\right)$$

Signatures:

sts

permutation

Description:

This symbols is an n-ary function 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.

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):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA><OMS cd="relation1" name="eq"/>
  <OMA><OMS cd="permutation1" name="permutation"/>
  </OMA>
  <OMS cd="fns1" name="identity"/>
</OMA>
</OMOBJ>

eq (permutation () , identity)

$$\mathrm{permutation}\left(\right)=\mathrm{Id}$$

Example:

The permutation (1,5,4,2)(6,7) sending 1 to 5, 5 to 4, 4 to 2, 2 to 1, 6 to 7, 7 to 6, is given by

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>	<OMS cd="permutation1" name="permutation"/>
					<OMA>	<OMS cd="permutation1" name="cycle"/>
						<OMI> 1 </OMI>
						<OMI> 5 </OMI>
						<OMI> 4 </OMI>
						<OMI> 2 </OMI>
					</OMA>
					<OMA>	<OMS cd="permutation1" name="cycle"/>
						<OMI> 6 </OMI>
						<OMI> 7 </OMI>
					</OMA>
				</OMA>
			</OMOBJ>

permutation (cycle ( 1 , 5 , 4 , 2 ) , cycle ( 6 , 7 ) )

$$\mathrm{permutation}(\mathrm{cycle}(1,5,4,2),\mathrm{cycle}(6,7))$$

Example:

The following two expressions represent the same permutation of {1,2,3,4,5}.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>	<OMS cd="fns1" name="inverse"/>
					<OMA>	<OMS cd="permutation1" name="permutation"/>
						<OMA>   <OMS cd="permutation1" name="cycle"/>
							<OMI>1</OMI>
							<OMI>3</OMI>
							<OMI>2</OMI>
						</OMA>
						<OMA>	<OMS cd="permutation1" name="cycle"/>
							<OMI>4</OMI>
							<OMI>5</OMI>
						</OMA>
					</OMA>
				</OMA>
			</OMOBJ>

inverse (permutation (cycle (1, 3, 2) , cycle (4, 5) ) )

$${\mathrm{permutation}(\mathrm{cycle}(1,3,2),\mathrm{cycle}(4,5))}^{-1}$$

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>	<OMS cd="permutation1" name="permutation"/>
					<OMA>	<OMS cd="permutation1" name="cycle"/>
						<OMI>1</OMI>
						<OMI>2</OMI>
						<OMI>3</OMI>
					</OMA>
					<OMA>	<OMS cd="permutation1" name="cycle"/>
						<OMI>4</OMI>
						<OMI>5</OMI>
					</OMA>
				</OMA>
			</OMOBJ>

permutation (cycle (1, 2, 3) , cycle (4, 5) )

$$\mathrm{permutation}(\mathrm{cycle}(1,2,3),\mathrm{cycle}(4,5))$$

Example:

Left and right composition of two permutations may lead to distinct results:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>	<OMS cd="relation1" name="eq"/>
					<OMA>	<OMS cd="fns1" name="left_compose"/>
						<OMA>	<OMS cd="permutation1" name="permutation"/>
							<OMA>	<OMS cd="permutation1" name="cycle"/>
								<OMI>1</OMI>
								<OMI>2</OMI>
							</OMA>
						</OMA>
						<OMA>	<OMS cd="permutation1" name="permutation"/>
							<OMA>	<OMS cd="permutation1" name="cycle"/>
								<OMI>1</OMI>
								<OMI>2</OMI>
								<OMI>3</OMI>
							</OMA>
						</OMA>
					</OMA>
					<OMA>	<OMS cd="permutation1" name="permutation"/>
						<OMA>	<OMS cd="permutation1" name="cycle"/>
							<OMI>2</OMI>
							<OMI>3</OMI>
						</OMA>
					</OMA>
				</OMA>
			</OMOBJ>

eq (left_compose (permutation (cycle (1, 2) ) , permutation (cycle (1, 2, 3) ) ) , permutation (cycle (2, 3) ) )

$$\mathrm{permutation}\left(\mathrm{cycle}(1,2)\right)o\mathrm{permutation}\left(\mathrm{cycle}(1,2,3)\right)=\mathrm{permutation}\left(\mathrm{cycle}(2,3)\right)$$

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>	<OMS cd="relation1" name="eq"/>
					<OMA>	<OMS cd="fns1" name="right_compose"/>
						<OMA>	<OMS cd="permutation1" name="permutation"/>
							<OMA>	<OMS cd="permutation1" name="cycle"/>
								<OMI>1</OMI>
								<OMI>2</OMI>
							</OMA>
						</OMA>
						<OMA>	<OMS cd="permutation1" name="permutation"/>
							<OMA>	<OMS cd="permutation1" name="cycle"/>
								<OMI>1</OMI>
								<OMI>2</OMI>
								<OMI>3</OMI>
							</OMA>
						</OMA>
					</OMA>
					<OMA>	<OMS cd="permutation1" name="permutation"/>
						<OMA>	<OMS cd="permutation1" name="cycle"/>
							<OMI>1</OMI>
							<OMI>3</OMI>
						</OMA>
					</OMA>
				</OMA>
			</OMOBJ>

eq (right_compose (permutation (cycle (1, 2) ) , permutation (cycle (1, 2, 3) ) ) , permutation (cycle (1, 3) ) )

$$\mathrm{right\_compose}(\mathrm{permutation}\left(\mathrm{cycle}(1,2)\right),\mathrm{permutation}\left(\mathrm{cycle}(1,2,3)\right))=\mathrm{permutation}\left(\mathrm{cycle}(1,3)\right)$$

Signatures:

sts

is_perm

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_perm(A) is true then permutation(A) is well defined.

Example:

The following value is the boolean false

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA><OMS cd="permutation1" name="is_perm"/>
				  <OMA><OMS cd="set1" name="set"/>
				    <OMA><OMS cd="permutation1" name="cycle"/>
					 <OMI> 5 </OMI>	<OMI> 4 </OMI>	<OMI> 4 </OMI>	<OMI> 2 </OMI>	<OMI> 1 </OMI>
				     </OMA>
				  </OMA>
				</OMA>
			</OMOBJ>

is_perm (set (cycle ( 5 , 4 , 4 , 2 , 1 ) ) )

$$\mathrm{is\_perm}\left(\left\{\mathrm{cycle}(5,4,4,2,1)\right\}\right)$$

whereas the following value is true

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
			<OMA><OMS cd="permutation1" name="is_perm"/>
			  <OMA><OMS cd="set1" name="set"/>
			    <OMA><OMS cd="permutation1" name="cycle"/>
 				 <OMI> 5 </OMI>	<OMI> 4 </OMI>	<OMI> 3 </OMI>	<OMI> 2 </OMI>	<OMI> 1 </OMI>
			    </OMA>
			  </OMA>
			</OMA>
			</OMOBJ>

is_perm (set (cycle ( 5 , 4 , 3 , 2 , 1 ) ) )

$$\mathrm{is\_perm}\left(\left\{\mathrm{cycle}(5,4,3,2,1)\right\}\right)$$

Signatures:

sts

support

Description:

This symbol is a function with one argument which is a permutation. When applied to a permutation P 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,4,5}.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>	<OMS cd="permutation1" name="permutation"/>
					<OMA>	<OMS cd="permutation1" name="cycle"/>
						<OMSTR>jan</OMSTR>
						<OMI>4</OMI>
						<OMSTR>klaas</OMSTR>
					</OMA>
					<OMA>	<OMS cd="permutation1" name="cycle"/>
						<OMI>3</OMI>
						<OMSTR>klaas</OMSTR>
					</OMA>
					<OMA>	<OMS cd="permutation1" name="cycle"/>
						<OMSTR>piet</OMSTR>
						<OMI>5</OMI>
					</OMA>
				</OMA>
			</OMOBJ>

permutation (cycle ( "jan" , 4, "klaas" ) , cycle (3, "klaas" ) , cycle ( "piet" , 5) )

$$\mathrm{permutation}(\mathrm{cycle}(\text{jan},4,\text{klaas}),\mathrm{cycle}(3,\text{klaas}),\mathrm{cycle}(\text{piet},5))$$

Signatures:

sts

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 the permutation mapping i to a_i.

Example:

The following two expressions represent the same permutation of {1,2,3,4,5}.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>   <OMS cd="permutation1" name="perm"/>
					<OMI>2</OMI>
					<OMI>3</OMI>
					<OMI>1</OMI>
					<OMI>5</OMI>
					<OMI>4</OMI>
				</OMA>
			</OMOBJ>

perm (2, 3, 1, 5, 4)

$$\mathrm{perm}(2,3,1,5,4)$$

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>	<OMS cd="permutation1" name="permutation"/>
					<OMA>	<OMS cd="permutation1" name="cycle"/>
						<OMI>1</OMI>
						<OMI>2</OMI>
						<OMI>3</OMI>
					</OMA>
					<OMA>	<OMS cd="permutation1" name="cycle"/>
						<OMI>4</OMI>
						<OMI>5</OMI>
					</OMA>
				</OMA>
			</OMOBJ>

permutation (cycle (1, 2, 3) , cycle (4, 5) )

$$\mathrm{permutation}(\mathrm{cycle}(1,2,3),\mathrm{cycle}(4,5))$$

Example:

The following expression evaluates to true.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>	<OMS cd="relation1" name="eq"/>
                                  <OMA>	<OMA>	<OMS cd="permutation1" name="perm"/>
						<OMI> 5 </OMI>
						<OMI> 1 </OMI>
						<OMI> 3 </OMI>
						<OMI> 2 </OMI>
						<OMI> 4 </OMI>
					</OMA>
					<OMI> 4 </OMI>
				  </OMA>
				  <OMI> 2 </OMI>
				</OMA>

			</OMOBJ>

eq (perm ( 5 , 1 , 3 , 2 , 4 ) ( 4 ) , 2 )

$$\left(\mathrm{perm}(5,1,3,2,4)\right)\left(4\right)=2$$

Signatures:

sts

listperm

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. Here n is at least the maximum of the support of P.

Example:

The following two expressions represent the same list.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>   <OMS cd="permutation1" name="listperm"/>
					<OMA>   <OMS cd="permutation1" name="permutation"/>
						<OMA>	<OMS cd="permutation1" name="cycle"/>
							<OMI> 1 </OMI>
							<OMI> 5 </OMI>
							<OMI> 4 </OMI>
							<OMI> 2 </OMI>
						</OMA>
						<OMA>	<OMS cd="permutation1" name="cycle"/>
							<OMI> 6 </OMI>
							<OMI> 7 </OMI>
						</OMA>
					</OMA>
				</OMA>
			</OMOBJ>

listperm (permutation (cycle ( 1 , 5 , 4 , 2 ) , cycle ( 6 , 7 ) ) )

$$\mathrm{listperm}\left(\mathrm{permutation}(\mathrm{cycle}(1,5,4,2),\mathrm{cycle}(6,7))\right)$$

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
				<OMA>	<OMS cd="list1" name="list"/>
					<OMI> 5 </OMI>
					<OMI> 1 </OMI>
					<OMI> 3 </OMI>
					<OMI> 2 </OMI>
					<OMI> 4 </OMI>
					<OMI> 7 </OMI>
					<OMI> 6 </OMI>
				</OMA>
			</OMOBJ>

list ( 5 , 1 , 3 , 2 , 4 , 7 , 6 )

$$(5,1,3,2,4,7,6)$$

Signatures:

sts

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):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMBIND><OMS cd="quant1" name="forall"/>
  <OMBVAR><OMV name="P"/><OMV name="Q"/></OMBVAR>
  <OMA><OMS cd="logic1" name="implies"/>
    <OMA><OMS cd="logic1" name="and"/>
      <OMA><OMS cd="permutation1" name="is_perm"/>
           <OMV name="P"/>
      </OMA>
      <OMA><OMS cd="permutation1" name="is_perm"/>
           <OMV name="Q"/>
      </OMA>
    </OMA>
    <OMA><OMS cd="relation1" name="eq"/>
      <OMA><OMS cd="permutation1" name="cycle_type"/>
      <OMA><OMS cd="fns2" name="apply_to_list"/>      
          <OMS cd="fns1" name="left_compose"/>
          <OMA><OMS cd="list1" name="list"/>
               <OMV name="Q"/>
               <OMV name="P"/>
               <OMA><OMS cd="fns1" name="inverse"/>
                    <OMV name="Q"/>
               </OMA>
          </OMA>
        </OMA>
      </OMA>
      <OMA><OMS cd="permutation1" name="cycle_type"/>
           <OMV name="P"/>
      </OMA>
    </OMA> 
  </OMA> 
</OMBIND>
</OMOBJ>

forall [ P Q] . (implies (and (is_perm ( P) , is_perm ( Q) ) , eq (cycle_type (apply_to_list (left_compose, list ( Q, P, inverse ( Q) ) ) ) , cycle_type ( P) ) ) )

$$\forall \hspace{0.17em}P,Q.\mathrm{is\_perm}\left(P\right)\wedge \mathrm{is\_perm}\left(Q\right)\Rightarrow \mathrm{cycle\_type}\left(\mathrm{apply\_to\_list}(o,(Q,P,Q^{-1}))\right)=\mathrm{cycle\_type}\left(P\right)$$

Example:

The cycle type of the permutation (4,3,2,1)(5,6)("jan","piet") equals {4,2,2}:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA><OMS cd="relation1" name="eq"/>
  <OMA><OMS cd="permutation1" name="cycle_type"/>
    <OMA><OMS cd="permutation1" name="permutation"/>
      <OMA><OMS cd="permutation1" name="cycle"/>
        <OMI> 4 </OMI> <OMI> 3 </OMI><OMI> 2 </OMI><OMI> 1 </OMI>
      </OMA>
      <OMA><OMS cd="permutation1" name="cycle"/>
        <OMI> 5 </OMI><OMI> 6 </OMI>
      </OMA>
      <OMA><OMS cd="permutation1" name="cycle"/>
        <OMSTR>jan</OMSTR><OMSTR>piet</OMSTR>
      </OMA>
    </OMA>
  </OMA>
  <OMA><OMS cd="multiset1" name="multiset"/>
    <OMI> 4 </OMI><OMI> 2 </OMI><OMI> 2 </OMI>
  </OMA>
</OMA>
</OMOBJ>

eq (cycle_type (permutation (cycle ( 4 , 3 , 2 , 1 ) , cycle ( 5 , 6 ) , cycle ( "jan" , "piet" ) ) ) , multiset ( 4 , 2 , 2 ) )

$$\mathrm{cycle\_type}\left(\mathrm{permutation}(\mathrm{cycle}(4,3,2,1),\mathrm{cycle}(5,6),\mathrm{cycle}(\text{jan},\text{piet}))\right)=\mathrm{multiset}(4,2,2)$$

Signatures:

sts

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):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMBIND><OMS cd="quant1" name="forall"/>
  <OMBVAR><OMV name="P"/></OMBVAR>
  <OMA><OMS cd="logic1" name="implies"/>
    <OMA><OMS cd="permutation1" name="is_perm"/>
      <OMV name="P"/>
    </OMA>
    <OMA><OMS cd="relation1" name="eq"/>
      <OMA><OMS cd="permutation1" name="order"/>
        <OMV name="P"/>
      </OMA>
      <OMA><OMS cd="fns2" name="apply_to_list"/>      
           <OMS cd="arith1" name="lcm"/>
           <OMA><OMS cd="permutation1" name="cycle_type"/>
               <OMV name="P"/>
           </OMA>
      </OMA>
    </OMA>
  </OMA> 
</OMBIND>
</OMOBJ>

forall [ P] . (implies (is_perm ( P) , eq (order ( P) , apply_to_list (lcm, cycle_type ( P) ) ) ) )

$$\forall \hspace{0.17em}P.\mathrm{is\_perm}\left(P\right)\Rightarrow \mathrm{order}\left(P\right)=\mathrm{apply\_to\_list}(\mathrm{lcm},\mathrm{cycle\_type}\left(P\right))$$

Example:

The order of the permutation (4,3,2,1)(5,6)("jan","piet") equals 4:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA><OMS cd="relation1" name="eq"/>
  <OMA><OMS cd="permutation1" name="order"/>
    <OMA><OMS cd="permutation1" name="permutation"/>
      <OMA><OMS cd="permutation1" name="cycle"/>
        <OMI> 4 </OMI> <OMI> 3 </OMI><OMI> 2 </OMI><OMI> 1 </OMI>
      </OMA>
      <OMA><OMS cd="permutation1" name="cycle"/>
        <OMI> 5 </OMI><OMI> 6 </OMI>
      </OMA>
      <OMA><OMS cd="permutation1" name="cycle"/>
        <OMSTR>jan</OMSTR><OMSTR>piet</OMSTR>
      </OMA>
    </OMA>
  </OMA>
    <OMI> 4 </OMI>
</OMA>
</OMOBJ>

eq (order (permutation (cycle ( 4 , 3 , 2 , 1 ) , cycle ( 5 , 6 ) , cycle ( "jan" , "piet" ) ) ) , 4 )

$$\mathrm{order}\left(\mathrm{permutation}(\mathrm{cycle}(4,3,2,1),\mathrm{cycle}(5,6),\mathrm{cycle}(\text{jan},\text{piet}))\right)=4$$

Signatures:

sts

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.

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">  <OMA> 	<OMS cd="permutation1" name="are_distinct"/>
			<OMI> 1 </OMI>
			<OMI> 3 </OMI>
			<OMI> 2 </OMI>
			<OMI> 3</OMI>
                 </OMA>
        </OMOBJ>

are_distinct ( 1 , 3 , 2 , 3)

$$\mathrm{are\_distinct}(1,3,2,3)$$

Signatures:

sts

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 b = a_1+...+a_m.

Formal Mathematical property (FMP):

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMBIND><OMS cd="quant1" name="forall"/>
 <OMBVAR><OMV name="P"/></OMBVAR>
 <OMA><OMS cd="relation1" name="eq"/>
      <OMA><OMS cd="permutation1" name="sign"/>
           <OMA><OMS cd="permutation1" name="permutation"/>
                <OMV name="P"/>
           </OMA>
      </OMA>
      <OMA><OMS cd="arith1" name="power"/>
           <OMI>-1</OMI>
           <OMA><OMS cd="fns2" name="apply_to_list"/>      
                <OMA><OMS cd="arith1" name="plus"/>
                     <OMA><OMS cd="list1" name="map"/>
                          <OMBIND><OMS cd="fns1" name="lambda"/>
                                  <OMBVAR><OMV name="x"/></OMBVAR>
                                  <OMA><OMS cd="arith1" name="plus"/>
                                       <OMV name="x"/>
                                       <OMI>1</OMI>      
                                  </OMA>
                          </OMBIND>
                     </OMA>
                     <OMA><OMS cd="permutation1" name="cycle_type"/>
                          <OMA><OMS cd="permutation1" name="permutation"/>
                               <OMV name="P"/>
                          </OMA>
                     </OMA>

                </OMA>
           </OMA>
      </OMA> 
 </OMA>  
</OMBIND>
</OMOBJ>

forall [ P] . (eq (sign (permutation ( P) ) , power (-1, apply_to_list (plus (map (lambda [ x] . (plus ( x, 1) ) ) , cycle_type (permutation ( P) ) ) ) ) ) )

$$\forall \hspace{0.17em}P.\mathrm{sign}\left(\mathrm{permutation}\left(P\right)\right)={-1}^{\mathrm{apply\_to\_list}\left(\mathrm{list}\left(x+1\right|x\in )+\mathrm{cycle\_type}\left(\mathrm{permutation}\left(P\right)\right)\right)}$$

Example:

The sign of the permutation (4,3,2,1)(5,6)("jan","piet") equals -1:

xml prefix mathml

<OMOBJ xmlns="http://www.openmath.org/OpenMath">
<OMA><OMS cd="relation1" name="eq"/>
  <OMA><OMS cd="permutation1" name="sign"/>
    <OMA><OMS cd="permutation1" name="permutation"/>
      <OMA><OMS cd="permutation1" name="cycle"/>
        <OMI> 4 </OMI> <OMI> 3 </OMI><OMI> 2 </OMI><OMI> 1 </OMI>
      </OMA>
      <OMA><OMS cd="permutation1" name="cycle"/>
        <OMI> 5 </OMI><OMI> 6 </OMI>
      </OMA>
      <OMA><OMS cd="permutation1" name="cycle"/>
        <OMSTR>jan</OMSTR><OMSTR>piet</OMSTR>
      </OMA>
    </OMA>
  </OMA>
    <OMI> -1 </OMI>
</OMA>
</OMOBJ>

eq (sign (permutation (cycle ( 4 , 3 , 2 , 1 ) , cycle ( 5 , 6 ) , cycle ( "jan" , "piet" ) ) ) , -1 )

$$\mathrm{sign}\left(\mathrm{permutation}(\mathrm{cycle}(4,3,2,1),\mathrm{cycle}(5,6),\mathrm{cycle}(\text{jan},\text{piet}))\right)=-1$$

Signatures:

sts