Coinducción

En informática , 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 . ^{[ cita necesaria ]} Los tipos de datos definidos coinductivamente 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 demostrar que una ecuación se satisface con todas las implementaciones posibles de dicha especificación.

Para generar y manipular codatos, normalmente se utilizan funciones correcursivas , junto con una evaluación diferida . Informalmente, en lugar de definir una función mediante la coincidencia 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 de comunicación concurrente. Co-LP tiene aplicaciones para árboles racionales, verificación de propiedades infinitas, evaluación diferida, programación lógica concurrente , verificación de modelos , pruebas de bisimilitud , 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 ver ^[3] ) y SWI-Prolog .

Descripción

En ^[4] se da una declaración concisa tanto del principio de inducción como del principio de coinducción . Si bien este artículo no se ocupa principalmente de la inducción , es útil considerar de inmediato sus formas algo generalizadas. Para enunciar los principios, se requieren algunos preliminares.

Preliminares

Sea un conjunto y sea 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 consistente con F si ${\displaystyle X\subseteq F(X)}$

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

Estos términos se pueden entender intuitivamente de la siguiente manera. Supongamos que es un conjunto de afirmaciones y es la operación que arroja las consecuencias de . Entonces es F-cerrado cuando no puede concluir más de lo que ya ha afirmado, mientras que es F-consistente cuando todas sus afirmaciones están respaldadas por otras afirmaciones (es decir, no hay "supuestos no lógicos F "). ${\displaystyle X}$ ${\displaystyle F(X)}$ ${\displaystyle X}$ ${\displaystyle X}$ ${\displaystyle X}$

El teorema de Knaster-Tarski nos dice que el punto fijo mínimo de (denotado ) está dado por la intersección de todos los conjuntos F-cerrados , mientras que el punto fijo más grande (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 F es 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 es útil considerarlos de la siguiente manera. Supongamos que desea probar una propiedad de . Por el principio de inducción , basta con exhibir un conjunto F-cerrado para el cual se cumple la propiedad. Doblemente, supongamos que desea mostrar eso . Entonces basta con exhibir un conjunto F-consistente del que se sabe que es miembro. ${\displaystyle \mu F}$ ${\displaystyle X}$ ${\displaystyle x\in \nu F}$ ${\displaystyle x}$

Ejemplos

Definir un conjunto de tipos 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 listas (no homogéneas). Estos tipos se pueden identificar con cadenas sobre el alfabeto . Denotemos 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 cadena , símbolo y 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. Usando el principio de inducción , podemos probar 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 llega a la conclusión. ${\displaystyle \Sigma }$ ${\displaystyle F}$

Ahora supongamos que tomamos como nuestro conjunto de tipos de datos. Nos gustaría utilizar el principio de coinducción para probar la siguiente afirmación: ${\displaystyle \nu F}$

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

Aquí denota la lista infinita que consta de todos . 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 consistente con F y, por tanto , . Esto depende de la declaración sospechosa 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 interpretar las cadenas como secuencias , es decir, funciones de . Intuitivamente, el argumento es similar al argumento que (consulte Decimal periódico ). ${\displaystyle \mathbb {N} \rightarrow \Sigma }$ ${\displaystyle 0.{\bar {0}}1=0}$

Tipos de datos coinductivos en lenguajes de programación.

Considere la siguiente definición de flujo : ^[5]

flujo de datos a = S a ( flujo a )       - Corriente "destructores" cabeza ( S a astream ) = una cola ( S a astream ) = astream          

Esta parecería ser una definición que no está bien fundamentada , pero no obstante es útil en programación y se puede razonar sobre ella. En cualquier caso, una secuencia es una lista infinita de elementos de los cuales puedes observar el primer elemento, o colocar un elemento delante para obtener otra secuencia.

Relación con F -coalgebras

Fuente: ^[6]

Considere 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 coalgebra F 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 coalgebra con morfismo asociado . Porque 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}$

tal 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 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 es testigo del isomorfismo , que en términos categóricos indica que es un punto fijo y justifica la notación. ${\displaystyle \nu F\simeq F(\nu F)}$ ${\displaystyle \nu F}$ ${\displaystyle F}$

Stream como coalgebra final

mostraremos que

Corriente A

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

fuera a la corriente = ( cabeza a la corriente , cola a la corriente ) fuera' ( a , a la corriente ) = S a a la corriente            

Se ve fácilmente que estos son mutuamente inversos, lo que atestigua el isomorfismo. Consulte la referencia para obtener más detalles.

Relación con la inducció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 eso . Por lo tanto, por el principio de inducción , si queremos probar alguna propiedad de , basta con demostrar que es F-cerrada . 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 inducción matemática como se dijo.

Ver también

• F-coálgebra
• Corecursión
• bisimulación
• Anamorfismo
• Programación funcional total

Referencias

1. "Programación Co-Logic | Lambda the Ultimate".
2. "Página de inicio de Gopal Gupta".
3. "Logtalk3/Ejemplos/Coinducción en maestro · LogtalkDotOrg/Logtalk3". GitHub .
4. Benjamín C. Pierce . "Tipos y lenguajes de programación". La prensa del MIT .
5. Dexter Kozen , Alexandra Silva . "Coinducción práctica". CiteSeerX 10.1.1.252.3961 . 
6. Ralf Hinze (2012). "Programación genérica con complementos". Programación genérica e indexada . Apuntes de conferencias sobre informática. vol. 7470. Saltador. págs. 47-129. doi :10.1007/978-3-642-32202-0_2. ISBN 978-3-642-32201-3.

Otras lecturas

Libros de texto

• Davide Sangiorgi (2012). Introducción a la Bisimulación y 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). "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", Transacciones ACM sobre lenguajes y sistemas de programación , vol. 31, N° 4, mayo de 2009.

Misceláneas

• 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