Warum sind sich Agda und Coq nicht einig über strikte Positivität?

Ich bin auf eine verwirrende Meinungsverschiedenheit zwischen Agda und Coq gestoßen, die offensichtlich nicht mit den bekanntesten Unterscheidungen zwischen ihren Typentheorien zusammenhängt (z. B. (Im-) Prädikativität, Induktionsrekursion usw.).

Insbesondere wird die folgende Definition von Agda akzeptiert:

  data Ty : Set0 -> Set0 where
    c1 : Ty ℕ
    c2 : Ty (Ty ℕ)

wohingegen die äquivalente Coq-Definition verworfen wird, weil das Erscheinen von [Ty_] als Index von sich selbst in c2 als Verstoß gegen die strikte Positivität angesehen wird.

  Inductive Ty : Set -> Set :=
    | c1 : Ty nat
    | c2 : Ty (Ty nat).

In der Tat ist dieser Fall fast wörtlich ein Beispiel aus Coq'Art Abschnitt 14.1.2.1 für die Verletzung strikter Positivität:

  Inductive T : Set -> Set := c : (T (T nat)).

Aber ich sehe keine Gründe für diesen Unterschied zwischen den Typentheorien. Das klassische Beispiel, Falsch zu beweisen, indem ein negatives Vorkommen eines Typs in einem Konstruktorargument verwendet wird, ist für mich klar, aber ich kann nicht sehen, wie man aus diesem Indexierungsstil einen Widerspruch ableiten kann (unabhängig von ansonsten ausschließlich positiven Konstruktorargumenten).

In Dybjers Artikel über frühe induktive Familien wird die Lösung von Paulin-Mohring im CID-Artikel mit geringfügig unterschiedlichen Einschränkungen aus der Literatur heraus kommentiert, und es wird vage vermutet, dass die Unterschiede im Zusammenhang mit Impredikativität stehen könnten, sie werden jedoch nicht weiter ausgeführt. Dybjers Papier scheint dies zuzulassen, während Paulin-Mohrings es eindeutig verbietet.

Anscheinend bin ich nicht der erste, der diese Meinungsverschiedenheit bemerkt, und einige glauben, dass diese Definition in beiden Systemen nicht zulässig sein sollte ( https://lists.chalmers.se/pipermail/agda/2012/004249.html ), aber Ich habe keine Erklärung dafür gefunden, warum es entweder in einem System klingt, aber nicht in dem anderen, oder nur eine Meinungsverschiedenheit.

Ich habe also vermutlich mehrere Fragen:

1. Ist dies ein Beispiel für einen monotonen, aber nicht streng positiven Typ? (In Coq; eindeutig hält Agda es für streng positiv)
2. Warum erlaubt Agda dies, während Coq es ablehnt? Es ist einfach ein eigenwilliger Unterschied in der Interpretation von "streng positiv". Gibt es einen subtilen Unterschied zwischen Coq und Agda, der es in Agda klingen lässt und in Coq nicht klingt, oder ist es eine Geschmackssache, die von bestimmten theoretischen Vorlieben bestimmt wird?
3. Gibt es einen signifikanten Unterschied zwischen der obigen ersten Definition und der äquivalenten induktiv-rekursiven Definition?

Induktiv-rekursive Definition:

  mutual
    data U : Set0 -> Set0 where
      c : (i : Fin 2) -> U (T i)
    T : Fin 2 -> Set0
    T zero = ℕ
    T (suc zero) = U ℕ

Ich freue mich über Hinweise auf relevante Literatur.

Danke im Voraus.

Das Problem scheint eine Verwirrung zu sein, die sich aus einem Zusammentreffen zweier Faktoren ergibt:

1. Ich habe eine veraltete Version von Agda (2.3.0.1) verwendet. Es scheint, dass Agda vor 2.3.2 einfach nicht die strikte Positivität der Indizes der Konstruktorergebnisse überprüft hat (siehe den Fehler, den ich an anderer Stelle im Thread verlinkt habe).
2. Eine genauere Lektüre von Dybjers Arbeit über induktive Familien legt nahe, dass er möglicherweise beabsichtigt hat, dass der zu definierende induktive Typ beim Eingeben der Indizes eines Konstruktorergebnisses nicht gebunden wird . Abschnitt 3.2.1 gibt das Schema für induktive Konstruktoren in Prosa an, und anscheinend habe ich die Sprache, die die Bindungsumgebungen für jeden Teil des Schemas beschreibt, falsch verstanden.

Diese nähere Betrachtung steht natürlich im Einklang mit der Überprüfung, die Coq und (neuere Versionen von) Agda durchführen und die das Auftreten von T in ihren eigenen Indizes verbieten.

Ein möglicher Grund für den Unterschied ist, wie Ihre eigenen Bemerkungen andeuten, die Ungenauigkeit. Coq hatte historisch gesehen ein beeindruckendes Set (ich glaube immer noch als Flagge erhältlich!)

Zitiert das Buch von Adam Chlipala http://adam.chlipala.net/cpdt/html/Universes.html

Die Coq-Tools unterstützen ein Befehlszeilen-Flag -impredicative-set, das Gallina grundlegender modifiziert, indem Set improvisiert wird. Ein Begriff wie für T: Set, T hat den Typ Set, und induktive Definitionen in Set können Konstruktoren enthalten, die über Argumente beliebigen Typs quantifizieren. Um die Konsistenz aufrechtzuerhalten, muss eine Eliminierungsbeschränkung eingeführt werden, ähnlich der Einschränkung für Prop. Die Einschränkung gilt nur für große induktive Typen, bei denen einige Konstruktoren über einen Typ des Typs Type quantifizieren. In solchen Fällen kann ein Wert in diesem induktiven Typ nur über ein Muster abgeglichen werden, um einen Ergebnistyp zu erhalten, dessen Typ Set oder Prop ist. Diese Regel steht im Gegensatz zu der Regel für Prop, bei der die Einschränkung auch für nicht große induktive Typen gilt. und wo der Ergebnistyp möglicherweise nur den Typ Prop hat. In alten Versionen von Coq war Set standardmäßig anzeigend. In späteren Versionen ist Set ein Prädikativ, um Inkonsistenzen mit einigen klassischen Axiomen zu vermeiden. Insbesondere sollte man bei der Verwendung von Impredicative Set mit Axiomen der Wahl aufpassen. In Kombination mit ausgeschlossener mittlerer oder Prädikat-Extensionalität kann dies zu Inkonsistenzen führen. Impredicative Set kann nützlich sein, um inhärent improvisierte mathematische Konzepte zu modellieren, aber fast alle Coq-Entwicklungen kommen ohne sie zurecht.