Coinducción

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

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

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

• X es F-cerrado si${\displaystyle F(X)\subseteq X}$
• X es F-consistente si${\displaystyle X\subsetequ F(X)}$
• X es un punto fijo si${\displaystyle X=F(X)}$

Estos términos pueden entenderse intuitivamente de la siguiente manera. Supongamos que${\displaystyle X}$es un conjunto de afirmaciones, y${\displaystyle F(X)}$es la operación que produce las consecuencias de${\displaystyle X}$. Entonces${\displaystyle X}$es F-cerrado cuando no se puede concluir nada más de lo que ya se ha afirmado, mientras que${\displaystyle X}$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 más pequeño de${\displaystyle F}$(denotado${\displaystyle \mu F}$) viene dado por la intersección de todos los conjuntos F-cerrados , mientras que el mayor punto fijo (denotado${\displaystyle \nu F}$) viene dado por la unión de todos los conjuntos F-consistentes . Ahora podemos enunciar los principios de inducción y coinducción.

• Principio de inducción : Si${\displaystyle X}$es F-cerrado , entonces${\displaystyle \mu F\subsetequ X}$
• Principio de coinducción : Si${\displaystyle X}$es F-consistente , entonces${\displaystyle X\subsetequ \nu F}$

Consideremos 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".${\displaystyle \bot }$, el "tipo superior"${\displaystyle \top }$y tipos de productos. Estos tipos se pueden identificar con cadenas sobre el alfabeto.${\displaystyle \Sigma =\{\bot ,\top ,\times \}}$. Dejar${\displaystyle \Sigma ^{\leq \omega }}$denotan todas las cadenas (posiblemente infinitas) sobre${\displaystyle \Sigma }$. Consideremos la función${\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,${\displaystyle x\times y}$significa "la concatenación de cadena"${\displaystyle x}$, el símbolo${\displaystyle \times }$y cuerda${\displaystyle y}$." Ahora deberíamos definir nuestro conjunto de tipos de datos como un punto fijo de${\displaystyle F}$, pero importa si tomamos el punto fijo menor o el mayor .

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

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

Para llegar a esta conclusión, consideremos el conjunto de todas las cadenas finitas sobre${\displaystyle \Sigma }$. Claramente${\displaystyle F}$no puede producir una cadena infinita, por lo que resulta que este conjunto es F-cerrado y la conclusión se deduce.

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

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

Aquí${\displaystyle \bot \times \bot \times \cdots }$denota la cadena infinita${\displaystyle (\bot ,\times ,\bot ,\times ,\ldots )}$Para utilizar el principio de coinducción , consideremos el siguiente conjunto:

$${\displaystyle S=\{\bot ,\;\bot \times \bot \times \cdots \}}$$

Este conjunto es F-consistente . Primero,${\displaystyle \bot \in \{\bot ,\top \}\subseteq F(S)}$Segundo, puesto que${\displaystyle \bot \in S}$y${\displaystyle \bot \times \bot \times \cdots \in S}$, tenemos${\displaystyle \bot \times (\bot \times \bot \times \cdots )\in F(S)}$. Interpretación de cadenas como secuencias (funciones de${\displaystyle \mathbb {N} \rightarrow \Sigma }$), anteponiendo el prefijo finito${\displaystyle \bot \times }$a la cadena infinita${\displaystyle \bot \times \bot \times \cdots }$rendimientos${\displaystyle \bot \times \bot \times \cdots }$sí mismo, así que${\displaystyle \bot \times \bot \times \cdots \in F(S)}$. Por lo tanto${\displaystyle S\subseteq F(S)}$y por el principio de coinducción ,${\displaystyle \bot \times \bot \times \cdots \in \nu F}$.

Nota. La representación de tipos como cadenas sobre${\displaystyle \Sigma }$no es fiel a la estructura de árbol subyacente. Cadenas finitas como${\displaystyle \bot \times \top \times \bot }$son ambiguos sin corchetes, y para cualquier cadena infinita${\displaystyle s}$la concatenación${\displaystyle s\times t=s}$a pesar de${\displaystyle t}$, de modo que se pueden identificar árboles distintos. Esto no afecta al argumento anterior, que solo ilustra el principio de coinducción a través de la consistencia F , pero importaría en entornos donde se debe preservar la estructura del constructor. Un tratamiento estructural estándar representa los tipos a través del isomorfismo${\displaystyle T\cong 1+1+(T\times T)}$; consulte F-coalgebra para obtener más detalles.

Consideremos la siguiente definición de un flujo en Haskell : ^{[ 5 ]}

Flujo de datos a = S a ( Flujo a )-- Destructores de flujo cabeza :: Flujo a -> a cabeza ( S a flujo a ) = a cola :: Flujo a -> Flujo a cola ( S a flujo a ) = a flujo

La primera línea indica que un flujo se compone de un elemento seguido de otro flujo (S es un constructor de elementos, y a denota un tipo arbitrario para los elementos). Dado que no existe un caso base , esta definición parecería poco fundamentada , pero no obstante resulta útil en programación y se puede razonar sobre ella. En cualquier caso, un flujo es una lista infinita de elementos de la que se puede observar el primer elemento o colocar un elemento delante para obtener otro flujo.

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

$${\displaystyle {\begin{aligned}F(x)&=A\times x\\F(f)&=\langle \mathrm {id} _{A},f\rangle \end{aligned}}}$$

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

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

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

$${\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${\displaystyle {\overline {F(\mathrm {out} )}}\circ \mathrm {out} }$induce otro homomorfismo de F -coalgebra${\displaystyle \nu F\rightarrow \nu F}$. Desde${\displaystyle \nu F}$es final, este homomorfismo es único y por lo tanto${\displaystyle \mathrm {id} _ {\nu F}}$En total tenemos:

$${\displaystyle {\begin{aligned}{\overline {F(\mathrm {out} )}}\circ \mathrm {out} &=\mathrm {id} _{\nu F}\\[0.5ex]\mathrm {out} \circ {\overline {F(\mathrm {out} )}}=F{\bigl (}{\overline {F(\mathrm {out} )}}\circ \mathrm {fuera} {\bigr )}&=\mathrm {id} _ {F(\nu F)}\end{aligned}}}$$

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

salida astream = ( cabeza astream , cola astream ) salida' ( a , astream ) = S a astream

Demostraremos cómo el principio de inducción engloba la inducción matemática. Sea${\displaystyle P}$Sea alguna propiedad de los números naturales . Tomaremos la siguiente definición de inducción matemática:

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

Ahora consideremos 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${\displaystyle \mu F=\mathbb {N} }$Por lo tanto, por el principio de inducción , si deseamos demostrar alguna propiedad${\displaystyle P}$de${\displaystyle \mathbb {N} }$, basta con demostrar que${\displaystyle P}$es F-cerrado . En detalle, requerimos:

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

Eso es,

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

Esto es precisamente inducción matemática, tal como se ha dicho.