关于排列的表示

Posted 2023-02-15

【中文标题】关于排列的表示

【英文标题】：On representations of permutations

【发布时间】：2013-06-30 01:58:45

【问题描述】：

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

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

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

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

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

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

【问题讨论】：

我对 Coq 一无所知，但这有帮助吗？ coq.inria.fr/stdlib/Coq.Sorting.Permutation.html

不幸的是，它没有。我想要的是不参考容器的排列编码。尽管有一个与上述相似的关系的容器通用定义会很愉快。

也许您可以对其进行专门化，以便排列一个排序的索引列表？

另一个对我来说效果很好的表示是我在github.com/copumpkin/containers/blob/master/… 中使用的。不幸的是，它没有像双射那样简单的组合概念。

这可能会在cs.stackexchange.com上获得更多关注

【参考方案1】：

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

http://s-s-r2.msr-inria.inria.fr/doc/s-s-reflect-1.4/Ssreflect.seq.html

您可以在此处获取完整的资源。

http://research.microsoft.com/en-us/downloads/5464E7B1-BD58-4F7C-BFE1-5D3B32D42E6D/default.aspx

最后，

http://comments.gmane.org/gmane.science.mathematics.logic.coq.club/4193

讨论排列的 3 种表示。