"Efficient" 最小和最大固定点计算？
"Efficient" least- and greatest fixpoint computations?
我正在尝试分别使用最小和最大固定点计算来计算某些可枚举类型的两个有限集（比方说 char）。我希望我的定义可提取到 SML，并在执行时为 "semi-efficient"。我有哪些选择？
通过探索 HOL 库和代码生成，我有以下观察结果：
- 我可以使用
complete_lattice.lfp 和 complete_lattice.gfp 常量以及一对额外的单调函数来计算我的集合，事实上我目前正在这样做。代码生成确实使用这些常量，但生成的代码效率低得可怕，如果我正确理解生成的 SML 代码，则会对字符的幂集中的每个可能集执行详尽搜索。因此，无论多么简单，对 char 类型的这两个常量的任何使用都会导致执行时出现分歧。
- 我可以尝试在有向完全偏序中使用 Kleene 不动点定理描述的迭代不动点。通过探索，理论
Complete_Partial_Order中有一个ccpo_class.fixp常数，但是根据它定义的基础iterates常数没有相关的代码方程，因此无法提取代码。
是否有任何现有的固定点组合器隐藏在某处，适合与有限集一起使用，产生我错过的带有代码生成的半高效代码？
Isabelle 的标准库中的 None 通用定点组合器旨在直接用于代码提取，因为它们的构造过于通用，无法在实践中使用。 （理论~~/src/HOL/Library/Bourbaki_Witt_Fixpoint中还有一个。）但是理论~~/src/HOL/Library/While_Combinator将lfp和gfp固定点连接到您正在寻找的迭代实现，参见定理lfp_while_lattice 和 gfp_while_lattice。这些刻画的前提是函数是单调的，因此不能直接作为代码方程使用。所以你有两个选择：
在您的代码方程式 and/or 定义中使用 while 组合器代替 lfp/gfp。
告诉代码预处理器使用 lfp_while_lattice 作为 [code_unfold] 等式。如果您还添加预处理器需要的所有规则来证明这些方程的假设适用于它应该应用的实例，那么这将起作用。因此，我建议您还添加 [code_unfold] 函数的单调性声明和证明 char set 有限性的定理，即 finite_class.finite.
我正在尝试分别使用最小和最大固定点计算来计算某些可枚举类型的两个有限集（比方说 char）。我希望我的定义可提取到 SML，并在执行时为 "semi-efficient"。我有哪些选择？
通过探索 HOL 库和代码生成，我有以下观察结果：
- 我可以使用
complete_lattice.lfp和complete_lattice.gfp常量以及一对额外的单调函数来计算我的集合，事实上我目前正在这样做。代码生成确实使用这些常量，但生成的代码效率低得可怕，如果我正确理解生成的 SML 代码，则会对字符的幂集中的每个可能集执行详尽搜索。因此，无论多么简单，对char类型的这两个常量的任何使用都会导致执行时出现分歧。 - 我可以尝试在有向完全偏序中使用 Kleene 不动点定理描述的迭代不动点。通过探索，理论
Complete_Partial_Order中有一个ccpo_class.fixp常数，但是根据它定义的基础iterates常数没有相关的代码方程，因此无法提取代码。
是否有任何现有的固定点组合器隐藏在某处，适合与有限集一起使用，产生我错过的带有代码生成的半高效代码？
None 通用定点组合器旨在直接用于代码提取，因为它们的构造过于通用，无法在实践中使用。 （理论~~/src/HOL/Library/Bourbaki_Witt_Fixpoint中还有一个。）但是理论~~/src/HOL/Library/While_Combinator将lfp和gfp固定点连接到您正在寻找的迭代实现，参见定理lfp_while_lattice 和 gfp_while_lattice。这些刻画的前提是函数是单调的，因此不能直接作为代码方程使用。所以你有两个选择：
在您的代码方程式 and/or 定义中使用
while组合器代替lfp/gfp。告诉代码预处理器使用
lfp_while_lattice作为[code_unfold]等式。如果您还添加预处理器需要的所有规则来证明这些方程的假设适用于它应该应用的实例，那么这将起作用。因此，我建议您还添加[code_unfold]函数的单调性声明和证明char set有限性的定理，即finite_class.finite.