Pourquoi Agda et Coq ne sont-ils pas d'accord sur une positivité stricte?

24

Je suis tombé sur un désaccord déroutant entre Agda et Coq qui n'est évidemment pas lié aux distinctions les plus connues entre leurs théories de types (par exemple, (im) prédicativité, induction-récursivité, etc.).

En particulier, la définition suivante est acceptée par Agda:

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

tandis que la définition équivalente de Coq est rejetée parce que l'apparition de [Ty _] comme un index de lui-même dans c2 est considérée comme violant la positivité stricte.

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

En fait, ce cas est presque mot pour mot un exemple tiré de la section 14.1.2.1 de Coq'Art de violation de la positivité stricte:

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

Mais je ne vois pas les raisons de cette différence entre les théories de type. L'exemple classique de prouver Faux en utilisant une occurrence négative d'un type dans un argument constructeur est clair pour moi, mais je ne vois pas comment on pourrait dériver une contradiction de ce style d'indexation (indépendamment des arguments constructeur autrement strictement positifs).

En fouillant dans la littérature, le premier article de Dybjer sur les familles inductives fait un commentaire désinvolte sur la solution de Paulin-Mohring dans le document CID ayant des restrictions légèrement différentes, et suggère vaguement que les différences pourraient être liées à l'imprédicativité, mais n'élabore pas davantage. Le document de Dybjer semble permettre cela, alors que celui de Paulin-Mohring l'interdit clairement.

Apparemment, je ne suis pas le premier à remarquer cette différence d'opinion, et certains pensent que cette définition ne devrait pas être autorisée dans les deux systèmes ( https://lists.chalmers.se/pipermail/agda/2012/004249.html ), mais Je n'ai trouvé aucune explication de la raison pour laquelle il est soit sain dans un système mais pas dans l'autre, ou juste une différence d'opinion.

Je suppose donc que j'ai plusieurs questions:

  1. Est-ce un exemple d'un type monotone, mais non strictement positif? (En Coq; clairement Agda le considère strictement positif)
  2. Pourquoi Agda le permet-il alors que Coq le rejette? C'est simplement une différence idiosyncrasique dans l'interprétation de «strictement positif», y a-t-il une différence subtile entre Coq et Agda qui la rend saine dans Agda et non saine dans Coq, ou est-ce une question de goût motivée par des préférences théoriques particulières?
  3. Existe-t-il une différence significative entre la première définition ci-dessus et la définition équivalente inductive-récursive ci-dessous?

Définition inductive-récursive:

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

Je suis heureux d'avoir des pointeurs sur la littérature pertinente.

Merci d'avance.

Colin Gordon
la source
1
Pour autant que je sache, Coq est plus strict que ce que permet la théorie sous-jacente, car il était plus facile à mettre en œuvre et suffisamment utile dans la pratique. Cette réponse à propos d'un cas différent mais connexe est pour autant que je le comprenne.
Gilles 'SO- arrête d'être méchant'
1
Cette définition n'est pas acceptée par la version de développement actuelle d'Agda:Ty is not strictly positive, because it occurs in an index of the target type of the constructor c2 in the definition of Ty.
gallais
2
Oui, tu as raison, quelqu'un d'autre me l'a fait remarquer hier soir. J'utilisais le paquet 2.3.0.1 de Debian, mais 2.3.2.1 de Cabal rejette les définitions directes et IR. Il semble qu'un bug apparemment sans rapport ait rendu la vérification de la positivité des indices plus stricte: code.google.com/p/agda/issues/detail?id=690 Comme il a été discuté sur la liste sans être explicitement marqué comme un problème de solidité, je suis toujours me demandant si le type lui-même est sain.
Colin Gordon

Réponses:

10

Le problème semble être la confusion résultant de la confluence de deux facteurs:

  1. J'utilisais une version périmée d'Agda (2.3.0.1). Il semble qu'avant la 2.3.2, Agda ne vérifiait tout simplement pas la positivité stricte des indices des résultats des constructeurs (voir le bug que j'ai lié ailleurs dans le fil).
  2. Une lecture plus approfondie de l'article sur les familles inductives de Dybjer suggère qu'il peut avoir voulu que le type inductif défini ne soit pas lié lors de la saisie des indices d'un résultat de constructeur . La section 3.2.1 donne le schéma des constructeurs inductifs en prose, et apparemment j'ai mal lu le langage décrivant les environnements de liaison de chaque partie du schéma.

Cette lecture plus approfondie est bien sûr cohérente avec la vérification effectuée par Coq et (versions récentes de) Agda, qui interdisent toute apparition de T dans ses propres indices.

Colin Gordon
la source
4

Une raison possible de la différence, comme l'indiquent vos propres remarques, est l'imprédicativité. Coq avait historiquement un ensemble imprédicatif (toujours disponible comme drapeau je crois!)

Citant le livre d'Adam Chlipala http://adam.chlipala.net/cpdt/html/Universes.html

Les outils Coq prennent en charge un indicateur de ligne de commande -impredicative-set, qui modifie Gallina d'une manière plus fondamentale en rendant Set imprédicatif. Un terme comme forall T: Set, T a le type Set, et les définitions inductives dans Set peuvent avoir des constructeurs qui quantifient sur des arguments de tous types. Pour maintenir la cohérence, une restriction d'élimination doit être imposée, de la même manière que la restriction pour Prop. La restriction ne s'applique qu'aux grands types inductifs, où certains constructeurs quantifient sur un type de type Type. Dans de tels cas, une valeur de ce type inductif peut uniquement être mise en correspondance avec un motif pour produire un type de résultat dont le type est Set ou Prop. Cette règle contraste avec la règle de Prop, où la restriction s'applique même aux types inductifs non importants, et où le type de résultat ne peut avoir que le type Prop. Dans les anciennes versions de Coq, Set était imprédicatif par défaut. Les versions ultérieures rendent Set prédictif pour éviter l'incohérence avec certains axiomes classiques. En particulier, il faut faire attention lors de l'utilisation de Set imprédicatif avec des axiomes de choix. En combinaison avec une extensionnalité intermédiaire ou prédicat exclue, une incohérence peut en résulter. Impredicative Set peut être utile pour modéliser des concepts mathématiques intrinsèquement imprédicatifs, mais presque tous les développements Coq s'en sortent bien sans lui.

Carter Tazio Schonwald
la source
D'après le son du correctif de bogue que j'ai trouvé ci-dessus, il semble que Agda ne vérifiait tout simplement pas la positivité des indices pour les résultats du constructeur. Ce qui n'indique pas réellement si mon type proposé est monotone, mais suggère qu'il n'est pas lié à l'imprédicativité.
Colin Gordon
2
Et oui, -impredicative-set rend Set imprédicatif dans Coq.
Colin Gordon