Sur les représentations des permutations

j'aimerais avoir un type inductif pour décrire les permutations et leur action sur certains conteneurs. Il est clair que, selon la description de ce type, la complexité de la définition (en termes de longueur) des algorithmes (calcul de la composition ou inverse, décomposition en cycles disjoints, etc.) varient.

réfléchir à la définition suivante dans Coq. Je crois que c'est la formalisation de Lehmer code:

Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).

Il est facile de définir son action sur Vecteurs de taille n, légèrement plus dur sur les autres récipients et (au moins pour moi) difficile à trouver formalisation de la composition ou inverse.

nous pouvons aussi représenter la permutation comme une carte finie avec des propriétés. La Composition ou l'inverse peut être facilement défini, mais il est difficile de le décomposer en cycles disjoints.

Donc ma question est: existe-il des documents qui traitent de ce compromis problème? Tous les travaux, que j'ai réussi à trouver, faire face à une complexité des réglages impératifs, alors que je m'intéresse à la "complexité du raisonnement" et à la programmation fonctionnelle.

25
demandé sur Sjoerd Visscher 2013-07-02 19:47:56
la source

1 ответов

Georges Gonthier a longuement étudié les permutations pour ses preuves du théorème des 4 couleurs et du théorème de Feit-Thompson. Son paquet ssreflect pour coq facilite le raisonnement sur les permutations, en particulier sur les ensembles finis, en utilisant le calcul dans Coq plutôt que d'utiliser des tactiques. Sa bibliothèque seq est le point d'entrée.

http://ssr2.msr-inria.inria.fr/doc/ssreflect-1.4/Ssreflect.seq.html

Vous pouvez obtenir les sources complètes ici.

http://research.microsoft.com/en-us/downloads/5464E7B1-BD58-4F7C-BFE1-5D3B32D42E6D/default.aspx

Enfin,

http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/4193

discute 3 représentations de permutations.

4
répondu seanmcl 2013-10-23 21:31:42
la source