On representations of permutations

Question

I would like to have an inductive type to describe permutations and their action on some containers. It is clear that depending on the description of this type the definition complexity (in terms of its length) of algorithms (computing composition or inverse, decomposing into disjoint cycles, etc.) will vary.

Consider the following definition in Coq. I believe it to be formalisation of Lehmer code:

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

It is easy to define its action on vectors of size n, slightly harder on other containers and (at least for me) hard to find out formalisation of composition or inverse.

Alternatively we can represent permutation as a finite map with properties. Composition or inverse can be easily defined but decomposing it into disjoint cycles is difficult.

So my question is: are there any papers that address this trade-off issue? All works, that I managed to find, deal with a computational complexity in imperative settings, whereas I'm interested in "reasoning complexity" and functional programming.

Answer 1

Georges Gonthier has extensively studied permutations for his proofs of both the 4 color theorem and the Feit-Thompson theorem. His ssreflect package for coq facilitates reasoning about permutations, especially over finite sets, by using computation in Coq rather than using tactics. His seq library is the entry point.

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

You can get the full sources here.

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

Finally,

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

discusses 3 representations of permutations.