Coinducción - Coinduction
En ciencias de la computación , la coinducción es una técnica para definir y probar propiedades de sistemas de objetos que interactúan concurrentes .
La coinducción es el dual matemático de la inducción estructural . Los tipos definidos de forma coinductiva se conocen como codatos y suelen ser estructuras de datos infinitas , como flujos .
Como definición o especificación , la coinducción describe cómo un objeto puede ser "observado", "descompuesto" o "destruido" en objetos más simples. Como técnica de prueba , se puede utilizar para mostrar que todas las posibles implementaciones de dicha especificación satisfacen una ecuación .
Para generar y manipular codatos, normalmente se utilizan funciones corecursivas , junto con la evaluación perezosa . De manera informal, en lugar de definir una función haciendo coincidir patrones en cada uno de los constructores inductivos, se define cada uno de los "destructores" u "observadores" sobre el resultado de la función.
En programación, la programación co-lógica (co-LP para abreviar) "es una generalización natural de la programación lógica y la programación lógica coinductiva, que a su vez generaliza otras extensiones de la programación lógica, como árboles infinitos, predicados perezosos y predicados comunicantes concurrentes. Co-LP tiene aplicaciones para árboles racionales, verificación de propiedades infinitarias, evaluación diferida, programación lógica concurrente, verificación de modelos, pruebas de bisimilitud , etc. " Las implementaciones experimentales de co-LP están disponibles en la Universidad de Texas en Dallas y en Logtalk (para ver ejemplos, consulte) y SWI-Prolog .
Ver también
Referencias
Otras lecturas
- Libros de texto
- Davide Sangiorgi (2012). Introducción a la bisimulación y la coinducción . Prensa de la Universidad de Cambridge.
- Davide Sangiorgi y Jan Rutten (2011). Temas avanzados en Bisimulación y Coinducción . Prensa de la Universidad de Cambridge.
- Textos introductorios
-
Andrew D. Gordon (1994). "Tutorial de Coinducción y Programación Funcional". 1994: 78–95. CiteSeerX 10.1.1.37.3914 . Cite journal requiere
|journal=( ayuda ) - descripción orientada matemáticamente - Bart Jacobs y Jan Rutten (1997). Un tutorial sobre (Co) álgebras e (Co) inducción ( enlace alternativo ): describe la inducción y la coinducción simultáneamente
- Eduardo Giménez y Pierre Castéran (2007). "Un tutorial sobre [Co-] tipos inductivos en Coq"
- Coinducción - breve introducción
- Historia
- Davide Sangiorgi . " Sobre los orígenes de la bisimulación y la coinducción ", Transacciones ACM sobre lenguajes y sistemas de programación, vol. 31, N ° 4, mayo de 2009.
- Diverso
- Programación Co-Lógica: Ampliación de la Programación Lógica con Coinducción - describe el paradigma de programación co-lógica