关于排列的表示

Question

我想有一个归纳类型来描述排列及其对某些容器的行为.很明显,根据这种类型的描述,算法的定义复杂度(就其长度而言)(计算组合或逆,分解成不相交的循环等)将会变化.

考虑Coq中的以下定义.我认为这是Lehmer代码的形式化:

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

很容易在大小为n的向量上定义它的动作,在其他容器上稍微硬一些,并且(至少对我而言)很难找到组合的形式化或逆向.

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

所以我的问题是:是否有任何文件可以解决这个权衡问题？我设法找到的所有工作都处理了命令式设置中的计算复杂性,而我对"推理复杂性"和函数式编程感兴趣.

Answer 1

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

您可以在这里获取完整的来源。

最后，

讨论排列的 3 种表示。