Un método para definir y razonar sobre estructuras o comportamientos potencialmente infinitos o circulares, caracterizándolos como puntos fijos máximos de operadores y probando propiedades mediante hipótesis coinductivas como bisimulaciones y observaciones.

Principio

La coinducción establece la pertenencia o equivalencia a un conjunto de punto fijo mayor: para demostrar que un objeto satisface una propiedad coinductiva, hay que mostrar que exhibe los comportamientos observables que la definición coinductiva preserva (a menudo demostrando una bisimulación o una condición de preservación).

Demostración

Las corrientes infinitas (streams) se tratan coinductivamente: para probar que dos streams s y t son iguales, se define una relación de bisimulación R y se muestra (s,t) ∈ R y que R se preserva al tomar cabeza y cola, concluyéndose coinductivamente s = t.

Aplicación incorrecta

Aplicar argumentos de construcción finita al estilo inductivo a estructuras inherentemente no bien fundadas, o usar la coinducción sin verificar la condición de preservación/invarianza (asumiendo así propiedades que no están cerradas bajo el desplegado coalgebraico), es un uso indebido.

Consecuencia

El razonamiento coinductivo permite pruebas sonoras y composicionales sobre datos infinitos, sistemas reactivos y comportamientos (por ejemplo, streams, procesos, árboles infinitos) y admite definiciones por comportamiento observable en lugar de por construcción.

Inversión

La inducción (razonamiento por punto fijo mínimo) es el dual: prueba pertenencia por construcción finita a partir de casos base y constructores, mientras que la coinducción prueba pertenencia mostrando que un elemento no puede distinguirse de los miembros del conjunto coinductivo mediante movimientos observables.

Límite

Aplicable a dominios no bien fundados o corecursivos modelados como coálgebras y a sistemas especificados por puntos fijos máximos; no es apropiada para propiedades que requieren terminación finita o inducción bien fundada sin justificación adicional.

Tensión semántica

Existe tensión entre tratar objetos extensivamente (por comportamiento observable, coinducción) y intensivamente (por construcción, inducción); algunas pruebas solo son convertibles entre ambas bajo restricciones adicionales de finitud o protegidas (guardedness).

Síntesis

El razonamiento coinductivo consiste en probar propiedades de estructuras infinitas o circulares mostrando la preservación del comportamiento observable al desplegarlas; complementa la inducción al centrarse en caracterizaciones por puntos fijos máximos y permite razonar sobre procesos continuos y datos infinitos.