2

私は、ドメインが自然数の有限の「インデックスセット」であり、そのイメージが最大値を定義できる何らかのタイプの関数として、ベクトルのカスタム実装を使用していますreal。たとえば、とを使用して 2 次元ベクトルを作成できvます。v 1 = 2.7v 3 = 4.2

3そのようなベクトルでは、上記の例で、最大コンポーネントのインデックスを教えてくれる「arg max」のような演算子を定義したいと思いますv。「arg max」のような演算子は、値を持つコンポーネントに適用されるタイブレーク関数をさらに受け入れるため、「the」インデックスと言っています。（背景はオークションでの入札です。）

私はMax、有限集合が次を使用して定義されていることを知ってfold1います(それがどのように機能するかはまだわかりません)。私はこれを試しましたが、それ自体は受け入れられましたが、私がやりたかった他のことにはうまくいきませんでした:

fun arg_max_tb :: "index_set ⇒ tie_breaker ⇒ (real vector) ⇒ nat"
where "arg_max_tb N t v = fold1
  (λ x y . if (v x > v y) then x      (* component values differ *)
   else if (v x = v y ∧ t x y) then x (* tie-breaking needed *)
   else y) N"

さらに、「arg max」のような演算子の特定のプロパティを証明したいことに注意してください。これには、誘導が必要になる可能性があります。finite_ne_induct有限集合上の帰納法の法則があることは知っています。わかりましたが、評価できるように演算子を定義できるようにしたいと思います（たとえば、具体的な有限集合を試す場合）が、評価します

value "arg_max_tb {1::nat} (op >) (nth [27::real, 42])"

期待される戻り値1を使用すると、次のエラーが発生します。

Wellsortedness error
(in code equation arg_max_tb ?n ?t ?v \equiv
                  fold1 (\lambda x y. if ord_real_inst.less_real (?v y) (?v x) then ...) ?n):
Type nat not of sort enum
 No type arity nat :: enum

したがって、有限集合をリストに変換することにしました。リストでは、演算子を定義し、そのプロパティの一部を証明することができました (興味がある場合はコードを共有できます) list_nonempty_induct。

作業リストベースの定義は次のようになります。

fun arg_max_l_tb :: "(nat list) ⇒ tie_breaker ⇒ (real vector) ⇒ nat"
where "arg_max_l_tb [] t v = 0"
      (* in practice we will only call the function
         with lists of at least one element *)
    | "arg_max_l_tb [x] t v = x"
    | "arg_max_l_tb (x # xs) t v =
      (let y = arg_max_l_tb xs t v in
        if (v x > v y) then x              (* component values differ *)
        else if (v x = v y ∧ t x y) then x (* tie-breaking needed *)
        else y)"

fun arg_max_tb :: "index_set ⇒ tie_breaker ⇒ (real vector) ⇒ nat"
where "arg_max_tb N t v = arg_max_l_tb (sorted_list_of_set N) t v"

有限集合のコンストラクターに対して関数を直接定義することに成功しませんでした。以下は機能しません。

fun arg_max_tb :: "index_set ⇒ tie_breaker ⇒ (real vector) ⇒ participant"
where "arg_max_tb {} t b = 0"
    | "arg_max_tb {x} t b = x"
    | "arg_max_tb (insert x S) t b =
      (let y = arg_max_tb S t b in
        if (b x > b y) then x
        else if (b x = b y ∧ t x y) then x
        else y)"

エラーメッセージが表示されます

Malformed definition:
Non-constructor pattern not allowed in sequential mode.
⋀t b. arg_max_tb {} t b = 0

これは、リスト コンストラクターが として定義されているdatatypeのに対し、有限集合は単にinductiveスキームとして定義されているためでしょうか?

何であれ、この関数を有限集合上で定義する方法を知っていますか? 直接書き留めるか、折り畳み式のユーティリティ関数を使用しますか?

4

2 に答える 2

3

この質問は実際には複数の質問で構成されています。

有限集合に対する関数の定義

フォールド / フォールドl1

通常の再帰コンビネータはFinite_Set.fold(or fold1) です。ただし、何かを証明できるようにするには、結果が の要素に適用されるfold f z S順序に依存しない必要があります。fS

fが結合的かつ交換可能である場合、 and を使用 しFinite_Set.ab_semigroup_mult.fold1_insert て簡単なFinite_Set.fold1_singletonルールを取得でき、誘導ルールとしてfold1 f S使用できるはずです。finite_ne_induct

ffold1 に与える関数 (私は と呼びます)tは、 が線形順序である場合にのみ可換であることに注意してください。

fun arg_max_tb :: "index_set ⇒ tie_breaker ⇒ (real vector) ⇒ nat"
where "arg_max_tb N t v = fold1
  (λ x y . if (v x > v y) then x      (* component values differ *)
   else if (v x = v y ∧ t x y) then x (* tie-breaking needed *)
   else y) N"

これは、fold1 の既存のレンマではカバーされていないため、一般化されたバリアントを証明するかFinite_Set.ab_semigroup_mult.fold1_insert、追加のタイブレーカーを挿入する必要があります。

   else if (v x = v y ∧ ~t x y ∧ ~t y x ∧ x < y) then x

線形注文の場合t、単純なルールからこの追加のタイ ブレーカーを削除できます。この追加のタイブレーカーは、基本的に を使用して得られるものであることに注意してくださいsorted_list_of_set。

THE / SOME

特定arg_max_tbのプロパティを持つリストの 1 つの要素を選択します。THE x. P xこれは、構文またはSOME x. P x(選択演算子)を使用して直接定義することもできます。前者は、プロパティ P を満たす一意の要素を選択します (一意の要素が存在しない場合、結果は未定義です)。後者は、プロパティ P を満たす要素を選択します (そのような要素が存在しない場合、結果は未定義です)。どちらも無限リストでも機能します。

実行可能コードが必要ない場合は、これらが望ましいことがよくあります。

実行可能な関数の取得

再帰によって定義された関数 (つまりprimrec、funまたはfunction) は、デフォルトで実行可能です (定義で使用されているすべての関数も実行可能である場合)。THE一般にSOME、列挙可能なドメインに対してのみ実行できます（これは、得られたエラーメッセージですvalue--nat有限ではないため、列挙できません）。

ただし、関数の代替定義をいつでもコード ジェネレーターに与えることができます。関数定義のチュートリアル、特に改良に関するセクションを参照してください。

証明のために選択演算子を使用した定式化を好むが、関数を実行可能にしたい場合、最も簡単な方法は、arg_max_tb選択を介して と の定義sorted_list_of_setが同等であることを証明することです。次に、[code_unfold]述語を使用して、選択による定義を (実行可能な) 定義に置き換えることができます。sorted_list_of_set

于 2013-05-23T06:29:58.940 に答える