O reprezentacjach permutacji

Question

Chciałbym mieć typ indukcyjny do opisu permutacji i ich działania w niektórych pojemnikach. Oczywiste jest, że w zależności od opisu tego typu złożoność definicji (pod względem długości) algorytmów (kompozycja obliczeniowa lub odwrotność, rozkład na rozłączne cykle itp.) Będzie się różnić.

Rozważ poniższą definicję w Coq. Wierzę, że jest formalizacja kodu Lehmer:

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

Łatwo jest określić swoje działania na wektorach o rozmiarze n, nieco trudniej na innych pojemników i (przynajmniej dla mnie) trudno dowiedzieć się formalizacji składu lub odwrotność.

Alternatywnie możemy przedstawić permutację jako skończoną mapę z właściwościami. Kompozycję lub odwrotność można łatwo określić, ale rozkładanie jej na rozłączne cykle jest trudne.

Moje pytanie brzmi: czy są jakieś dokumenty, które dotyczą tego problemu? Wszystkie prace, które udało mi się znaleźć, zajmują się złożonością obliczeniową w imperatywnych ustawieniach, natomiast interesuję się "złożonością rozumowania" i programowaniem funkcjonalnym.

Answer 1

Georges Gonthier obszernie przestudiował permutacje dla swoich dowodów zarówno twierdzenia o 4 kolorach, jak i twierdzeniu Feit-Thompson. Jego pakiet ssreflect dla coq ułatwia rozumowanie o permutacjach, szczególnie w stosunku do zbiorów skończonych, używając obliczeń w Coq zamiast używać taktyk. Jego biblioteka seq jest punktem wejścia.

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

Można tu dostać pełne źródła.

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

Wreszcie

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

omówiono 3 reprezentacje permutacji.