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ć.O reprezentacjach permutacji
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.
Nic nie wiem o Coq, ale czy to pomaga? http://coq.inria.fr/stdlib/Coq.Sorting.Permutation.html –
Niestety tak nie jest. Potrzebuję kodowania permutacji bez odniesienia do kontenera. Chociaż byłoby przyjemnie mieć ogólną definicję relacji podobną do wspomnianej. –
Być może mógłbyś go wyspecjalizować, aby przestawiał uporządkowaną listę indeksów? –