1

Isabelle/HOL理論マニュアルからコード生成を読みました。しかし、私はまだ少し迷っています。どこにあるのlinorder？たとえば、赤黒木を使用して処理を高速化するにはどうすればよいですか？localeプログラムの改良の文脈でどのように使用されますか？..。

改良を始めるためのチュートリアルはありますか？そうでない場合は、短い、自己完結型の正しい例がありますか？

例を開発できますか？

A :: 'a set私たちが持っていて、知っていると仮定しましょうfinite A。たとえば、の効率的なコードを生成するにはどうすればよいですa ∈ Aか？

の知識をどのように表現しますかfinite A。a ∈ A数学的理論（ ）をコード生成および最適化から分離するにはどうすればよいですか？

4

1 に答える 1

1

さて、私はこの質問に答えるために最善を尽くします。コメントや編集をして、改善してください。カルマが必要な場合は、この回答をコピーして再投稿することもできます（回答が優れている場合は、回答を削除します）。

このユーザーガイドは私が始めるのを助けました。

さて、私たちの理論がにあると仮定しましょうlocale MyLocale。

locale MyLocale =
  fixes A :: "'a set"
  begin
    definition isInA :: "'a => bool" where
      "isInA a ⟷ a ∈ A"
  end

isInAロケールをで実装することで関数を実装するとset Aしますlist。次に、コードを生成してその正しさを示すことができます

definition code_isInA_list :: "'a list => 'a => bool"
  where "code_isInA_list Al a ⟷ a ∈ set Al"

lemma code_isInA_list_correct: 
 "code_isInA_list Al a = MyLocale.isInA (set Al) a"
  by(simp add: MyLocale.isInA_def code_isInA_list_def)

export_code code_isInA_list in Scala file -

これにより、基本的に次のScalaコードが生成されます

def code_isInA_list[A : HOL.equal](al: List[A], a: A): Boolean =
  Lista.member[A](al, a)

Lista.member関数は線形時間アルゴリズムです。もっと上手くできますか？

linorderタイプにが付いていると仮定しましょう'a。たとえば、linorder自然数、文字列、リスト、タプルなどがあります。この仮定は、'a ::linorderの代わりに書くことで表現し'aます。プロパティを活用できるデータ型の1つlinorderは、赤黒木です。私たちのロケールでは、Aでしたset。セットでは、要素の順序は重要ではありません。したがって、リストの代わりに、より効率的な赤黒木を使用できます。リストは固定された順序を指示しますが、要素は任意に順序付けることができるため、赤黒木はリストよりも効率的です。赤黒木を使用するには、正式な証明のアーカイブからコレクションフレームワークをインポートします。thy-fileの先頭で、importsセクションに追加します

"./isabelle_afp/Collections/Collections"

これで、赤黒木（rs）バージョンを実装し、その正しさを示すことができます。コレクションフレームワークの関数rs_α（alpha<tab>アルファ版の場合はjEditと入力）は、赤黒木を対応するセットにマップします。

definition code_isInA_rs :: "('a ::linorder) rs => 'a => bool"
  where "code_isInA_rs Al a ⟷ rs_memb a Al"

lemma code_isInA_rs_correct: 
 "code_isInA_rs Ars a = MyLocale.isInA (rs_α Ars) a"
  by(simp add: MyLocale.isInA_def code_isInA_rs_def rs_correct)

export_code code_isInA_rs in Scala file -

次のコードを生成します

def code_isInA_rs[A : Orderings.linorder](al: RBT.rbt[A, Unit], a: A): Boolean =
  RBTSetImpl.rs_memb[A].apply(a).apply(al)

このrs_memb関数には対数実行時間があります。TODO：本当に？どこで調べられますか？

コードをさらに改善しましょう。コードではリストの方が簡単なので、バージョンに固執したいとしcode_isInA_listます。code_isInA_listの観点から実装できますcode_isInA_rs。したがって、これを使用list_to_rsしてリストを赤黒木に変換します。この[code]属性を使用して、コードジェネレーターに新しいバージョンを使用するように指示します。

lemma [code]: "code_isInA_list Al a ⟷ code_isInA_rs (list_to_rs Al) a"
  by(simp add: code_isInA_list_def code_isInA_rs_def rs_correct)

export_code code_isInA_list in Scala file -

次のコードを生成します。

def code_isInA_list[A : Orderings.linorder](al: List[A], a: A): Boolean =
  code_isInA_rs[A](RBTSetImpl.list_to_rs[A].apply(al), a)

赤黒を作成してからルックアップを実行すると、単純なリストバージョンよりもコストがかかると思いますが、これは単なる例です。より多くのルックアップが必要な場合は、赤黒木バージョンの方が間違いなく効率的です。

IsabellejEditのコードをいくつかのタイプでテストしてみましょう。自然数から始めます。

value[code] "code_isInA_list [(1::nat), 3, 7, 4] 4"

これにより、True

次に、文字列を試してみます。

value[code] "code_isInA_list [''a'', ''b'', ''xyz''] ''b''"

これにより、

Wellsortedness error:
  Type char list not of sort linorder
  No type arity list :: linorder

エラーメッセージはlinorder、タイプにnoが定義されていることを示していstringます。そこで、以下の理論をインポートします。

"~~/src/HOL/Library/List_lexord"
"~~/src/HOL/Library/Code_Char"
"~~/src/HOL/Library/Code_Char_chr"
"~~/src/HOL/Library/Code_Char_ord"

これで、目的の結果が得られますTrue。このコードはタプルでも機能します。

value[code] "code_isInA_list [(''a'', ''a''), (''b'', ''c''), (''xyz'', '''')] (''b'', ''c'')"
于 2013-03-27T19:20:40.807 に答える