26

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.

Sjoerd Visscher
  • 11,840
  • 2
  • 47
  • 59
Katty J.
  • 686
  • 4
  • 11
  • 2
    I know nothing about Coq, but does this help? http://coq.inria.fr/stdlib/Coq.Sorting.Permutation.html – Sjoerd Visscher Jul 02 '13 at 18:00
  • 1
    Unfortunately, it does not. What I want is the encodings of permutation without reference to a container. Though it would be pleasant to have a container-generic definition of relation similar to the one mentioned. – Katty J. Jul 03 '13 at 06:21
  • 1
    Perhaps you could specialise it so it permutes a sorted list of indices? – Sjoerd Visscher Jul 03 '13 at 10:24
  • I think you should ask your question on the Coq mailing list (coq-club), you might reach more people able to answer it. – Vinz Jul 04 '13 at 10:14
  • 3
    Another representation that has worked fairly well for me is what I used in https://github.com/copumpkin/containers/blob/master/CommutativeSemigroup.agda#L30. Unfortunately it doesn't have nearly as simple a notion of composition as a bijection would. – copumpkin Jul 13 '13 at 03:41
  • 1
    This might get more traction on http://cs.stackexchange.com/ – Zac Thompson Sep 17 '13 at 21:47

1 Answers1

4

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.

seanmcl
  • 9,740
  • 3
  • 39
  • 45