Coinduction - Coinduction
En informatique , la coinduction est une technique permettant de définir et de prouver les propriétés de systèmes d' objets en interaction simultanés .
La coinduction est le double mathématique de l' induction structurelle . Les types définis de manière coinductive sont connus sous le nom de codata et sont généralement des structures de données infinies , telles que des flux .
En tant que définition ou spécification , la coinduction décrit comment un objet peut être « observé », « décomposé » ou « détruit » en objets plus simples. En tant que technique de preuve , elle peut être utilisée pour montrer qu'une équation est satisfaite par toutes les implémentations possibles d'une telle spécification.
Pour générer et manipuler des codonnées, on utilise généralement des fonctions corecursives , en conjonction avec l' évaluation paresseuse . De manière informelle, plutôt que de définir une fonction par correspondance de motifs sur chacun des constructeurs inductifs, on définit chacun des "destructeurs" ou "observateurs" sur le résultat de la fonction.
En programmation, la programmation co-logique (co-LP pour brièveté) « est une généralisation naturelle de la programmation logique et de la programmation logique coinductive, qui à son tour généralise d'autres extensions de la programmation logique, telles que les arbres infinis, les prédicats paresseux et les prédicats communicants concurrents. Co-LP a des applications aux arbres rationnels, à la vérification de propriétés infinités, à l'évaluation paresseuse, à la programmation logique concurrente, à la vérification de modèle, aux preuves de bisimilarité , etc." Des implémentations expérimentales de co-LP sont disponibles auprès de l'Université du Texas à Dallas et dans Logtalk (pour des exemples, voir ) et SWI-Prolog .
Voir également
Les références
Lectures complémentaires
- Manuels
- Davide Sangiorgi (2012). Introduction à la bisimulation et à la co-induction . La presse de l'Universite de Cambridge.
- Davide Sangiorgi et Jan Rutten (2011). Sujets avancés en bisimulation et coinduction . La presse de l'Universite de Cambridge.
- Textes d'introduction
-
Andrew D. Gordon (1994). "Un didacticiel sur la co-induction et la programmation fonctionnelle". 1994 : 78-95. CiteSeerX 10.1.1.37.3914 . Citer le journal nécessite
|journal=( aide ) — description orientée mathématiquement - Bart Jacobs et Jan Rutten (1997). Un didacticiel sur les (co)algèbres et (co)induction ( lien alternatif ) - décrit l'induction et la co-induction simultanément
- Eduardo Giménez et Pierre Castéran (2007). "Un didacticiel sur les types [co-] inductifs en Coq"
- Coinduction — brève introduction
- Histoire
- Davide Sangiorgi . " Sur les origines de la bisimulation et de la coinduction ", Transactions ACM sur les langages et systèmes de programmation, Vol. 31, n° 4, mai 2009.
- Divers
- Programmation co-logique : extension de la programmation logique avec Coinduction - décrit le paradigme de la programmation co-logique