Mi piacerebbe avere un tipo induttivo per descrivere le permutazioni e la loro azione su alcuni contenitori. È chiaro che a seconda della descrizione di questo tipo la complessità della definizione (in termini di lunghezza) di algoritmi (composizione computazionale o inversa, scomposizione in cicli disgiunti, ecc.) Varierà.Su rappresentazioni di permutazioni
Considerare la seguente definizione in Coq. Credo che sia formalizzazione del codice di Lehmer:
Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).
È facile definire la sua azione sui vettori di dimensione n, un po 'più difficile per altri contenitori e (almeno per me) è difficile trovare fuori formalizzazione della composizione o inverso.
In alternativa, possiamo rappresentare la permutazione come una mappa finita con proprietà. La composizione o l'inverso possono essere facilmente definiti ma la loro decomposizione in cicli disgiunti è difficile.
Quindi la mia domanda è: ci sono documenti che affrontano questo problema di trade-off? Tutti i lavori, che sono riuscito a trovare, affrontano una complessità computazionale in contesti imperativi, mentre sono interessato alla "complessità del ragionamento" e alla programmazione funzionale.
Non so nulla di Coq, ma questo aiuto? http://coq.inria.fr/stdlib/Coq.Sorting.Permutation.html –
Sfortunatamente no. Quello che voglio sono le codifiche della permutazione senza riferimento a un contenitore. Anche se sarebbe piacevole avere una definizione generica del contenitore di relazione simile a quella menzionata. –
Forse potresti specializzarlo in modo tale da permutare un elenco ordinato di indici? –