On appellera type concret un type I spécifié par la donnée d’un ensemble fini de constructeurs qui sont des constantes dont le type a pour conclusion une instance de I.
On attend d’un type concret la propriété suivante : tout terme clos de ce type se réduit en un terme commençant par un constructeur.
Lorsque le type I apparait dans un type d’un argument d’un constructeur alors le type est dit récursif.
Si de plus les occurrences de I sont positives dans les arguments des constructeurs alors on dira que le type concret est positif.
Un modèle de ces types est donné par des arbres dont les nœuds sont indicés par les constructeurs et dont certaines branches peuvent être des fonctions renvoyant des familles d’arbres de même nature ce qui permet de représenter par un terme fini un branchement infini. C’est le cas par exemple des notations ordinales introduites dans le paragraphe 3.3.1.
On peut vouloir se restreindre aux structures dont chaque branche est
finie (même si du fait des branchements infinis, la structure
elle-même n’est pas finie). On parlera alors d’objet bien
fondé dans le type positif.
Lorsqu’on se restreint à ces objets bien fondés, on peut disposer de
principes de récurrence pour le type, soit sous la forme d’une
récurrence structurelle généralisée, soit en disant que l’ordre
sous-terme est bien fondé.
Mais il peut être intéressant de disposer aussi d’un type qui
pourrait contenir des arbres dont les branches sont potentiellement
infinies. Il ne s’agit pas alors de se donner un principe de
récurrence pour raisonner sur ces objets mais au contraire des
opérateurs pour construire de tels objets infinis, en effet
l’application des seuls constructeurs ne construira que des objets
finis.
L’exemple de base qui est donné pour de tels types infinis est celui des listes 1:
Dans le cas de ListI les listes peuvent être finies ou infinies, dans le cas de Stream, il n’y a que des listes infinies dans ce type.
Montrer que si on définit le type Stream de manière inductive et pas coinductive alors ce type est vide, c’est-à-dire que l’on a une preuve de Stream→ False.
Il faut garder à l’esprit que l’on cherche à préserver la propriété des types concrets que chaque terme clos se réduira vers un terme qui commence par un constructeur.
Dans le cas des streams, cela revient à dire que tout terme de type Stream est égal à (Cons a l) pour un certain a:A et l:Stream ce qui peut s’écrire:
D’un point de vue plus opérationnel, si toute valeur de type Stream peut être réduite vers un terme construit avec Cons alors on peut utiliser un opérateur de définition par filtrage:
et on a la réduction suivante:
Ceci permet de définir les fonctions d’accès au premier élément de la liste ainsi qu’à sa queue:
En combinant ces deux fonctions et par récurrence structurelle sur n il est possible de définir la fonction d’accès au n-ème élément d’une liste.
Tout comme les branchements infinis étaient en fait représentés par des fonctions qui sont une notation finie pour représenter une infinité de valeurs, les branches infinies seront représentées intentionnellement par des programmes permettant de les développer aussi loin que nécessaire.
Le principe dit de co-itération a le type suivant:
Le principe de base pour représenter un liste infinie par un objet fini est de se donner un type X quelconque, une fonction out de type X → A une fonction tran de type X → X et un objet x de type X. Ces composantes permettent de construire un processus dont l’état est composé d’un registre de type X dont la valeur initiale est x et des deux fonctions out et tran. On obtient alors une stream (Stream_coiter out tran x) que l’on notera également (X,out,tran,x). On peut interpréter cette stream comme un processus : A chaque étape ce processus a une valeur x dans son registre il peut émettre une valeur de type A donnée par (out x) et transformer son registre en la valeur (tran x). Si on appelle p la fonction qui prend en entrée la valeur x du registre et renvoie la stream (X,out,tran,x) alors on a :
| (p x)=(Cons (out x) (p (tran x))) (4.1) |
Tout comme il existe plusieurs algorithmes qui implantent la même fonction, la même liste infinie pourra être engendrée par des processus très différents.
Par exemple on peut engendrer la suite des puissances successives de n : 1 n n2 … nk… des deux manières suivantes en prenant dans les deux cas un registre de type entier:
S’il faut calculer un segment de cette suite alors la seconde méthode sera plus efficace.
En général si on se donne une fonction f:nat→ A alors celle-ci peut être implantée par une stream de registre entier initialisée à 0 de fonction out égale à f et de fonction tran égale à la fonction successeur. Si cette stream permet de calculer toutes les valeurs successives de f, elle ne tient pas compte des calculs précédents pour le faire.
Les streams définies par co-itération peuvent véritablement se voir comme des petits circuits séquentiels.
Dans le principe de co-itération, le processus fournit des valeurs successives en mettant à jour le registre mais ne modifie jamais sa structure interne (type du registre, ou fonctions de sortie ou de transition).
Ce n’est pas théoriquement un problème. En effet supposons que l’on veuille faire évoluer un processus (X1,out1,tran1,x1) vers un processus (X2,out2,tran2,x2) il suffit de le prévoir en avance et d’appliquer le principe de coitération à un registre de type la somme disjointe X1+X2 de X1 et X2, la fonction de sortie qui utilise out1 lorsque le registre est dans l’état X1 et out2 lorsque le registre est dans l’état X2, quant à la fonction de transition elle peut choisir de laisser le processus dans l’état X1 ou X2 ou au contraire d’effectuer une transition d’un état X1 dans un état X2 ou inversement.
Il y a une manière systématique de capturer cette possibilité de transformation dans l’implantation d’une stream, c’est le principe de co-récursion:
La fonction de transition peut soit choisir de renvoyer un processus de même implantation, soit choisir de transformer le processus en un nouvel objet de type Stream pouvant avoir une implantation complètement différente.
Montrer que la propriété de corécursion Stream_corec se déduit de la coitération Stream_coiter.
La propriété attendue pour l’opérateur de co-récursion est la suivante :
| (p x)=(Cons (out x) Cases (tran x) of (inl x′)⇒ (p x′) | (inr s)⇒ s end) (4.2) |
Dans les langages de programmation fonctionnels qui manipulent des structures infinies (par exemple les langages de la famille ML paresseux tels que Haskell), il n’est pas question d’opérateur de co-itération, on utilise simplement le point fixe général du langage et la paresse de l’évaluation pour construire des structures infinies. En reprenant les équations définissant les propriétés des streams définies par coitération ou corécursion, on voit que ces streams auraient pu être directement définies par les équations récursives 4.1 ou 4.2.
Cependant dans notre approche, nous avons supposé a priori que toute liste était infinie et en particulier possédait un objet de tête. Il ne sera donc pas possible d’accepter n’importe quelle définition de point fixe.
L’exemple classique de liste problématique est la fonction qui filtre une liste infinie en ne gardant que les objets qui vérifient une condition P. Dans un langage de programmation on écrirait comme corps de la définition de (filtre P s):
| Cases s of (Cons a l)⇒ if (P a) then (Cons a (filtre P l)) else (filtre P l) end |
Cette définition n’est pas correcte sans information supplémentaire,
en effet si la liste ne possède plus à partir d’un certain rang
d’éléments qui vérifie P alors la liste (filtre P s) n’est
pas infinie. Renvoyer le résultat dans le type des listes finies ou
infinies ne solutionne pas le problème puisqu’on ne sais pas décider
si la liste s’arrête ou pas en ayant examiné un fragment initial. Le
même problème se pose d’ailleurs si les listes infinies sont
représentées par des fonctions totales.
Pour contourner cette difficulté on peut adopter plusieurs approches
comme par exemple introduire un constructeur silencieux pour les
listes résultats qui sera introduit dans le cas où l’élément ne
vérifie pas P. On peut aussi ajouter un élément de preuve qui va
garantir que P est vrai infiniment souvent dans s.
Nous montrons maintenant les différentes constructions disponibles dans Coq pour manipuler les structures infinies.
Ceux-ci se spécifient à l’aide d’une construction analogue à celle des définitions inductives mais utilisant le mot clé CoInductive. On a vu la définition du type des listes.
L’opéateur de destruction par filtrage Cases traite de la même manière les définitions inductives et coinductives. Il exprime juste qu’une valeur dans le type concret est formé à partir de l’un des constructeurs du type.
Les définitions d’objets infinis se font à l’aide d’un point fixe gardé par des constructeurs, il n’y a pas besoin de spécifier d’argument de décroissance comme dans le cas de définition inductive.
La condition de garde stipule qu’un appel récursif ne peut avoir lieu que sous au moins un constructeur (et il doit alors être en position d’argument récursif) et sous uniquement des constructeurs, en particulier un appel récursif ne doit pas se trouver en position d’argument d’un symbole de fonction ou dans la partie principale d’un filtrage, par contre il peut être dans la branche d’une définition par cas. Par exemple pour définir la fonction map sur les streams.
On vérifie que la fonction filter n’est pas acceptée.
Cependant, certaines définitions qui sont sémantiquement productives ne sont pas acceptées par ce critère essentiellement syntaxique :
D’autres systèmes [Gim97] permettent une tolérance plus grande vis-à-vis de ces définitions.
Comme dans le cas des définitions co-inductives, il est nécessaire de "garder" également la réduction afin de ne pas perdre la normalisation forte.
Un point fixe est une forme normale :
Si f est définie comme le co-fixpoint de la fonctionnelle F par f:=λ x ⇒ (F f x) alors la réduction (f x) →ι (F f x) ne se produira que si f se trouve en position de tête dans une définition par cas. La ι-réduction a donc pour forme :
| match (f x) with … end →ι match (F f x) with … end |
La preuve de normalisation forte peut se trouver dans [Gim96b].
Cette propriété de réduction est suffisante pour calculer n’importe quelle valeur d’une stream :
En pratique, il est possible de faire une preuve de :
| (f x)=(F f x) |
dans laquelle l’égalité est celle de Leibniz, alors que (f x) et (F f x) ne sont pas directement convertibles. Pour cela il faut passer par une étape intermédiaire analogue à une η-expansion que nous allons expliquer maintenant :
Soit I un type inductif avec n constructeurs c1,…,cn. Il est facile de montrer par cas sur x la propriété suivante que nous appelerons η :
| x=match x with (c1 vec(x))⇒ (c1 vec(x)) | … (cn vec(x))⇒ (cn vec(x)) end |
On procède ensuite de la manière suivante :
|
Dans le cas des streams, le lemme de η-expansion aura la forme suivante :
On montre ensuite les propriétés attendues :
Le schéma de définition de familles inductives suit le schéma de définition des types inductifs. Il en est de même pour les définitions de familles co-inductives.
Une famille définie co-inductivement est une propriété dont les preuves peuvent être des objets infinis.
Supposons que l’on veuille justifier que de streams (potentiellement infinies) sont extensionnellement égales, c’est-à-dire que les valeurs de leurs différents éléments sont les mêmes. On pourrait le faire en utilisant un entier n et l’accès à la n-ème valeur d’une stream. Cependant, si le type co-inductif devient plus compliqué, alors l’accès aux composantes va nécessiter l’introduction de types de données assez complexes. Il est plus naturel d’utiliser une définitions structurelle de l’égalité. Deux objets co-inductifs sont égaux si ils commencent par le même constructeur et que les composantes sont égales. Évidemment, dans le cas d’objets infinis, on ne peut utiliser une définition inductive de l’égalité. Il faut avoir recours à une définition co-inductive pour capturer l’égalité d’objets infinis.
Dans le cas des streams, cela donne :
Une variante équivalente est :
Les preuves de définitions de relations co-inductives suivent les même règles que les types coinductifs. On peut leur appliquer des analyses par cas, des inversions ou bien construire des preuves par co-itération, co-récursion ou plus généralement par point fixe gardé. Cette dernière méthode s’avère la plus souple. Cependant sa manipulation pour la construction de preuves peut être parfois délicate. En effet les preuves sont construites interactivement par des tactiques. Pour les constructions par point fixe, une tactique t(Cofix) existe. Elle introduit dans le but une hypothèse identique à la propriété à prouver mais qui ne pourra être utilisée que de manière gardée. Vérifier que la condition de garde est toujours satisfaite après chaque application de tactique est trop couteûx, aussi cette vérification n’est faite qu’au moment de la sauvegarde de la preuve finale ou bien à la demande explicite de l’utilisateur.
Nou pouvons montrer que l’égalite sur les streams est réflexive, symétrique et transitive :
On peut également montrer que l’égalité ainsi définie est bien la plus grande relation R qui vérifie : (R s1 s2) ⇒ (head s1)=(head s2) ∧ (R (tail s1) (tail s2)). Il suffit de montrer que si R est une telle relation alors : (R s1 s2) ⇒ (EqStream s1 s2). Cette preuve se fait aisément en utilisant un point fixe est est laissée en exercice.
Les définitions co-inductives sont utiles à la modélisation de processus parallèles. En effet une définition co-inductive d’une algèbre de processus permet de pouvoir définir des processus récursifs sans avoir explicitement à manipuler un opérateur de récursion. D’autres part les définitions de bisimulation entre processus sont naturellement des définitions co-inductives. Dans les contributions du système Coq, on trouvera des modélisations de plusieurs algèbres de processus (CCS, CBS) ainsi que du π-calcul.
Les définitions co-inductives permettent également de définir naturellement certains opérateurs de la logique temporelle. Si on suppose donnée un système de transitions R sur des états de type X.
Les formules de la logique temporelle ont pour interprétation in ensemble d’états. On peut définir les propriétés de la logique temporelle, en les représentant directement par leur semantique.
Il sera alors très simple de définir de manière co-inductive les opérateurs All et Ex sur les formules. La sémantique de All (resp. Ex) est que soit P une formule et x un état, pour tout chemin (resp. pour un chemin) issu de x, la formule P est vérifiée.
Les définitions co-inductives peuvent également être utilisées pour représenter des suites infinies, par exemple des suites de rationnels permettant de représenter des entiers.