Une méthode de définition et de raisonnement sur des structures ou comportements potentiellement infinis ou circulaires en les caractérisant comme points fixes les plus grands d'opérateurs et en prouvant des propriétés par des hypothèses coinductives telles que des bisimulations et des observations.

Principe

La coinduction établit l'appartenance ou l'équivalence à un ensemble de plus grand point fixe : pour prouver qu'un objet satisfait une propriété coinductive, il faut montrer qu'il présente les comportements observables préservés par la définition coinductive (souvent en démontrant une bisimulation ou une condition de préservation).

Démonstration

Les flux infinis (streams) sont souvent traités coinductivement : pour prouver que deux flux s et t sont égaux, on définit une relation de bisimulation R et on montre (s,t) ∈ R et que R est préservée par prise de tête et de queue, ce qui permet de conclure coinductivement s = t.

Mauvaise application

Appliquer des arguments inductifs de construction finie à des structures fondamentalement non fondées, ou utiliser la coinduction sans vérifier la condition de préservation/invariance (supposant ainsi des propriétés qui ne sont pas fermées par le déroulement coalgebrique), constitue une mauvaise utilisation.

Conséquence

Le raisonnement coinductif permet des preuves sonores et compositionnelles au sujet de données infinies, de systèmes réactifs et de comportements (par ex. flux, processus, arbres infinis) et autorise des définitions par comportement observable plutôt que par construction.

Inversion

L'induction (raisonnement par point fixe le plus petit) est le dual : elle prouve l'appartenance par construction finie à partir de cas de base et de constructeurs, tandis que la coinduction prouve l'appartenance en montrant qu'un élément est indiscernable des membres de l'ensemble coinductif par des mouvements observables.

Limite

Applicable aux domaines non bien-fondés ou corecursifs modélisés comme coalgebres et aux systèmes spécifiés par points fixes les plus grands ; inadaptée aux propriétés qui exigent terminaison finie ou induction bien fondée sans justifications supplémentaires.

Tension sémantique

La tension apparaît entre traiter les objets extentionnellement (par comportement observable, coinduction) et intentionnellement (par construction, induction) ; certaines preuves ne sont convertibles entre les deux que sous contraintes de finitude ou de garde supplémentaires.

Synthèse

Le raisonnement coinductif consiste à prouver des propriétés de structures infinies ou circulaires en montrant la préservation du comportement observable lors du déroulement ; il complète l'induction en ciblant les caractérisations par points fixes les plus grands et permet de raisonner sur des processus continus et des données infinies.