Ich möchte einen induktiven Typ haben, um Permutationen und ihre Wirkung auf einige Behälter zu beschreiben. Es ist klar, dass abhängig von der Beschreibung dieses Typs die Definitionskomplexität (in Bezug auf ihre Länge) von Algorithmen (Berechnung der Zusammensetzung oder invers, Zerlegung in disjunkte Zyklen usw.) variieren wird.Auf Darstellungen von Permutationen
Betrachten Sie die folgende Definition in Coq. Ich glaube, es Formalisierung von Lehmer-Code zu sein:
Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).
Es ist leicht, seine Wirkung auf Vektoren der Größe n zu definieren, etwas härter auf anderen Behältern und (zumindest für mich) hart Formalisierung der Zusammensetzung, um herauszufinden, oder invers.
Alternativ können wir Permutation als eine endliche Karte mit Eigenschaften darstellen. Zusammensetzung oder Umkehrung kann leicht definiert werden, aber es ist schwierig, sie in disjunkte Zyklen zu zerlegen.
Also meine Frage ist: Gibt es Papiere, die diese Frage Problem behandeln? Alle Arbeiten, die ich gefunden habe, befassen sich mit einer rechnerischen Komplexität in imperativen Einstellungen, während ich mich für "Argumentationskomplexität" und funktionale Programmierung interessiere.
Ich weiß nichts über Coq, aber hilft das? http://coq.inria.fr/stdlib/Coq.Sorting.Permutation.html –
Leider tut es das nicht. Was ich will, sind die Kodierungen der Permutation ohne Bezugnahme auf einen Container. Obwohl es angenehm wäre, eine Container-generische Definition der Beziehung ähnlich der genannten zu haben. –
Vielleicht könnten Sie es spezialisieren, damit es eine sortierte Liste von Indizes permutiert? –