Я хотел бы иметь индуктивный тип для описания перестановок и их действия на некоторых контейнерах. Понятно, что в зависимости от описания этого типа сложность определения (по длине) алгоритмов (вычислительная композиция или обратная, разлагающаяся на непересекающиеся циклы и т.д.) Будет различаться.
Рассмотрим следующее определение в Coq. Я считаю, что это формализация кода Леммера:
Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).
Легко определить его действие на векторах размера n, немного сложнее на других контейнерах и (по крайней мере для меня) трудно найти формализацию композиции или инверсии.
В качестве альтернативы мы можем представить перестановку как конечное отображение со свойствами. Композицию или инверсию можно легко определить, но сложно разложить ее на непересекающиеся циклы.
Итак, мой вопрос: есть ли какие-либо документы, посвященные этой проблеме компромиссов? Все работы, которые мне удалось найти, имеют дело с вычислительной сложностью в императивных настройках, тогда как меня интересует "сложность рассуждений" и функциональное программирование.
