代码之家 › 专栏 › 技术社区 › Dominic Mulligan

“高效”最小和最大不动点计算?

isabelle

0

Dominic Mulligan · 技术社区 · 7 年前

我试图计算一些可枚举类型的两个有限集(例如 char )分别使用最小和最大不动点计算。我希望我的定义可以提取到SML,并且在执行时是“半有效的”。我有什么选择?

通过探索HOL库和代码生成,我有以下观察结果:

complete_lattice.lfp 和 complete_lattice.gfp 常数和一对额外的单调函数来计算我的集合,事实上我现在正在做。代码生成确实可以使用这些常量,但生成的代码效率极低,如果我正确理解生成的SML代码,则会对字符幂集中的每个可能集执行穷举搜索。这两个常量在类型因此,在执行时会导致分歧。
我可以尝试在有向完全偏序中使用克莱恩不动点定理描述的迭代不动点。从探索中,有一个 ccpo_class.fixp 理论中的常数 Complete_Partial_Order iterates 根据定义的常数没有关联的代码方程,因此无法提取代码。

是否有任何现有的不动点组合隐藏在某个地方,适合用于有限集,可以生成我错过的半有效代码生成?

1 回复 | 直到 7 年前

1

Andreas Lochbihler 7 年前

Isabelle标准库中的通用不动点组合器都不打算直接用于代码提取,因为它们的构造过于通用,无法在实践中使用。(理论中还有一个 ~~/src/HOL/Library/Bourbaki_Witt_Fixpoint )但是理论 ~~/src/HOL/Library/While_Combinator lfp 和 gfp 您正在寻找的迭代实现的不动点,请参见定理 lfp_while_lattice gfp_while_lattice 这些特征具有函数单调的前提,因此不能直接用作代码方程。所以你有两个选择:

使用 while / 绿色荧光蛋白 在代码方程和/或定义中。
告诉代码预处理器使用 [code_unfold] 方程式如果您还添加了预处理器需要的所有规则,以证明这些方程的假设适用于它应该应用的实例,那么这是可行的。因此,我建议您也添加为 [代码展开] 函数的单调性陈述和证明函数有限性的定理 char set finite_class.finite .