「高效」最少和最大固定點計算？

Question

我想分別使用最小和最大固定點計算來計算一些枚舉類型的兩個有限集合（假設爲char）。我希望我的定義能夠被提取到SML，並且在執行時是「半效的」。我有什麼選擇？

從探索HOL庫和代碼生成玩弄，我有以下幾點看法：

1. 我可以使用complete_lattice.lfp和complete_lattice.gfp常數有一對額外的單調函數來計算我的集合，這在其實我現在在做。代碼生成可以處理這些常量，但生成的代碼效率非常低，並且如果我理解正確生成的SML代碼正在對字符的powerset中的每個可能集進行徹底搜索。因此，char類型的這兩個常量的任何使用（無論多麼簡單）都會在執行時導致分歧。
2. 我可以嘗試利用Kleene不動點定理所描述的迭代不動點的定向完整偏序。從探索的角度來看，理論Complete_Partial_Order中有一個ccpo_class.fixp常量，但是其中定義的常量不存在相關的代碼方程，因此無法提取代碼。

是否有任何現有的固定點組合器隱藏在某處，適合用於有限集合，生成我已經錯過的代碼生成的半高效代碼？

Answer 1

Isabelle標準庫中的一般定點組合器都不是用來直接用於代碼提取的，因爲它們的構造過於普遍而無法在實踐中使用。 （理論~~/src/HOL/Library/Bourbaki_Witt_Fixpoint中有另一個。）但理論~~/src/HOL/Library/While_Combinator將lfp和gfp固定點連接到您正在查找的迭代實施，請參閱定理lfp_while_lattice和gfp_while_lattice。這些特徵具有函數是單調的前提條件，因此它們不能直接用作代碼方程。所以，你有兩個選擇：

1. 使用while組合子，而不是lfp/gfp代碼中的公式和/或定義。

2. 通知代碼預處理器使用lfp_while_lattice作爲[code_unfold]公式。如果您還添加了預處理器需要的所有規則以證明這些方程的假設適用於它的實例，那麼這會起作用。因此，我建議您也添加[code_unfold]函數的單調性陳述和證明char set的有限性的定理，即finite_class.finite。