2

タイプに対してポリモーフィックな可変ファンアウトを持つ加重ツリーを定義したいと考えています。私はこれを思いつきました：

(* Weighted tree with topological ordering on the nodes. *)
Inductive wtree (A : Type) : Type :=
  LNode : A->wtree A
| INode : A->list (R*wtree A) -> wtree A.

ただし、次のようなタイプに重みを格納することをお勧めします。

Inductive Wtype (A : Type) : Type := W : R->A->Wtype A.
Inductive wtree (A : Wtype) : Type :=
  LNode : A->wtree A
| INode : A->list (wtree A) -> wtree A.

ここRで、標準ライブラリからの実数のセットです。

はではなく であるため、これは機能しませんWtypeが、これを行う方法がわかりません。残念ながら、私はまだオブジェクト指向の世界に住んでおり、より制限的なスーパータイプを に与えたいだけなのですが、Coq でそれを行う方法がわかりません。Type->TypeTypeAType

4

2 に答える 2

2

問題は、WtypeそうType -> Typeですか。適用できないので、なんらかの引数を与える必要があります。したがって、それをいくつかの引数に適用する必要があります。これに対する簡単な解決策は、

Inductive wtree' (A : Type) : Type :=
| LNode : A -> wtree' A
| INode : A -> list (wtree' A) -> wtree A.

Inductive Wtype (A : Type) : Type := W : R -> A -> Wtype A.

Definition wtree (A : Type) := wtree' (Wtype A).
于 2013-11-09T21:06:55.270 に答える