关于排列的表示方法

Question

26

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

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

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

对于大小为n的向量，其作用容易定义；对于其他容器稍微困难一些，而且（至少对我来说）在组合或反演的形式化方面也比较难找到。

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

所以我的问题是：是否有任何论文涉及这种权衡问题？所有我找到的研究都处理命令式设置中的计算复杂性，而我则对“推理复杂性”和函数式编程感兴趣。

- Katty J.

2

我对Coq一无所知，但这个链接有帮助吗？http://coq.inria.fr/stdlib/Coq.Sorting.Permutation.html - Sjoerd Visscher

1

很遗憾，它没有。我想要的是排列的编码，而不涉及容器。虽然拥有类似提到的关系的通用容器定义会很好。 - Katty J.

1

也许你可以将其专门化，使其对排好序的索引列表进行置换？ - Sjoerd Visscher

我认为你应该在Coq邮件列表（coq-club）上提出你的问题，这样你可能会联系到更多能够回答它的人。 - Vinz

3

我用过的另一种表达方式是 https://github.com/copumpkin/containers/blob/master/CommutativeSemigroup.agda#L30 中使用的方法，效果还不错。不幸的是，它并没有像双射那样简单的组合概念。 - copumpkin

1

这可能会在http://cs.stackexchange.com/上获得更多关注。 - Zac Thompson

1个回答

网页内容由stack overflow 提供, 点击上面的

可以查看英文原文，
原文链接

- seanmcl · Accepted Answer

乔治·冈蒂耶为证明四色定理和费特-汤普森定理而广泛研究排列。他的Coq ssreflect包通过在Coq中使用计算而不是策略来促进对排列的推理，尤其是有限集上的排列。他的seq库是入口点。

在这里可以获取完整的源代码。

最后，

讨论排列的三种表示方法。