在排列

的表示，我想有一個感應式來描述置換及其對某些容器行動。清楚的是，取決於這種類型的描述，算法的定義複雜性（按其長度）（計算組合或逆，分解成不相交的週期等）將會變化。在排列

考慮勒柯克下面的定義。我相信這是萊默代碼形式化：

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

很容易界定在一個大小爲載體的作用，稍硬其他容器（至少我）很難找出的構成形式化或逆。

另外，我們可以表示置換爲有限地圖特性。成分或逆可以很容易地定義，但將其分解成不相交的週期是困難的。

所以我的問題是：有沒有解決這個權衡問題的任何文件？我設法找到的所有作品都處理命令式設置中的計算複雜性，而我對「推理複雜性」和函數式編程感興趣。

2013-07-02 Katty J.

我一無所知勒柯克，但是這是否幫助？ http://coq.inria.fr/stdlib/Coq.Sorting.Permutation.html –

不幸的是，它沒有。我想要的是不考慮集裝箱的排列編碼。雖然有一個類似於所提到的關係的容器泛型定義會很令人愉快。 –

也許你可以專門化它，以便它排列索引的排序列表？ –

喬治斯·戈西爾廣泛研究排列爲他的四色定理和費特 - 湯普森定理都證明。他的coref的ssreflect包通過在Coq中使用計算而不是使用策略來促進關於置換的推理，特別是在有限集上的推理。他的seq庫是入門點。

你可以在這裏得到充分的來源。

最後，

討論排列3級表示。

2013-10-23 17:18:33 seanmcl

回答