types - 关于排列的表示

Question

我想有一个归纳类型来描述排列及其对某些容器的作用。很明显，根据对这种类型的描述，算法的定义复杂性（就其长度而言）（计算组合或逆，分解成不相交的循环等）会有所不同。

考虑 Coq 中的以下定义。我相信这是 Lehmer 代码的形式化：

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

在大小为 n 的向量上定义它的作用很容易，在其他容器上稍微难一些，而且（至少对我而言）很难找到组合或逆的形式化。

或者，我们可以将置换表示为具有属性的有限映射。组合或逆可以很容易地定义，但将其分解为不相交的循环是困难的。

所以我的问题是：有没有解决这个权衡问题的论文？我设法找到的所有作品都处理命令式设置中的计算复杂性，而我对“推理复杂性”和函数式编程感兴趣。

score 4 · Accepted Answer

Georges Gonthier 为证明 4 色定理和 Feit-Thompson 定理而广泛研究了排列。他的 coq ssreflect 包通过在 Coq 中使用计算而不是使用策略来促进对排列的推理，尤其是在有限集上。他的 seq 库是入口点。

你可以在这里获得完整的资源。

最后，

讨论排列的 3 种表示。

1 回答 1