Polymorphisme et types de données inductifs

Je suis curieux. J'ai travaillé sur ce type de données dans OCaml :

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

Qui peut être manipulé en utilisant des fonctions récursives explicitement typées (une fonctionnalité qui a été ajoutée assez récemment). Exemple:

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

Mais je n'ai jamais pu le définir dans Coq :

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

Coq gémit. Il n'aime pas le dernier constructeur et dit quelque chose que je ne comprends pas complètement ou avec lequel je ne suis pas d'accord:

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

Ce que je peux comprendre, c'est que les types inductifs utilisant une négation à l'intérieur de leur définition comme type 'a term = Constructor ('a term -> …)sont rejetés, car ils conduiraient à des bêtes laides non fondées comme des termes λ (non typés). Cependant, ce exptreetype de données particulier semble assez anodin: en regardant sa définition OCaml , son argument 'an'est jamais utilisé dans des positions négatives.

Il semble que Coq soit trop prudent ici. Existe-t-il vraiment un problème avec ce type de données inductif particulier? Ou Coq pourrait-il être un peu plus permissif ici?

Et qu'en est-il des autres assistants de preuve, sont-ils capables de faire face à une telle définition inductive (de manière naturelle)?

Cela est apparu plusieurs fois sur la liste de diffusion Coq, mais je n'ai jamais vu de réponse concluante. Coq n'est pas aussi général qu'il pourrait l'être; les règles de (Coquand, 1990) et (Giménez, 1998) (et sa thèse de doctorat) sont plus générales et ne nécessitent pas une positivité stricte. Cependant, la positivité n'est pas suffisante lorsque vous sortez Set; cet exemple est ressorti de plusieurs discussions :

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

Avec des structures de données simples telles que la vôtre, le type inductif ne causerait pas de problèmes autres que la mise en œuvre plus complexe.

Il existe un moyen général de définir des types tels que celui-ci défini comme le point fixe d'un polynôme:

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

Au lieu de tenter de définir la fonction , définissez la famille de types . Cela signifie ajouter un paramètre entier au type qui code le nombre d'auto-compositions ( , , , etc.), et un constructeur d'injection supplémentaire pour transformer en .$\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)$$\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
.

Vous pouvez continuer à définir des valeurs et à les travailler. Coq pourra souvent déduire l'exposant. Set Implicit Argumentsrendrait ces définitions plus jolies.

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

Vous préférerez peut-être diminuer l'argument de 1, ce qui exptreeest le cas et 0. Cela supprime beaucoup de choses S ndans la définition, ce qui peut rendre certaines preuves plus faciles, mais cela nécessite de séparer le cas initial du cas de récurrence dans chaque constructeur qui prend un dans un argument (au lieu d'ajouter un seul constructeur d'injection pour ). Dans cet exemple, il n'y a qu'un seul constructeur à diviser, donc cela devrait être un bon choix.$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)).

Je pense que c'est le même principe proposé sous une forme plus générale par Ralph Mattes .

Références

Thierry Coquand et Christine Paulin. Types définis par induction . Dans Actes de COLOG'88 , LNCS 417, 1990. [ Springer ] [ Google ]

Eduardo Giménez. Définitions structurelles récursives en théorie des types . In ICALP'98: Actes du 25e Colloque international sur les automates, les langues et la programmation. Springer-Verlag, 1998. [ PDF ]

Ralph Matthes décrit comment simuler des types comme celui-ci dans Coq dans "A Datastructure for Iterated Powers" ( code , papier ).

L'une des premières choses que fait Coq est de construire le principe d'induction associé au type inductif que vous venez de définir et la compréhension du principe d'induction sous-jacent est un bon exercice.

Par exemple O : nat | S : nat -> natva générer le principe d'induction P O -> (∀ n, P n -> P (S n)) -> ∀ n, P n.

À quoi correspondrait le principe d'induction iota? Il semble qu'il n'y a pas prédicat Pqui serait en mesure de parler P tet P (iota t), parce qu'il devrait parler exptree a, exptree (exptree a), exptree (exptree (exptree a))...

Le Omicronfait la même chose mais le type est plus petit à chaque fois. Vous devriez sentir que le fait d'avoir une référence à la fois à un type plus petit et à un type plus grand rendrait les choses désordonnées. (Cela dit, Omicronc'est la bonne façon)

Ce ne sont pas les critères exacts qui expliquent pourquoi la définition ne devrait pas être acceptée, mais cela explique pourquoi cela me semble mal.

exptreesemble que vous construisez une grammaire pour les expressions, chose qui n'est généralement pas si récursive. Voulez-vous de l'aide à ce sujet?