types - tipos - Sobre representaciones de permutaciones.

permutaciones y combinaciones

Question

Me gustaría tener un tipo inductivo para describir las permutaciones y su acción en algunos contenedores. Es claro que, dependiendo de la descripción de este tipo, la complejidad de la definición (en términos de su longitud) de los algoritmos (composición computacional o inversa, descomposición en ciclos disjuntos, etc.) variará.

Considere la siguiente definición en Coq. Creo que es formalización del código de Lehmer:

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

Es fácil definir su acción en vectores de tamaño n, un poco más duro en otros recipientes y (al menos para mí) difícil de averiguar la formalización de la composición o la inversa.

Alternativamente, podemos representar la permutación como un mapa finito con propiedades. La composición o inversa se puede definir fácilmente, pero es difícil descomponerla en ciclos separados.

Entonces, mi pregunta es: ¿hay documentos que aborden este problema de compensación? Todos los trabajos, que logré encontrar, tratan con una complejidad computacional en entornos imperativos, mientras que me interesa la "complejidad de razonamiento" y la programación funcional.

Answer 1

Georges Gonthier ha estudiado exhaustivamente las permutaciones de sus pruebas del teorema de los 4 colores y del teorema de Feit-Thompson. Su paquete ssreflect para coq facilita el razonamiento sobre las permutaciones, especialmente sobre conjuntos finitos, al usar el cálculo en Coq en lugar de usar tácticas. Su biblioteca de seq es el punto de entrada.

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

Puede obtener las fuentes completas aquí.

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

Finalmente,

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

discute 3 representaciones de permutaciones.