2

私はCoqが初めてです。単位、積、合計を使用してリスト、マップ、ツリーを定義するのに問題があります。タイトルのエラーメッセージが表示されます。コメントの上のコードは正常に機能しますが、その下のコードは機能しません。

Inductive one : Type := nil : one.

Inductive sum (t0 t1 : Type) : Type :=
  | inject_left : t0 -> sum t0 t1
  | inject_right : t1 -> sum t0 t1.

Inductive product (t0 t1 : Type) : Type := pair : t0 -> t1 -> product t0 t1.

Definition list (t0 : Type) : Type := sum one (product t0 (list t0)).

Definition map (t0 t1 : Type) : Type := list (product t0 t1).

(* From here on nothing works. *)

Definition List (t0 : Type) : Type := sum one (product t0 (List t0)).

Definition map (t0 t1 : Type) : Type :=
  sum one (product (product t0 t1) (map t0 t1)).

Definition Map (t0 t1 : Type) : Type :=
  sum one (product (product t0 t1) (Map t0 t1)).

Definition tree (t0 : Type) : Type :=
  sum one (product t0 (product (tree t0) (tree t0))).

Definition Tree (t0 : Type) : Type :=
  sum one (product t0 (product (Tree t0) (Tree t0))).
4

1 に答える 1

2 
Definition List (t0 : Type) : Type := sum one (product t0 (List t0)).

Coq では、 を使用して再帰関数を記述することはできません。Definition使用する必要がありますFixpoint(またはより強力なもの)。http://coq.inria.fr/refman/Reference-Manual003.html#@command14を参照してください。

それだけではありませんが、再帰的な定義は証明可能に終了する必要があります (使用するロジックの一貫性を確保するため)。特に、次のようなものは記述できません。

Fixpoint List (t0 : Type) : Type := sum one (product t0 (List t0)).

入ったのと同じ引数で再帰呼び出しを行っているため、これは明らかに終了に失敗します。

とにかく、これらのような型を定義するには、おそらくInductive(and CoInductive) を使用する必要があります。

于 2012-07-02T05:24:19.010 に答える