「効率的な」最低および最高の固定点計算

Question

私はいくつかの列挙型の有限集合（それぞれcharとしましょう）を、最小と最大の固定点計算を使って計算しようとしています。私は自分の定義をSMLに抽出可能にし、実行すると「半効率的」にしたい。私の選択肢は何ですか？

HOLライブラリを探索し、コード生成で遊んでから、私は次の観察を持っている：

1. 私はここで、私のセットを計算するために、追加の単調関数のペアを持つcomplete_lattice.lfpとcomplete_lattice.gfp定数を使用することができます私が現在やっている事実。コード生成はこれらの定数で動作しますが、生成されるコードはひどく非効率的です。生成されたSMLコードが正しく認識されている場合は、文字セット内のすべての可能なセットを網羅的に検索します。どんなに単純なものであっても、タイプcharのこれらの2つの定数を使用すると、実行時に相違が生じます。
2. 私は、Kleene固定点定理によって記述された反復固定点を有向完全部分順序で利用しようとする可能性があります。調べてみると、Complete_Partial_Orderという理論にはccpo_class.fixpという定数がありますが、この意味で定義されているiteratesの定数にはコード式が関連付けられていないため、コードを抽出できません。

私が見逃しているコード生成と半効率的なコードを生成し、有限のセットで使用するのに適してどこかに隠れ、既存の不動点コンビネータは、ありますか？

Answer 1

Isabelleの標準ライブラリの一般的な固定点結合子は、構成が実際には使えないほど一般的であるため、コード抽出に直接使用するものではありません。しかし、理論~~/src/HOL/Library/While_Combinatorは、lfpとgfpの固定点を、あなたが探している反復実装に接続します。lfp_while_latticeとgfp_while_latticeを参照してください。これらの特徴は、関数が単調であることを前提としているため、コード方程式として直接使用することはできません。だから、2つのオプションがあります。

1. あなたのコードの方程式および/または定義に代わりlfp/gfpのwhileコンビネータを使用してください。

2. lfp_while_latticeを[code_unfold]の式として使用するようにコードプリプロセッサに指示します。これは、プリプロセッサが適用する必要があるインスタンスに対して、これらの方程式の仮定を証明するために必要なすべてのルールを追加する場合にも機能します。したがって、という具合、すなわちfinite_class.finiteを証明する定理と関数の単調性ステートメントを[code_unfold]として追加することをお勧めします。