Qu'est-ce que la coinduction?

J'ai entendu parler de l'induction (structurelle). Il vous permet de construire des structures finies à partir de plus petites et vous donne des principes de preuve pour raisonner sur de telles structures. L'idée est assez claire.

Mais qu'en est-il de la coinduction? Comment ça marche? Comment peut-on dire quelque chose de concluant sur une structure infinie?

Il y a (au moins) deux angles à aborder, à savoir la coinduction comme moyen de définir les choses et comme technique de preuve.

En ce qui concerne la coinduction en tant que technique de preuve, quelle est la relation entre la coinduction et la bisimulation?

Premièrement, pour dissiper une possible dissonance cognitive: raisonner sur des structures infinies n’est pas un problème, nous le faisons tout le temps. Tant que la structure est finement descriptible, ce n'est pas un problème. Voici quelques types courants de structures infinies:

• langages (ensembles de chaînes sur un alphabet, qui peuvent être finis);
• langues d'arbre (ensembles d'arbres sur un alphabet);
• traces d'exécution d'un système non déterministe;
• nombres réels;
• ensembles d'entiers;
• des ensembles de fonctions allant d’entiers à entiers; …

La coinductivité en tant que plus grand point de fixation

Là où les définitions inductives construisent une structure à partir de blocs élémentaires, les définitions coinductives façonnent les structures à partir de la manière dont elles peuvent être déconstruites. Par exemple, le type de listes dont les éléments sont dans un ensemble Aest défini comme suit dans Coq:

Inductive list (A:Set) : Set :=
  | nil : list A
  | cons : A -> list A -> list A.

De manière informelle, le listtype est le plus petit type contenant toutes les valeurs construites à partir des constructeurs nilet cons, avec l'axiome suivant: . Inversement, nous pouvons définir le type le plus grand contenant toutes les valeurs construites à partir de ces constructeurs, en conservant l’axiome de discrimination:$\forall x \, y, \: \mathtt{nil} \ne \mathtt{cons} \: x \: y$

CoInductive colist (A:Set) : Set :=
  | conil : colist A
  | cocons : A -> colist A -> colist A.

listest isomorphe à un sous-ensemble de colist. En outre, colistcontient des listes infinies: listes avec coconssur cocons.

CoFixpoint flipflop : colist ℕ := cocons 1 (cocons 2 flipflop).
CoFixpoint from (n:ℕ) : colist ℕ := cocons n (from (1 + n)).

flipflopest l'infini (liste circulaire) ; est la liste infinie de nombres naturels .0 : : 1 : : 2 : : $1::2::1::2::\ldots$from 0$0::1::2::\ldots$

Une définition récursive est bien formée si le résultat est construit à partir de blocs plus petits: les appels récursifs doivent fonctionner sur des entrées plus petites. Une définition corécursive est bien formée si le résultat génère des objets plus volumineux. L'induction regarde les constructeurs, la coinduction regarde les destructeurs. Notez que la dualité passe non seulement de plus en plus petit à plus grand mais également d’entrées en sorties Par exemple, la raison pour laquelle les flipflopet fromdéfinitions ci - dessus sont bien formés est que l'appel corecursive est gardée par un appel au coconsconstructeur dans les deux cas.

Lorsque les déclarations sur les objets inductifs ont des preuves inductives, les déclarations sur les objets coinductifs ont des preuves coinductives. Par exemple, définissons le prédicat infini sur les colistes; intuitivement, les colistes infinis sont ceux qui ne finissent pas avec conil.

CoInductive Infinite A : colist A -> Prop :=
  | Inf : forall x l, Infinite l -> Infinite (cocons x l).

Pour prouver que les couleurs de la forme from nsont infinies, nous pouvons raisonner par coinduction. from nest égal à cocons n (from (1 + n)). Cela montre que from nest plus grand que from (1 + n), qui est infini par l'hypothèse de la coinduction, from nest donc infini.

Bisimilarité, une propriété coinductive

La coinduction en tant que technique de preuve s'applique également aux objets finitaires. Intuitivement, les preuves inductives sur un objet sont basées sur la façon dont l'objet est construit. Les preuves coinductives sont basées sur la façon dont l'objet peut être décomposé.

Lors de l’étude de systèmes déterministes, il est courant de définir l’équivalence par des règles inductives: deux systèmes sont équivalents s’il est possible de passer de l’un à l’autre par une série de transformations. De telles définitions tendent à ne pas saisir les nombreuses manières différentes dont les systèmes non déterministes peuvent avoir le même comportement (observable) malgré une structure interne différente. (La coinduction est également utile pour décrire les systèmes sans terminaison, même s'ils sont déterministes, mais ce n'est pas ce sur quoi je vais me concentrer ici.)

Les systèmes non déterministes tels que les systèmes concurrents sont souvent modélisés par des systèmes de transition étiquetés . Un LTS est un graphe orienté dans lequel les arêtes sont étiquetées. Chaque bord représente une transition possible du système. Une trace d'un LTS est la séquence d'étiquettes de bord sur un chemin dans le graphique.

Deux LTS peuvent se comporter de manière identique, en ce sens qu'ils ont les mêmes traces possibles, même si leur structure interne est différente. L'isomorphisme des graphes est trop fort pour définir leur équivalence. Au lieu de cela, un LTS est dit pour simuler un autre LTS si chaque transition du second LTS admet une transition correspondant à la première. Formellement, soit l’union disjointe des états des deux LTS, l’ensemble (commun) d’étiquettes et la relation de transition. La relation est une simulation si B S L → R ⊆ S × S ∀ ( p , q ) ∈ R ,  si  p alpha → p '  puis  ∃ q '$\mathscr{A}$$\mathscr{B}$$S$$L$$\rightarrow$$R \subseteq S \times S$

$\mathscr{A}$ simule s'il existe une simulation dans laquelle tous les états de sont liés à un état dans . Si est une simulation dans les deux sens, on parle de bisimulation . La simulation est une propriété coinductive: toute observation d'un côté doit correspondre à l'autre.$\mathscr{B}$$\mathscr{B}$$\mathscr{A}$$R$

Il existe potentiellement de nombreuses bisimulations dans un LTS. Différentes bisimulations peuvent identifier différents états. Étant donné deux bisimulations et , la relation donnée en prenant l'union des graphes de relation est elle-même une bisimulation, car les états liés donnent lieu à des états liés pour les deux relations. (Cela vaut également pour les unions infinies. La relation vide est une bisimulation non intelligible, de même que la relation identitaire.) En particulier, l'union de toutes les bisimulations est elle-même une bisimulation, appelée bisimilarité. La bisimilarité est le moyen le plus grossier d’observer un système qui ne fait pas la distinction entre des États distincts.$R_1$$R_2$$R_1 \cup R_2$

La bi-similitude est une propriété coinductive. Il peut être défini comme le plus grand point fixe d'un opérateur: c'est la relation la plus grande qui, lorsqu'elle est étendue à l'identification d'états équivalents, reste la même.

Références

• Coq et le calcul des constructions inductives

  • Yves Bertot et Pierre Castéran. Démonstration de théorèmes interactifs et développement de programmes - Coq'Art: le calcul des constructions inductives . Springer, 2004. Ch. 13. [ site web ] [ Amazon ]
  • Eduardo Giménez. Une application de types co-inductifs en coq: vérification du protocole à bits alternatifs . Dans Atelier sur les types de preuves et de programmes , numéro 1158 dans Notes de cours en informatique , pages 135-152. Springer-Verlag, 1995. [ Google Books ]
  • Eduardo Giménez et Pierre Castéran. Un tutoriel sur les types [co-] inductifs en Coq. 2007. [ PDF ]

• Systèmes de transition étiquetés et bisimulations

  • Robin Milner. Communication et concurrence . Prentice Hall, 1989.
  • Davide Sangiorgi. Sur les origines de la bisimulation et de la coinduction . Opérations ACM sur les langages et systèmes de programmation (TOPLAS), volume 31, numéro 4, mai 2009. [ PDF ] [ ACM ] Diapositives de cours associées: [ PDF ] [ CiteSeer ]

  • Davide Sangiorgi. Le Pi-calcul: une théorie des processus mobiles . Cambridge University Press, 2003. [ Amazon ]

    • Plus de références suggérées par Anton Trunov

  • Un chapitre de la programmation certifiée avec types dépendants par A. Chlipala

  • D. Sangiorgi. "Introduction à la bisimulation et à la coinduction". 2011. [ PDF ]
  • D. Sangiorgi et J. Rutten. Sujets avancés en bisimulation et coinduction . Cambridge University Press, 2012. [ Coupe ]

Considérons la définition inductive suivante:

$\qquad \displaystyle \begin{align*} &\phantom{\Rightarrow} \quad \varepsilon \in \mathcal{T} \\ w \in \mathcal{T} \quad &\Rightarrow \quad aw \in \mathcal{T}\\ aw \in \mathcal{T} \quad &\Rightarrow \quad baw \in \mathcal{T} \end{align*}$

Qu'est-ce que ? De toute évidence, le jeu de chaînes sans deux ultérieurs , c'est-à-dire$\mathcal{T}$$b$

$\qquad \displaystyle \mathcal{T} =\{\varepsilon, a, aa, ba, aaa, aba, \dots\} = \mathcal{L}\left((ba\mid a)^*\right) \subseteq \Sigma^*.$

Droite? Eh bien, ce dont nous avons besoin pour cela, c’est la phrase anodine "et est le plus petit ensemble qui remplisse ces conditions". C'est assez vrai, sinon fonctionnerait aussi.$\mathcal{T}$$\mathcal{T}=\{a,b\}^*$

Mais il y a plus que cela. Écrivez au-dessus de la définition sous forme de fonction (monotone) :$f : 2^{\Sigma^\infty} \to 2^{\Sigma^\infty}$

$\qquad f(T) = T \cup \{\varepsilon\} \cup \{aw \mid w\in T\} \cup \{baw \mid aw \in T\}$

Maintenant, est le plus petit point de fixation de . En fait, parce que est monotone et est un réseau complet , le théorème de Knaster-Tarski nous dit qu'un point de repère aussi petit existe et est un langage approprié. Parce que cela fonctionne avec n'importe quelle définition inductive raisonnable¹, nous n'en parlons généralement pas. Cela correspond tout à fait à notre intuition: nous commençons avec et appliquons les règles étape par étape; dans la limite, nous obtenons .$\mathcal{T}$$f$$f$$\left(2^{\Sigma^\infty},\subseteq\right)$$\{\varepsilon\}$$\mathcal{T}$

Maintenant nous retournons les choses. Au lieu de dire "si est inclus, ainsi est " nous disons "si est inclus, alors doit avoir été ". Nous ne pouvons pas retourner l'ancre, alors elle s'en va. Cela nous laisse avec un problème: nous devons pouvoir enlever les préfixes arbitrairement longs de tout mot de et rester dans ! Ce n'est pas possible avec des mots finis; C'est une bonne chose que je me suis glissé dans ci-dessus! On finit avec l'ensemble des mots infinis sans facteur (sous-chaîne) , c'est-à-dire .a w a w w T ' T ' Σ ∞ b b T ' = L ( ( b a | a ) ω $w$$aw$$aw$$w$$\mathcal{T}'$$\mathcal{T}'$$\Sigma^\infty$$bb$$\mathcal{T}'=\mathcal{L}\left((ba\mid a)^\omega\right)$

En termes de , est son plus grand point de fixation². C’est en fait assez intuitif: nous ne pouvons pas espérer toucher d’en bas , c’est-à-dire inductivement en partant de et en ajoutant des éléments qui respectent les règles, nous allons donc d’en haut , c’est-à-dire coinductivement en commençant de et en supprimant les éléments non conformes aux règles.T ' T ' { ε } Σ $f$$\mathcal{T}'$$\mathcal{T}'$$\{\varepsilon\}$$\Sigma^\infty$

Notation:

• $\Sigma^\infty = \Sigma^* \cup \Sigma^\omega$
• $\Sigma^\omega$ est l'ensemble de toutes les séquences infinies sur .$\Sigma$

¹ Vous n'êtes pas autorisé à faire des choses comme ; la fonction correspondante ne serait pas monotone. ² Nous devons balayer sous le tapis d’une manière ou d’une autre. { ε $w \in \mathcal{T} \Rightarrow aw \notin \mathcal{T}$
$\{\varepsilon\}$