Я хотел бы иметь индуктивный тип для описания перестановок и их действия на некоторых контейнерах. Понятно, что в зависимости от описания этого типа сложность определения (по длине) алгоритмов (вычислительная композиция или обратная, разлагающаяся на непересекающиеся циклы и т. Д.) Будет различаться.О представлениях перестановок
Рассмотрим следующее определение в Coq. Я считаю, что это формализация Лемера кода:
Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).
Легко определить его действие на векторы размера п, немного сложнее других контейнеров и (по крайней мере, для меня) трудно выяснить формализации композиции или обратное.
В качестве альтернативы мы можем представить перестановку как конечное отображение со свойствами. Композицию или инверсию можно легко определить, но сложно разложить ее на непересекающиеся циклы.
Итак, мой вопрос: есть ли какие-либо документы, посвященные этой проблеме компромиссов? Все работы, которые мне удалось найти, имеют дело с вычислительной сложностью в императивных настройках, тогда как меня интересует «разумная сложность» и функциональное программирование.
Я ничего не знаю о Coq, но помогает ли это? http://coq.inria.fr/stdlib/Coq.Sorting.Permutation.html –
К сожалению, это не так. Я хочу кодирование перестановки без ссылки на контейнер. Хотя было бы неплохо иметь контейнерное определение отношения, аналогичное упомянутому. –
Возможно, вы можете специализировать его, чтобы он перечислил отсортированный список индексов? –