我希望有一个归纳类型来描述排列及其对某些容器的作用。很明显,根据这个类型的描述,算法的定义复杂度(以长度衡量)(计算组合或逆,分解为不相交的循环等)将会有所不同。
考虑在Coq中以下定义。我认为它是Lehmer编码的形式化:
Inductive Permutation : nat -> Set :=
| nil : Permutation 0
| cons : forall (n k : nat), Permutation (k + n) -> Permutation (k + S n).
对于大小为n的向量,其作用容易定义;对于其他容器稍微困难一些,而且(至少对我来说)在组合或反演的形式化方面也比较难找到。
或者我们可以将置换表示为具有属性的有限映射。组合或反演可以很容易地定义,但将其分解为不相交的循环则很困难。
所以我的问题是:是否有任何论文涉及这种权衡问题?所有我找到的研究都处理命令式设置中的计算复杂性,而我则对“推理复杂性”和函数式编程感兴趣。