Coinducción

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 .

Descripción

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.

Preliminares

Sea un conjunto y una función monótona , es decir: ${\displaystyle U}$ ${\displaystyle F}$ ${\displaystyle 2^{U}\rightarrow 2^{U}}$

${\displaystyle X\subseteq Y\Rightarrow F(X)\subseteq F(Y)}$

A menos que se indique lo contrario, se asumirá que es monótono. ${\displaystyle F}$

X es F-cerrado si ${\displaystyle F(X)\subseteq X}$

X es F-consistente si ${\displaystyle X\subseteq F(X)}$

X es un punto fijo si ${\displaystyle X=F(X)}$

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"). ${\displaystyle X}$ ${\displaystyle F(X)}$ ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle X}$

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. ${\displaystyle F}$ ${\displaystyle \mu F}$ ${\displaystyle \nu F}$

Definición

Principio de inducción : Si es F-cerrado , entonces ${\displaystyle X}$ ${\displaystyle \mu F\subseteq X}$

Principio de coinducción : Si es F-consistente , entonces ${\displaystyle X}$ ${\displaystyle X\subseteq \nu F}$

Discusió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 . ${\displaystyle \mu F}$ ${\displaystyle X}$ ${\displaystyle x\in \nu F}$ ${\displaystyle x}$

Ejemplos

Definir un conjunto detipos de datos

Considere la siguiente gramática de tipos de datos:

${\displaystyle T=\bot \;|\;\top \;|\;T\times T}$

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 : ${\displaystyle \bot }$ ${\displaystyle \top }$ ${\displaystyle \Sigma =\{\bot ,\top ,\times \}}$ ${\displaystyle \Sigma ^{\leq \omega }}$ ${\displaystyle \Sigma }$ ${\displaystyle F:2^{\Sigma ^{\leq \omega }}\rightarrow 2^{\Sigma ^{\leq \omega }}}$

${\displaystyle F(X)=\{\bot ,\top \}\cup \{x\times y:x,y\in X\}}$

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 . ${\displaystyle x\times y}$ ${\displaystyle x}$ ${\displaystyle \times }$ ${\displaystyle y}$ ${\displaystyle F}$

Supongamos que tomamos como nuestro conjunto de tipos de datos . Utilizando el principio de inducción , podemos demostrar la siguiente afirmación: ${\displaystyle \mu F}$

Todos los tipos de datos son finitos ${\displaystyle \mu F}$

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. ${\displaystyle \Sigma }$ ${\displaystyle F}$

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: ${\displaystyle \nu F}$

El tipo ${\displaystyle \bot \times \bot \times \cdots \in \nu F}$

Aquí se denota la lista infinita que consta de todos los . Para utilizar el principio de coinducción , considere el conjunto: ${\displaystyle \bot \times \bot \times \cdots }$ ${\displaystyle \bot }$

${\displaystyle \{\bot \times \bot \times \cdots \}}$

Este conjunto resulta ser F-consistente y, por lo tanto , . Esto depende de la afirmación sospechosa de que ${\displaystyle \bot \times \bot \times \cdots \in \nu F}$

${\displaystyle \bot \times \bot \times \cdots =(\bot \times \bot \times \cdots )\times (\bot \times \bot \times \cdots )}$

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 ). ${\displaystyle \mathbb {N} \rightarrow \Sigma }$ ${\displaystyle 0.{\bar {0}}1=0}$

Tipos de datos coinductivos en lenguajes de programación

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.

Relación conF -coálgebras

Fuente: ^[6]

Consideremos el endofunctor en la categoría de conjuntos : ${\displaystyle F}$

${\displaystyle F(x)=A\times x}$

${\displaystyle F(f)=\langle \mathrm {id} _{A},f\rangle }$

La F-coálgebra final tiene el siguiente morfismo asociado: ${\displaystyle \nu F}$

${\displaystyle \mathrm {out} :\nu F\rightarrow F(\nu F)=A\times \nu F}$

Esto induce otra coálgebra con morfismo asociado . Como es final , hay un morfismo único. ${\displaystyle F(\nu F)}$ ${\displaystyle F(\mathrm {out} )}$ ${\displaystyle \nu F}$

${\displaystyle {\overline {F(\mathrm {out} )}}:F(\nu F)\rightarrow \nu F}$

de tal manera que

${\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ F(\mathrm {out} )=F\left({\overline {F(\mathrm {out} )}}\circ \mathrm {out} \right)}$

La composición induce otro homomorfismo de la F -coálgebra . Como es final, este homomorfismo es único y por lo tanto . En total tenemos: ${\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} }$ ${\displaystyle \nu F\rightarrow \nu F}$ ${\displaystyle \nu F}$ ${\displaystyle \mathrm {id} _{\nu F}}$

${\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} =\mathrm {id} _{\nu F}}$

${\displaystyle \mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F\left({\overline {F(\mathrm {out} )}}\right)\circ \mathrm {out} )=\mathrm {id} _{F(\nu F)}}$

Esto atestigua el isomorfismo , que en términos categóricos indica que es un punto fijo de y justifica la notación. ${\displaystyle \nu F\simeq F(\nu F)}$ ${\displaystyle \nu F}$ ${\displaystyle F}$

La corriente como coalgebra final

Demostraremos que

Transmisión A

es la coálgebra final del funtor . Considere las siguientes implementaciones: ${\displaystyle F(x)=A\times x}$

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.

Relación coninducción matemática

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: ${\displaystyle P}$

${\displaystyle 0\in P\land (n\in P\Rightarrow n+1\in P)\Rightarrow P=\mathbb {N} }$

Consideremos ahora la función : ${\displaystyle F:2^{\mathbb {N} }\rightarrow 2^{\mathbb {N} }}$

${\displaystyle F(X)=\{0\}\cup \{x+1:x\in X\}}$

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: ${\displaystyle \mu F=\mathbb {N} }$ ${\displaystyle P}$ ${\displaystyle \mathbb {N} }$ ${\displaystyle P}$

${\displaystyle F(P)\subseteq P}$

Eso es,

${\displaystyle \{0\}\cup \{x+1:x\in P\}\subseteq P}$

Esto es precisamente la inducción matemática tal como se afirma.

Véase también

• F-coálgebra
• Corrección
• Bisimulación
• Anamorfismo
• Programación funcional total

Referencias

1. "Programación Co-Logic | Lambda lo último".
2. "Página de inicio de Gopal Gupta".
3. "Logtalk3/Ejemplos/Coinducción en master · LogtalkDotOrg/Logtalk3". GitHub .
4. Benjamin C. Pierce . "Tipos y lenguajes de programación". The MIT Press .
5. Dexter Kozen , Alexandra Silva . "Coinducción práctica". CiteSeerX 10.1.1.252.3961 . 
6. Ralf Hinze (2012). "Programación genérica con adjuntos". Programación genérica e indexada . Apuntes de clase en informática. Vol. 7470. Springer. págs. 47–129. doi :10.1007/978-3-642-32202-0_2. ISBN. 978-3-642-32201-3.

Lectura adicional

Libros de texto

• Davide Sangiorgi (2012). Introducción a la bisimulación y la coinducción . Cambridge University Press.
• Davide Sangiorgi y Jan Rutten (2011). Temas avanzados en bisimulación y coinducción . Cambridge University Press.

Textos introductorios

• Andrew D. Gordon (1994). "Un tutorial sobre coinducción y programación funcional". 1994. págs. 78–95. CiteSeerX 10.1.1.37.3914 . — descripción orientada matemáticamente
• Bart Jacobs y Jan Rutten (1997). Un tutorial sobre (co)álgebras y (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 tipos [co-]inductivos en Coq"
• Coinducción: breve introducción

Historia

• Davide Sangiorgi . "Sobre los orígenes de la bisimulación y la coinducción", ACM Transactions on Programming Languages ​​and Systems , vol. 31, n.º 4, mayo de 2009.

Misceláneas

• Programación co-lógica: extensión de la programación lógica con coinducción: describe el paradigma de programación co-lógica