En informática , la coinducción es una técnica para definir y probar propiedades de sistemas de objetos que interactúan simultáneamente .
La coinducción es el dual matemático de la inducción estructural . [ cita requerida ] Los tipos de datos 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 , puede utilizarse para demostrar que una ecuación se satisface con todas las posibles implementaciones de dicha especificación.
Para generar y manipular codatos, normalmente se utilizan funciones recursivas conjuntas con la evaluación diferida . De manera informal, en lugar de definir una función mediante la comparación de 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 en árboles racionales, verificación de propiedades infinitarias, evaluación perezosa, programación lógica concurrente , verificación de modelos , pruebas de bisimilaridad , etc." [1] Las implementaciones experimentales de co-LP están disponibles en la Universidad de Texas en Dallas [2] y en el lenguaje Logtalk (para ejemplos, consulte [3] ) y SWI-Prolog .
En [4] se enuncia de forma concisa tanto el principio de inducción como el principio de coinducción . Aunque este artículo no se ocupa principalmente de la inducción , resulta útil considerar de inmediato sus formas algo generalizadas. Para enunciar los principios, se requieren algunas consideraciones preliminares.
Sea un conjunto y una función monótona , es decir:
A menos que se indique lo contrario, se asumirá que es monótono.
Estos términos pueden entenderse intuitivamente de la siguiente manera. Supongamos que es un conjunto de afirmaciones, y es la operación que produce las consecuencias de . Entonces es F-cerrado cuando no se puede concluir más de lo que ya se ha afirmado, mientras que es F-consistente cuando todas las afirmaciones están respaldadas por otras afirmaciones (es decir, no hay "suposiciones no F -lógicas").
El teorema de Knaster-Tarski nos dice que el punto fijo menor de (denotado ) está dado por la intersección de todos los conjuntos F-cerrados , mientras que el punto fijo mayor (denotado ) está dado por la unión de todos los conjuntos F-consistentes . Ahora podemos enunciar los principios de inducción y coinducción.
Los principios, como se han dicho, son algo opacos, pero se pueden considerar de la siguiente manera. Supóngase que se desea demostrar una propiedad de . Por el principio de inducción , basta con demostrar un conjunto F-cerrado para el que se cumple la propiedad. Dualmente, supóngase que se desea demostrar que . Entonces basta con demostrar un conjunto F-consistente que se sabe que es miembro de .
Considere la siguiente gramática de tipos de datos:
Es decir, el conjunto de tipos incluye el "tipo inferior" , el "tipo superior" y las listas (no homogéneas). Estos tipos se pueden identificar con cadenas sobre el alfabeto . Sea . todas las cadenas (posiblemente infinitas) sobre . Considere la función :
En este contexto, significa "la concatenación de la cadena , el símbolo y la cadena ." Ahora deberíamos definir nuestro conjunto de tipos de datos como un punto fijo de , pero importa si tomamos el punto fijo menor o mayor .
Supongamos que tomamos como nuestro conjunto de tipos de datos . Utilizando el principio de inducción , podemos demostrar la siguiente afirmación:
Para llegar a esta conclusión, considere el conjunto de todas las cadenas finitas sobre . Claramente no se puede producir una cadena infinita, por lo que resulta que este conjunto es F-cerrado y se deduce la conclusión.
Supongamos ahora que tomamos como conjunto de tipos de datos . Nos gustaría utilizar el principio de coinducción para demostrar la siguiente afirmación:
Aquí se denota la lista infinita que consta de todos los . Para utilizar el principio de coinducción , considere el conjunto:
Este conjunto resulta ser F-consistente y, por lo tanto , . Esto depende de la afirmación sospechosa de que
La justificación formal de esto es técnica y depende de la interpretación de cadenas como secuencias , es decir, funciones de . Intuitivamente, el argumento es similar al argumento que (ver Decimal periódico ).
Consideremos la siguiente definición de un flujo : [5]
Flujo de datos a = S a ( Flujo a ) -- "Destructores" de flujo cabeza ( S a astream ) = a cola ( S a astream ) = astream
Esta parecería ser una definición poco fundamentada , pero es útil en programación y se puede razonar al respecto. En cualquier caso, un stream es una lista infinita de elementos de la que se puede observar el primer elemento o colocar un elemento delante para obtener otro stream.
Fuente: [6]
Consideremos el endofunctor en la categoría de conjuntos :
La F-coálgebra final tiene el siguiente morfismo asociado:
Esto induce otra coálgebra con morfismo asociado . Como es final , hay un morfismo único.
de tal manera que
La composición induce otro homomorfismo de F -coálgebra . Como es final, este homomorfismo es único y por lo tanto . En total tenemos:
Esto atestigua el isomorfismo , que en términos categóricos indica que es un punto fijo de y justifica la notación.
Demostraremos que
Transmisión A
es la coálgebra final del funtor . Considere las siguientes implementaciones:
fuera un flujo = ( cabeza un flujo , cola un flujo ) fuera' ( a , un flujo ) = S a un flujo
Se puede ver fácilmente que son mutuamente inversos, lo que demuestra el isomorfismo. Consulte la referencia para obtener más detalles.
Demostraremos cómo el principio de inducción incluye la inducción matemática. Sea alguna propiedad de los números naturales . Tomaremos la siguiente definición de inducción matemática:
Consideremos ahora la función :
No debería ser difícil ver que . Por lo tanto, por el principio de inducción , si deseamos demostrar alguna propiedad de , basta con demostrar que es F-cerrado . En detalle, requerimos:
Eso es,
Esto es precisamente la inducción matemática tal como se afirma.