Dlaczego Agda i Coq nie zgadzają się co do ścisłej pozytywności?

Natknąłem się na mylące spory między Agdą i Coq, które nie są oczywiście związane z najbardziej znanymi różnicami między ich teoriami typów (np. (Im) predykatywność, indukcja-rekurencja itp.).

W szczególności Agda akceptuje następującą definicję:

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

podczas gdy równoważna definicja Coq została odrzucona, ponieważ pojawienie się [Ty _] jako wskaźnika samego siebie w c2 jest uważane za naruszające ścisłą pozytywność.

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

W rzeczywistości ten przypadek jest niemal dosłownie przykładem z sekcji 14.1.2.1 Coq'Art o naruszeniu ścisłej pozytywności:

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

Ale nie widzę przyczyn tej różnicy między teoriami typów. Klasyczny przykład udowodnienia Fałsz przy użyciu negatywnego wystąpienia typu w argumencie konstruktora jest dla mnie jasny, ale nie widzę, jak można wywnioskować sprzeczność z tego stylu indeksowania (niezależnie od ściśle pozytywnych argumentów konstruktora).

Grzebiąc w literaturze, wczesny artykuł Indukcyjnych Rodzin Dybjera od razu komentuje rozwiązanie Paulina-Mohringa w artykule CID mającym nieco inne ograniczenia i niejasno sugeruje, że różnice mogą być związane z impredykatywnością, ale nie wyjaśnia dalej. Papier Dybjera wydaje się na to pozwalać, podczas gdy Paulin-Mohring wyraźnie tego zabrania.

Najwyraźniej nie jestem pierwszym, który zauważył tę różnicę zdań i niektórzy uważają, że ta definicja nie powinna być dozwolona w żadnym systemie ( https://lists.chalmers.se/pipermail/agda/2012/004249.html ), ale Nie znalazłem żadnych wyjaśnień, dlaczego jest to dźwięk w jednym systemie, ale nie w drugim, lub po prostu różnica zdań.

Przypuszczam, że mam kilka pytań:

1. Czy to przykład typu monotonnego, ale nie do końca pozytywnego? (W Coq; wyraźnie Agda uważa to za całkowicie pozytywne)
2. Dlaczego Agda pozwala na to, a Coq to odrzuca? Jest to po prostu idiosynkratyczna różnica w interpretacji „ściśle pozytywnego”, czy istnieje subtelna różnica między Coq i Agda, która sprawia, że ​​brzmi to w Agdzie i nie brzmi w Coq, czy też jest to kwestia gustu wynikająca z określonych preferencji teoretycznych?
3. Czy istnieje znacząca różnica między pierwszą definicją powyżej a równoważną definicją indukcyjno-rekurencyjną poniżej?

Definicja indukcyjno-rekurencyjna:

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

Cieszę się, że mam wskazówki do odpowiedniej literatury.

Z góry dziękuję.

Problemem wydaje się być zamieszanie wynikające z połączenia dwóch czynników:

1. Korzystałem ze starej wersji Agdy (2.3.0.1). Wygląda na to, że przed 2.3.2 Agda po prostu nie sprawdzała ścisłej pozytywności wskaźników wyników konstruktora (patrz błąd, który umieściłem w innym miejscu w wątku).
2. Bliższe czytanie artykułu Dybjer's Inductive Families sugeruje, że mógł on chcieć, aby zdefiniowany typ indukcyjny nie był związany podczas wpisywania wskaźników wyniku konstruktora . Sekcja 3.2.1 podaje schemat konstruktorów indukcyjnych w prozie i najwyraźniej źle odczytałem język opisujący wiążące środowiska każdej części schematu.

To bliższe czytanie jest oczywiście zgodne z kontrolą przeprowadzoną przez Coq i (najnowsze wersje) Agdy, które zabraniają jakiegokolwiek pojawiania się T we własnych indeksach.

Możliwą przyczyną tej różnicy, jak wskazują własne uwagi, jest impredykatywność. Coq historycznie miał impredykacyjny zestaw (wierzę, że wciąż dostępny jako flaga!)

Cytując książkę Adama Chlipali http://adam.chlipala.net/cpdt/html/Universes.html

Narzędzia Coq obsługują zestaw flag-wierszy polecenia, który modyfikuje Gallinę w bardziej fundamentalny sposób, czyniąc Set impredykatywnym. Termin taki jak forall T: Set, T ma typ Set, a definicje indukcyjne w Set mogą mieć konstruktory, które kwantyfikują argumenty dowolnego typu. Aby zachować spójność, należy nałożyć ograniczenie eliminacji, podobnie jak ograniczenie Prop. Ograniczenie dotyczy tylko dużych typów indukcyjnych, w których jakiś konstruktor określa ilościowo typ typu Typ. W takich przypadkach wartość w tym typie indukcyjnym można dopasować do wzorca tylko w celu uzyskania typu wyniku, którego typ to Set lub Prop. Ta reguła jest sprzeczna z regułą dla Prop, gdzie ograniczenie dotyczy nawet niedużych typów indukcyjnych, i gdzie typ wyniku może mieć tylko typ Prop. W starych wersjach Coq Set był domyślnie impredykatywny. Późniejsze wersje ustawiają predykat, aby uniknąć niespójności z niektórymi klasycznymi aksjomatami. W szczególności należy uważać, używając impredykatywnego zestawu z wybranymi aksjomatami. W połączeniu z wykluczoną ekstensywnością środkową lub orzeczniczą może dojść do niespójności. Zestaw impredykatywny może być przydatny do modelowania z natury impredykatywnych pojęć matematycznych, ale prawie wszystkie opracowania Coq radzą sobie bez niego.