4

リストに関するいくつかの定理を証明し、それらからアルゴリズムを抽出しました。ルックアップと連結がより高速であるため、代わりにヒープを使用したいと考えています。これを達成するために私が現在行っていることは、抽出されたリストの種類にカスタム定義を使用することです。これをより正式な方法で行いたいと考えていますが、理想的には、すべての証明をやり直す必要はありません。私がタイプを持っているとしましょう

Heap : Set -> Set

と同型

f : forall A, Heap A -> List A.

さらに、私は関数 H_app と H_nth を持っています。

H_app (f a) (f b) = f (a ++ b)

と

H_nth (f a) = nth a

一方では、すべてのリスト再帰を、リスト再帰を模倣する特殊な関数に置き換える必要があります。一方、事前に++andnthをH_appandH_nthで置き換えたいと思うので、抽出されたアルゴリズムはより高速になります。simpl問題は、いくつかの場所でandのような戦術を使用していることcomputeです。証明コードのすべてを置き換えると、おそらく失敗します。後で関数を「オーバーロード」する可能性があるとよいでしょう。

このようなことは可能ですか？

編集: 明確にするために、同様の問題が数値で発生します: を使用する古い証明がいくつかnatありますが、数値が大きくなりすぎています。使っBinNatたほうがいいのですが、古い証明でもあまり手を加えずにBinNat代わりに使うことはできますか？(特に、 の非効率的な使用法を ?のより効率的な定義にnat置き換えます)+BinNat

4

1 に答える 1

3

わかりやすくするために、次のようにするHeap必要があります。

Inductive Heap A : Type :=
| Node : Heap A -> A -> Heap A -> Heap A
| Leaf : Heap A.

fとして定義されている

Fixpoint f A (h : Heap A) : list A :=
  match h with
  | Node h1 a h2 => f h1 ++ a :: f h2
  | Leaf => []
  end.

この場合、 はとの間の同型を定義 fしません。代わりに、次のような関数を見つけることができます。 Heap Alist AAg : forall A, list A -> Heap A

forall A (l : list A), f (g l) = l

それにもかかわらず、同じ抽象化、つまり何らかのタイプの要素のセットを実装するために使用される場合、両者はある意味で同等であるHeapと言いたいです。list

Coq などのパラメトリック ポリモーフィズムを持つ言語でこのアイデアを検証できる正確かつ正式な方法があります。パラメトリック性として知られるこの原則は、パラメトリックなポリモーフィック関数が、それらをインスタンス化する型に課す関係を尊重することを大まかに述べています。

これは少し抽象的なので、もっと具体的にしましょう。と のみをfoo使用するリストに対する関数 (たとえば) があるとします。パラメトリック性を使用し て同等のバージョンに置き換えることができるようにするには、 の定義をポリモーフィックにし、リスト上の関数を抽象化する必要があります。++nthfooHeapfoo

Definition foo (T : Set -> Set)
               (app : forall A, T A -> T A -> T A)
               (nth : forall A, T A -> nat -> option A)
               A (l : T A) : T A :=
  (* ... *)

リスト上でインスタンス化することにより、最初に foo のプロパティを証明します。

Definition list_foo := foo list @app @nth.

Lemma list_foo_lemma : (* Some statement *).

さて、H_appとH_nthは対応するリストと互換性があり、fooは多相的であるため、パラメトリック性の理論は証明できると言っています

Definition H_foo := foo Heap @H_app @H_nth.

Lemma foo_param : forall A (h : Heap A),
                    f (H_foo h) = list_foo (f h).

list_fooこの補題があれば、 のプロパティを の同様のプロパティに転送できるはずですH_foo。たとえば、簡単な例として、H_appリストへの変換まで、 が連想的であることを示すことができます。

forall A (h1 h2 h3 : Heap A),
  list_foo (H_app h1 (H_app h2 h3)) =
  list_foo (H_app (H_app h1 h2) h3).

パラメトリック性の良いところは、パラメトリックにポリモーフィックな関数に適用されることです : 適切な互換性条件が型に保持されている限り、特定の関数の 2 つのインスタンス化を同様の方法で に関連付けることができるはず foo_paramです。

ただし、2 つの問題があります。1 つ目は、ベース定義をポリモーフィックなものに変更する必要があることですが、これはおそらくそれほど悪くはありません。さらに悪いことに、パラメトリック性により、foo_param特定の条件下などで常に補題を証明できることが保証されますが、Coq はそれを無料で提供するわけではなく、これらの補題を手動で示す必要があります。痛みを和らげるには、次の 2 つの方法があります。

  1. 定型的な証明を自動的に導出するのに役立つ Coq 用のパラメトリック性プラグイン(CoqParam) があります。とはいえ、使ったことがないので、使いやすさはなんとも言えません。

  2. Coq 効果的な代数ライブラリ (略してCoqEAL ) は、パラメトリック性を使用して効率的なアルゴリズムについて証明し、より便利なアルゴリズムについて推論します。特に、あなたが提案したように、natとを切り替えることができる改良点を定義しています。BinNat内部的には、型クラスの推論に基づくインフラストラクチャを使用しており、元の例に適応させることができますが、現在、代わりに CoqParam を使用するように実装を移行していると聞きました。

于 2015-04-26T16:45:26.700 に答える