gpt4 book ai didi

types - 关于置换的表示

转载 作者:行者123 更新时间:2023-12-03 10:43:38 25 4
gpt4 key购买 nike

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

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

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

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

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

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

最佳答案

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

http://ssr2.msr-inria.inria.fr/doc/ssreflect-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 种表示。

关于types - 关于置换的表示,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/17430023/

25 4 0
Copyright 2021 - 2024 cfsdn All Rights Reserved 蜀ICP备2022000587号
广告合作:1813099741@qq.com 6ren.com