permutation1 http://www.win.tue.nl/~amc/oz/om/cds/permutation1.ocd 2004-06-01 2006-06-01 experimental 1 7 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 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. 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. 2 2 1 1 2 The following expression evaluates to true. 5 1 3 2 4 4 2 list_perm 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. 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 is_endomap 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. The following expression evaluates to true 1 3 1 The following expression evaluates to false 2 3 5 is_list_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 true if a_i is at most n for all i and all a_i are distinct, otherwise it is false. The following expression evaluates to false 1 3 1 The following expression evaluates to false 2 3 5 The following expression evaluates to true 2 3 1 domain 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}. The following expression represents the set {1,2,3,4,5}. 4 3 5 5 5 is_bijective 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. The following expression evaluates to true. 1 3 2 The following expression evaluates to false. 2 3 5 endomap_left_compose 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)). endomap_right_compose 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)). cycle 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. 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 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. 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)(6,7) sending 1 to 5, 5 to 4, 4 to 1, 6 to 7, 7 to 6, is given by 1 5 4 6 7 is_permutation 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_permutation(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 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,3,4,5}. jan 4 klaas 3 klaas piet 5 fix 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. The following expression represents the set {1,2}. jan 4 klaas 3 klaas piet 5 1 5 cycles This symbol has one argument which should be a endomap p. It returns the list of cycles of p. The following two objects represent the same list. 2 3 4 2 5 2 3 4 listendomap 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. The following two expressions represent the same list. 1 4 4231 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 s = 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 inverse 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. 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_compose 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)). Left and right composition of two permutations may lead to distinct results: 1 2 1 2 3 2 3 right_compose 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)). 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. 1 2 1 2 3 1 3 action 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. The permutation (1,5,4)(6,7) sends 1 to 5, so 1 5 4 6 7 1 5 permutationsn 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}. Both sides of the following equality represent the two permutations on {1,2}. 2 12