permutation1 http://www.win.tue.nl/~amc/oz/om/cds/permutation1.ocd 2002-10-21 2003-07-27 experimental 1.3 0 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 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. for i = 1,..., n cycle(a_i, a_{i+1},...,a_n,a_1,...,a_{i-1}) = cycle(a_1, a_2,...,a_n). The following expression represents the relation on the set {"jan","piet","klaas"} whose members are ("jan","piet"), ("piet","klaas"), and ("klaas","jan"). jan piet klaas length 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. The following expression should evaluate to 3. 2 4 3 permutation 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. 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). For a valid argument A the inverse of permutation(A) is a permutation again (that is, evaluates to permutation(C) for suitable argument C). permutation() is the identity. 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 1 5 4 2 6 7 The following two expressions represent the same permutation of {1,2,3,4,5}. 1 3 2 4 5 1 2 3 4 5 Left and right composition of two permutations may lead to distinct results: 1 2 1 2 3 2 3 1 2 1 2 3 1 3 is_perm 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. If is_perm(A) is true then permutation(A) is well defined. The following value is the boolean false 5 4 4 2 1 whereas the following value is true 5 4 3 2 1 support 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. The following expression represents the set {jan,piet,klaas,4,5}. jan 4 klaas 3 klaas piet 5 perm 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. The following two expressions represent the same permutation of {1,2,3,4,5}. 2 3 1 5 4 1 2 3 4 5 The following expression evaluates to true. 5 1 3 2 4 4 2 listperm 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. The following two expressions represent the same list. 1 5 4 2 6 7 5 1 3 2 4 7 6 cycle_type 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. The cycle type of the permutation (4,3,2,1)(5,6)("jan","piet") equals {4,2,2}: 4 3 2 1 5 6 janpiet 4 2 2 order 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. The order of a permutation is the least common multiple of the elements of its cycle type. The order of the permutation (4,3,2,1)(5,6)("jan","piet") equals 4: 4 3 2 1 5 6 janpiet 4 are_distinct 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). If are_distinct(a_1,...,a_n) is true then a_1,...,a_n is a valid argument sequence of cycle. The following expression evaluates to false. 1 3 2 3 sign 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. 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. -1 1 The sign of the permutation (4,3,2,1)(5,6)("jan","piet") equals -1: 4 3 2 1 5 6 janpiet -1