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是标准库中的实数集。

这不起作用，因为Wtypeis a Type->Type， not a Type，但我不知道如何做到这一点。不幸的是，我仍然生活在面向对象的领域，我真的只是想给Athan提供一个更严格的超级类型Type，但就是不知道如何在 Coq 中做到这一点。

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 回答
1

我想我已经解决了这个问题：

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

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

然而，似乎最好能说一些更像的东西Inductive wtree (A : WType) ...，并避免Wtype A在整个定义中用大量的“”来混淆定义。

于 2013-11-09T15:59:16.030 回答