Polymorphismus und induktive Datentypen

Ich bin neugierig. Ich habe an diesem Datentyp in OCaml gearbeitet :

type 'a exptree =
  | Epsilon
  | Delta of 'a exptree * 'a exptree
  | Omicron of 'a
  | Iota of 'a exptree exptree

Was mit explizit typisierten rekursiven Funktionen bearbeitet werden kann (eine Funktion, die erst kürzlich hinzugefügt wurde). Beispiel:

let rec map : 'a 'b. ('a -> 'b) -> 'a exptree -> 'b exptree =
  fun f ->
    begin function
    | Epsilon -> Epsilon
    | Delta (t1, t2) -> Delta (map f t1, map f t2)
    | Omicron t -> Omicron (f t)
    | Iota tt -> Iota (map (map f) tt)
    end

Aber ich konnte es nie in Coq definieren :

Inductive exptree a :=
  | epsilon : exptree a
  | delta : exptree a -> exptree a -> exptree a
  | omicron : a -> exptree a
  | iota : exptree (exptree a) -> exptree a
.

Coq jammert. Es mag den letzten Konstruktor nicht und sagt etwas, das ich nicht vollständig verstehe oder dem ich nicht zustimme:

Error: Non strictly positive occurrence of "exptree" in "exptree (exptree a) -> exptree a".

Was ich verstehen kann ist, dass induktive Typen, die eine Negation innerhalb ihrer Definition verwenden, type 'a term = Constructor ('a term -> …)abgelehnt werden, weil sie zu hässlichen, nicht fundierten Tieren wie (untypisierten) λ-Begriffen führen würden. Dieser spezielle exptreeDatentyp scheint jedoch harmlos genug zu sein: Wenn man sich seine OCaml- Definition ansieht , wird sein Argument 'aniemals in negativen Positionen verwendet.

Es scheint, dass Coq hier übervorsichtig ist. Gibt es also wirklich ein Problem mit diesem speziellen induktiven Datentyp? Oder könnte Coq hier etwas freizügiger sein?

Und was ist mit anderen Beweisassistenten, die in der Lage sind, mit einer solchen induktiven Definition (auf natürliche Weise) umzugehen?

Dies ist mehrmals auf der Coq-Mailingliste aufgetaucht, aber ich habe nie eine endgültige Antwort gesehen. Coq ist nicht so allgemein wie es sein könnte; Die Regeln in (Coquand, 1990) und (Giménez, 1998) (und seiner Doktorarbeit) sind allgemeiner und erfordern keine strikte Positivität. Positivität genug ist jedoch nicht genug, wenn Sie nach draußen gehen Set; Dieses Beispiel wurde in mehreren Diskussionen angesprochen :

Inductive Big : Type := B : ((B -> Prop) -> Prop) -> Big.

Bei einfachen Datenstrukturen wie Ihrer würde der induktive Typ keine anderen Probleme verursachen, als die Implementierung komplexer zu machen.

Es gibt eine allgemeine Möglichkeit, Typen wie diesen zu definieren, die als Fixpunkt eines Polynoms definiert sind:

$$F = \epsilon + \delta\, (F \times F) + \omicron\, \mathrm{id} + F \circ F$$

Anstatt zu versuchen, die Funktion zu definieren , definieren Sie die Familie der Typen . Dies bedeutet, dass dem Typ, der die Anzahl der Selbstkompositionen codiert, ein ganzzahliger Parameter hinzugefügt wird ( , , usw.) und ein zusätzlicher Injektionskonstruktor, um in .$\mathrm{exptree} : a \mapsto \mathrm{exptree}(a)$$\mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree}, \mathrm{exptree} \circ \mathrm{exptree} \circ \mathrm{exptree}, \ldots$$\mathrm{exptree}^0(a) = a$$\mathrm{exptree}^1(a) = \mathrm{exptree}(a)$a e x p t r e e 0 ( a ) = $\mathrm{exptree}^2(a) = \mathrm{exptree}(\mathrm{exptree}(a))$$a$$\mathrm{exptree}^0(a) = a$

Inductive et : nat -> Type -> Type :=
  | alpha : forall a, a -> et 0 a                      (*injection*)
  | omicron : forall n a, et n a -> et (S n) a         (**)
  | epsilon : forall (S n) a, et (S n) a
  | delta : forall n a, et (S n) a -> et (S n) a -> et (S n) a
  | iota : forall n a, et (S (S n)) a -> et (S n) a
.

Sie können fortfahren, Werte zu definieren und daran zu arbeiten. Coq kann oft auf den Exponenten schließen. Set Implicit Argumentswürde diese Definitionen schöner machen.

Definition exptree := et 1.
Definition et1 : exptree nat :=
  delta _ _ (omicron _ _ (alpha _ 42)) (epsilon _ _).
Definition et2 : exptree nat := iota _ _ (omicron _ _ et1).

Sie können es vorziehen , das Argument von 1 zu verringern, so daß exptreeist et 0. Dies entfernt viel von S nder Definition, was einige Beweise erleichtern kann, erfordert jedoch die Aufteilung des Anfangsfalls vom Wiederholungsfall in jedem Konstruktor, der ein in einem Argument verwendet (anstatt einen einzelnen Injektionskonstruktor für hinzuzufügen ). In diesem Beispiel muss nur ein einziger Konstruktor aufgeteilt werden. Dies sollte daher eine gute Wahl sein.$a$$a$

Inductive et : nat -> Type -> Type :=
  | omicron_0 : forall a, a -> et 0 a
  | omicron_S : forall n a, et n a -> et (S n) a
  | epsilon : forall n a, et n a
  | delta : forall n a, et n a -> et n a -> et n a
  | iota : forall n a, et (S n) a -> et n a
.
Definition exptree := et 0.
Definition et1 : exptree nat :=
  delta _ _ (omicron_0 _ 42) (epsilon _ _).
Definition et2 : exptree nat :=
  (iota _ _ (omicron_S _ _ et1)).

Ich denke, dies ist das gleiche Prinzip, das Ralph Mattes in einer allgemeineren Form vorgeschlagen hat .

Verweise

Thierry Coquand und Christine Paulin. Induktiv definierte Typen . In Proceedings of COLOG'88 , LNCS 417, 1990. [ Springer ] [ Google ]

Eduardo Giménez. Strukturelle rekursive Definitionen in der Typentheorie . In ICALP'98: Vorträge des 25. Internationalen Kolloquiums über Automaten, Sprachen und Programmierung. Springer-Verlag, 1998. [ PDF ]

Ralph Matthes beschreibt in Coq in "Eine Datenstruktur für iterierte Kräfte" ( Code , Papier ), wie solche Typen in Coq simuliert werden .

Eines der ersten Dinge, die Coq tut, ist das Aufbau des Induktionsprinzips, das mit dem soeben definierten induktiven Typ verbunden ist, und das Verständnis des zugrunde liegenden Induktionsprinzips ist eine gute Übung.

Zum Beispiel O : nat | S : nat -> natwird das Induktionsprinzip erzeugt P O -> (∀ n, P n -> P (S n)) -> ∀ n, P n.

Wem würde das Induktionsprinzip entsprechen iota? Es scheint, dass es kein Prädikat gibt P, über das man sprechen könnte, P tund P (iota t)weil es darüber sprechen exptree asollte exptree (exptree a), exptree (exptree (exptree a))...

Auch das Omicronmacht das gleiche, aber der Typ ist jedes Mal kleiner. Sie sollten das Gefühl haben, dass ein Verweis auf einen kleineren und einen größeren Typ die Dinge chaotisch machen würde. (Das heißt, Omicronist der richtige Weg)

Das sind nicht die genauen Kriterien, die besagen, warum die Definition nicht akzeptiert werden sollte, aber dies erklärt, warum sie sich für mich falsch anfühlt.

exptreeEs scheint, als würden Sie eine Grammatik für Ausdrücke erstellen, was im Allgemeinen nicht so rekursiv ist. Willst du etwas Hilfe dabei?