Algorithmen und Datenstrukturen 2011 WS

ADT

Type Permutation

Import int, String, Bool, Menge, Sequenz

Literals idn (für jede Permutationsgruppe Sn)

Operations

Permutation:	Sequenz<int> ---> Permutation	Erzeugt eine Permutation
	Sequenz<Sequenz<int>> ---> Permutation
	String -/-> Permutation
getPermElement:	int x Permutation -/-> int	Gibt das gewählte Abbild
cycle:	Permutation x int -/-> Sequenz<int>	Gibt den gewählten Zyklus
allCycles:	Permutation ---> Menge<Sequenz<int>>	Gibt alle Zyklen aus der Permutation
cycleType:	Permutation ---> Hashtabelle<int,int>	Gibt den Zyklentyp der Permutation
fixedPoints:	Permutation ---> Menge<Sequenz<int>>	Gibt alle Fixpunkt aus der Permutation
inverse:	Permutation ---> Permutation	Gibt die invertierte Permutation
toString:	Permutation ---> String	Darstellung als String
toCycleNotationString:	Permutation ---> String	Darstellung der Zyklen als String
toCycleTypeString:	Permutation ---> String	Darstellung des Zyklentyps als String
equals:	Permutation x Permutation ---> Bool	Prüft strukturelle Gleichheit
compose:	Permutation x Permutation -/-> Permutation	Gibt die Komposition der beiden Permutation wieder
permutationClass:	Permutation ---> int	Gibt die Anzahl der Elemente der Permutation
permPower:	Permutation x int ---> Permutation	Gibt die Permutation^n an
order:	Permutation ---> int	Gibt die Ordnung der Permutation an
id:	Permutation ---> Permutation	Gibt die Id der Permutation an
toTransposition:	Permutation -/-> Sequenz<Sequenz<int>>	Wandelt die Permutation in eine Transpositionsdarstellung um
toTranspositionString:	Permutation ---> String	Wandelt die Permutation in eine Transpositionsdarstellung in Stringform um
Sign:	Permutation ---> [-1; 1]	Gibt an ob die Permutation even(1) oder odd(-1) ist.

Axioms

σ: Permutation σ ∈ S1

cycle(σ ,1) = fixedPoints(σ)

inverse(σ) = σ

inverse(σ) = compose(σ,σ)

compose(σ,inverse(σ)) = σ

equals(σ,σ) = true

σ1,σ2,σ3,id :Permutation σ1,σ2,σ3,id ∈ Sn

n : Integer n ∈N && n!=0

id(σ1) = id;

id(id) = id;

compose(σ1,compose(σ2,σ3)) = compose(compose(σ1,σ2),σ3)

equals(σ1,id) = true & equals(σ1,σ2) = false => fixedPoints(σ1) != fixedPoints(σ2)

inverse(inverse(σ3)) = σ3

equals(σ1,σ2) = equals(σ2,σ1)

equals(σ1,σ2) = equals(cycle(σ1), cycle(σ2))

equals(σ1,σ2) => equals(inverse(σ1), inverse(σ2))

permPower(σ1,0) = id

permPower(σ1,1) = σ1

permPower(σ1,-1) = inverse(σ1)

permPower(σ1, order(σ1)) = id

permPower(σ1,-n) = permPower(inverse(σ1), n)

cycleType(id) = [1^permutationClass(id)]