1

この質問は、Isabelle/HOL定理証明者によるコード生成に関するものです。

distinctリスト上の関数のコードをエクスポートするとき

export_code distinct in Scala file -

次のコードを取得します

def member[A : HOL.equal](x0: List[A], y: A): Boolean = (x0, y) match {
  case (Nil, y) => false
  case (x :: xs, y) => HOL.eq[A](x, y) || member[A](xs, y)
}

def distinct[A : HOL.equal](x0: List[A]): Boolean = x0 match {
  case Nil => true
  case x :: xs => ! (member[A](xs, x)) && distinct[A](xs)
}

このコードには2次ランタイムがあります。より高速なバージョンはありますか？理論の最初に文字列をインポート"~~/src/HOL/Library/Code_Char"するようなものを考えており、リストの効率的なコード生成が設定されています。のより良い実装はdistinct、O（n log n）でリストをソートし、リストを1回繰り返すことです。しかし、私は人がもっとうまくいくことができると思いますか？

とにかく、利用可能なdistinct他の関数のより高速な実装はありMainますか？

4

1 に答える 1

7

Isabelle2013 のライブラリでのより高速な実装については知りませんが、次のように自分で簡単に実装できます。

  1. distinct_sortedソートされたリストの識別性を判断する関数を実装します。
  2. ソートされたリストでdistinct_sorted実際に実装されていることを証明するdistinct
  3. distinctviaとsort を実装する補題を証明し、distinct_listそれを の新しいコード方程式として宣言しdistinctます。

要約すると、これは次のようになります。

context linorder begin
fun distinct_sorted :: "'a list => bool" where
  "distinct_sorted [] = True"
| "distinct_sorted [x] = True"
| "distinct_sorted (x#y#xs) = (x ~= y & distinct_sorted (y#xs))"

lemma distinct_sorted: "sorted xs ==> distinct_sorted xs = distinct xs"
  by(induct xs rule: distinct_sorted.induct)(auto simp add: sorted_Cons)
end

lemma distinct_sort [code]: "distinct xs = distinct_sorted (sort xs)"
 by(simp add: distinct_sorted)

次に、効率的な並べ替えアルゴリズムが必要です。デフォルトでsortは、挿入ソートを使用します。HOL/LibraryからMultisetをインポートsortすると、クイックソートで実装されます。Archive of Formal Proofs からEfficient Mergesortをインポートすると、マージ ソートが得られます。

distinctこれにより効率が向上しますが、問題もあります。上記の宣言の後では、要素が型 class のインスタンスであるリストに対してのみ実行できますlinorder。この改良はコード ジェネレーター内でのみ行われるため、Isabelle での定義と定理は影響を受けません。

たとえばdistinct、任意のコード方程式でリストのリストに適用するには、最初にリストの線形順序を定義する必要があります。これは、辞書式順序を選択することによって行われますが、これには要素の線形順序が必要ですList_lexord。HOL/Libraryを使用する場合はstring、 を省略して、通常の順序を定義しchar listます。で対象言語の文字種に文字をマッピングする場合、 との組み合わせに対する適応理論も必要です。Char_ordcharCode_CharCode_Char_ordChar_ord

于 2013-03-21T11:22:38.897 に答える