CINVCAT/Coálgebras, coinducción

Ya hace varias décadas que las estructuras de datos trataron de describirse de manera algebraica, y con éxito varias de ellas. Sin embargo, hay otras estructuras de datos que no pueden describirse algebraicamente de manera apropiada. Con el tiempo, comenzó a entenderse que tales estructuras quedaban mejor modeladas coalgebraicamente, como las estructuras que implican una noción de estado que puede cambiar; por ejemplo, los sistemas de transición, los autómatas, la semántica de programación orientada a objetos, los automorfismos parciales, los números reales, las listas infinitas, las series de potencias formales, etc.
     Volviendo a las álgebras, desde el punto de vista del álgebra universal, se tiene que las signaturas de operaciones inducen ciertos funtores polinomiales y que las álgebras de estos funtores corresponden a las álgebras o modelos de las signaturas. Si generalizamos, dado un funtor $F:\mathbf{Con}\rightarrow\mathbf{Con}$, un álgebra de $F:\mathbf{Con}\rightarrow\mathbf{Con}$ (o una $F$-álgebra) es un par $(B,\beta:FB\rightarrow B)$, donde $B\in\mathbf{Con}$ y $\beta$ es una función. Dualmente, una coálgebra de $F$ (o una $F$-coálgebra) es un par $(A,\alpha:A\rightarrow FA)$, con $A\in\mathbf{Con}$ y $\alpha$ una función.
     Ahora, la inducción, como principio para definir o demostrar, se utiliza para las estructuras algebraicas que son generadas por una colección de constructores (u operaciones constructoras) —como los números naturales, que son generados por $0:1\rightarrow\mathbb{N}$ y $s:\mathbb{N}\rightarrow\mathbb{N}$, o como las listas y los árboles finitos—. Estas estructuras algebraicas son las álgebras iniciales en la categoría de álgebras de algún funtor pertinente; más precisamente, el principio de inducción en una estructura, como en el conjunto de los números naturales $\mathbb{N}$ o en el conjunto de las listas finitas $A^\ast$ sobre $A$, puede reformularse como la inicialidad de esa estructura en la categoría de álgebras de algún funtor. Dualmente, la terminalidad en la categoría de coálgebras de un funtor nos da un principio de coinducción para la cóalgebra terminal (o final) de esa categoría. La coálgebra terminal viene equipada con destructores u operaciones destructoras (también llamadas observadores, accesores, mapeos de transición o mutadores), las cuales la cogeneran. Volviendo a la inducción y siguiendo con la correspondencia entre inducción y la inicialidad, esta implica existencia única: la existencia corresponde a definir por inducción y la unicidad a demostrar por inducción. Tal correspondencia también se tiene para la coinducción.
     La coinducción puede formularse de manera alternativa mediante el concepto de bisimulación, que es una relación sobre una coálgebra que es cerrada de manera apropiada bajo las operaciones coalgebraicas de la coálgebra; tales relaciones se pueden entender como el concepto dual de congruencia, que es una relación cerrada bajo operaciones algebraicas.      Volviendo a las álgebras, expliquemos de manera más precisa la correspondencia entre álgebras de una signatura y las álgebras de funtores polinomiales. Sea $\Sigma$ una signatura (monoespécica), así que, dada una $\Sigma$-álgebra $X$ y $\sigma\in\Sigma$, se tiene una operación $$\sigma_X:\underbrace{X\times\cdots\times X}_{\mathrm{ar}(\sigma)\text{ veces}}\rightarrow X,$$ donde $\mathrm{ar}(\sigma)$ es la aridad de $\sigma$. Así que si $\Sigma=\{\sigma_1,\ldots,\sigma_n\}$, podemos asociarle a $\Sigma$ el funtor $T_\Sigma:\mathbf{Con}\rightarrow\mathbf{Con}$ dado como $$T_\Sigma X:=X^{\mathrm{ar}(\sigma_1)}+\cdots +X^{\mathrm{ar}(\sigma_n)}.$$ Ahora, la estructura algebraica $\beta:T_\Sigma X\rightarrow X$ de un álgebra $X$ del funtor $T_\Sigma$ puede identificarse con una $n$-cotupla $$\beta=[\beta_1,\ldots,\beta_n]:X^{\mathrm{ar}(\sigma_1)}+\cdots +X^{\mathrm{ar}(\sigma_n)}\rightarrow X$$ de funciones $\beta_i:X^{\mathrm{ar}(\sigma_i)}\rightarrow X$. De aquí, las álgebras de $T_\Sigma$ corresponden a los modelos de $\Sigma$, las $\Sigma$-álgebras. Es decir, los funtores polinomiales construidos a partir del funtor identidad, productos y coproductos tienen como álgebras las álgebras que son modelos de signaturas. Un ejemplo sencillo de tales funtores es el funtor $1+(-):\mathbf{Con}\rightarrow\mathbf{Con}$, una de cuyas álgebras es $(\mathbb{N},[0,s]:1+\mathbb{N}\rightarrow\mathbb{N})$, donde $0:1\rightarrow\mathbb{N}$ es el cero y $s:\mathbb{N}\rightarrow\mathbb{N}$ la función sucesor.
     Otros funtores polinomiales importantes son aquellos en los que aparecen conjuntos constantes, como el funtor $1+A\times (-):\mathbf{Con}\rightarrow\mathbf{Con}$, una de cuyas álgebras es el álgebra de listas finitas sobre el conjunto $A$; o sea, $(A^\ast,[\mathrm{\textbf{nil}},\mathrm{\textbf{cons}}]:1+A\times A^\ast\rightarrow A^\ast)$, con $\mathrm{\textbf{nil}}:1\rightarrow A^\ast$ la lista vacía y $\mathrm{\textbf{cons}}:A\times A^\ast\rightarrow A$ la prefijación de un elemento de tipo $A$ a una lista; o como el funtor $1+X\times A\times X$, una de cuyas álgebras es el álgebra de árboles finitos binarios enraizados con nodos en $A$; o sea, $(\mathrm{\textbf{Árbol}}(A),[\mathrm{\textbf{nil}},\mathrm{\textbf{nodo}}]:1+\mathrm{\textbf{Árbol}}(A)\times A\times\mathrm{\textbf{Árbol}}(A)\rightarrow\mathrm{\textbf{Árbol}}(A))$, con $\mathrm{\textbf{nil}}:1\rightarrow\mathrm{\textbf{Árbol}}(A)$ el árbol binario enraizado vacío y $\mathrm{\textbf{nodo}}:\mathrm{\textbf{Árbol}}(A)\times A\times\mathrm{\textbf{Árbol}}(A)\rightarrow\mathrm{\textbf{Árbol}}(A)$ la construcción de un árbol binario enraizado a partir de dos (sub)árboles y una raíz en $A$.
     Pasemos a las coálgebras y veamos algunos ejemplos. Consideremos una máquina que es una caja negra y que tiene dos botones, $\mathrm{\textbf{val}}$ y $\mathrm{\textbf{sig}}$. Presionar el botón $\mathrm{\textbf{val}}$ resulta en alguna indicación visible del estado interno de la máquina, indicación cuyos valores están en el conjunto de datos $A$; tal operación no afecta el estado interno de la máquina, así que presionar dos veces $\mathrm{\textbf{val}}$ da el mismo resultado. Si uno presiona el botón $\mathrm{\textbf{sig}}$, la máquina cambia de estado, cuyo valor puede inspeccionarse al presionar nuevamente $\mathrm{\textbf{val}}$. Esta máquina puede describirse de manera abstracta como una coálgebra con mapeo de estructura $$(\mathrm{\textbf{val}},\mathrm{\textbf{sig}}):X\rightarrow A\times X,$$ donde $X$ es el espacio de estados (internos) de la máquina. Un coálgebra del funtor $A\times(-)$ es la coálgebra de listas infinitas sobre $A$; a saber, $(A^\mathbb{N},(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}}):A^\mathbb{N}\rightarrow A\times A^\mathbb{N})$, donde $\mathrm{\textbf{cab}}:A^\mathbb{N}\rightarrow A$ nos da el primer elemento de una lista infinita y $\mathrm{\textbf{cola}}:A^\mathbb{N}\rightarrow A^\mathbb{N}$ nos da la lista que resulta de quitar el primer elemento de la lista. Otra máquina caja negra podría ser una con un botón y una luz. La máquina realiza una acción sólo si el botón es presionado y la luz se enciende sólo si la máquina se detiene por completo; así que lo único que podríamos observar es su comportamiento tras presionar el botón y si se enciende la luz. Esta máquina puede describirse como una coálgebra con mapeo de estructura $$\mathrm{\textbf{botón}}:X\rightarrow 1+X,$$ donde $\mathrm{\textbf{botón}}\, s=\ast$ si la máquina deja de operar tras presionar el botón y se enciende la luz, y $\mathrm{\textbf{botón}}\,s\in X$ si la máquina no deja de operar y ha cambiado de estado. Una coálgebra del funtor $1+(-):\mathbf{Con}\rightarrow\mathbf{Con}$ es $(\overline{\mathbb{N}},\mathrm{\textbf{pred}}:\overline{\mathbb{N}}\rightarrow 1+\overline{\mathbb{N}})$, donde $\overline{\mathbb{N}}:=\mathbb{N}+\{\infty\}$ y $\mathrm{\textbf{pred}}(0):=\ast$, $\mathrm{\textbf{pred}}(n+1):=n$ y $\mathrm{\textbf{pred}}(\infty):=\infty$.      Volvamos a las álgebras y expliquemos mediante el ejemplo de los números naturales la correspondencia entre inducción e inicialidad. La $1+(-)$-álgebra $(\mathbb{N},[0,s])$ es álgebra inicial en la categoría de álgebras del funtor $1+(-):\mathbf{Con}\rightarrow\mathbf{Con}$. En efecto, sean $A\in \mathbf{Con}$, $\varphi : \mathbb{N} \rightarrow A$ una función y $[d,r] : 1+A \rightarrow A$ una $1+(-)$-álgebra. Entonces, considérense los siguientes diagramas: $$\begin{xy} \xymatrix{ 1 \ar[d]_1 \ar[r] & 1+\mathbb{N} \ar[d]^{1+\varphi} & \mathbb{N} \ar[l] \ar[d]^{\varphi} & 1 \ar[r] \ar[rd]_0 & 1+\mathbb{N} \ar[d]^{[0,s]} & \mathbb{N} \ar[l] \ar[ld]^s \\ 1 \ar[r] \ar[rd]_d & 1+A \ar[d]^{[d,r]} & A \ar[l] \ar[ld]^r & & \mathbb{N} \ar[d]^{\varphi} & \\ & A & & & A & . }\end{xy}$$ De aquí, $$\begin{xy} \xymatrix{ 1+\mathbb{N} \ar[r]^{1+\varphi} \ar[d]_{[0,s]} \ar@{}[rd]|{=} & 1+A \ar[d]^{[d,r]} \ar@{}[rd]^(.6){\Leftrightarrow} & 1 \ar[r]^0 \ar@<-.5ex>[rd]_d \ar@<.5ex>@{}[rd]^{=} & \mathbb{N} \ar[r]^s \ar[d]^{\varphi} \ar@{}[rd]|{=} & \mathbb{N} \ar[d]^{\varphi} \\ \mathbb{N} \ar[r]_{\varphi} & A & & A \ar[r]_r & A; }\end{xy}$$ entonces, si $\varphi$ es un homomorfismo de álgebras, $\varphi$ tiene que cumplir que para todo $n\in \mathbb{N}$ $$\begin{xy} \xymatrix{ & 1 \ar[d]^0 \ar[ld]_d \\ A \ar[d]_{r^n} & \mathbb{N} \ar[l]_{\varphi} \ar[d]^{s^n} \\ A & \mathbb{N} \ar[l]^{\varphi} }\end{xy}$$ conmuta; por lo tanto, $\varphi n = r^n d$ para todo $n\in \mathbb{N}$.
     Luego, $(\mathbb{N},[0,s] : 1+\mathbb{N} \rightarrow \mathbb{N})$ es inicial.
     Observemos que pudimos haber obtenido el conjunto portador del álgebra inicial del funtor $1+(-)$ como el conjunto de los términos cerrados (los términos básicos —ground terms en inglés—, los que no tienen variables), es decir, de aquellos términos que son generados al aplicar iteradamente los constructores $\mathbf{0}:1\rightarrow X$ y $\mathbf{S}:X\rightarrow X$ de un álgebra cualquiera $(X,[\mathbf{0},\mathbf{S}]:1+X\rightarrow X)$ de $1+(-)$: $$\{\mathbf{0},\mathbf{S}\mathbf{0},\mathbf{S}\mathbf{S}\mathbf{0},\mathbf{S}\mathbf{S}\mathbf{S}\mathbf{0},\ldots\}.$$ En general, el conjunto portador del álgebra inicial de un funtor $T$ se puede obtener a partir de los términos cerrados, es decir, a partir de aquellos que son generados al aplicar iteradamente los constructores de un álgebra de $T$.
     Ahora el principio de inducción en los naturales usado como principio de demostración normalmente se formula de la siguiente manera: un subcojunto $P$ de $\mathbb{N}$ es igual a $\mathbb{N}$ si $0\in P$ y $n\in P\Rightarrow n+1\in P$. Reformulándolo, las suposiciones inductivas sobre $P$ esencialmente dicen que $P$ tiene una estructura de álgebra $0' : 1 \rightarrow P$, $s' : P \rightarrow P$ tal que la función inclusión $i : P \rightarrow \mathbb{N}$ es un homomorfismo de álgebras: $$\begin{xy} \xymatrix{ 1+P \ar[r]^{1+i} \ar[d]_{[0',s']} & 1+\mathbb{N} \ar[d]^{[0,s]} \\ P \ar[r]_i & \mathbb{N}. }\end{xy}$$ Es decir, $P$ es una subálgebra de $\mathbb{N}$. Ahora, de la inicialidad de $(\mathbb{N},[0,s])$, existe un homomorfismo $j : \mathbb{N} \rightarrow P$; nuevamente, por la inicialidad de $(\mathbb{N},[0,s])$, $i\circ j = 1_{\mathbb{N}}$: $$\begin{xy} \xymatrix{ 1+\mathbb{N} \ar[r]^{1+j} \ar[d]_{[0,s]} \ar@/^2pc/[rr]^{1+1_{\mathbb{N}}} & 1+P \ar[r]^{1+i} \ar[d]^{[0',s']} & 1+\mathbb{N} \ar[d]^{[0,s]} \\ \mathbb{N} \ar[r]_j \ar@/_2pc/[rr]_{1_{\mathbb{N}}} & P \ar[r]_i & \mathbb{N}; }\end{xy}$$ de aquí, $P = \mathbb{N}$.
     Veamos un ejemplo de cómo usar la inicialidad para las definiciones por inducción. Supongamos que queremos definir por inicialidad la función $fn=2^{-n}$ de los números naturales $\mathbb{N}$ a los racionales $\mathbb{Q}$. Las ecuaciones inductivas que la definen son $$f0:=1\qquad\text{y}\qquad f(n+1):=\frac{1}{2}fn.$$ Para definir esta función $f:\mathbb{N}\rightarrow\mathbb{Q}$ por inicialidad, hay que dotar a $\mathbb{Q}$ de una estructura de álgebra $1+\mathbb{Q}\rightarrow\mathbb{Q}$. Esta álgebra sobre $\mathbb{Q}$ corresponde al lado derecho de las dos ecuaciones inductivas que definen a $f$: $$\begin{xy} \xymatrix{ 1\ar[r]^1 & \mathbb{Q} & & \mathbb{Q}\ar[r]^{\frac{1}{2}(-)} & \mathbb{Q} }\end{xy}$$ $$\begin{xy} \xymatrix{ \ast\ar@{|->}[r] & 1 & & \ x\ar@{|->}[r] & \frac{1}{2}x. }\end{xy}$$ Entonces, $fn=2^{-n}$ está determinada por inicialidad como la única función que hace conmutar el siguiente diagrama: $$\begin{xy} \xymatrix{ 1+\mathbb{N}\ar[rr]^{1+f}\ar[d]_{[0,s]} & & 1+\mathbb{Q}\ar[d]^{[1,\frac{1}{2}(-)]}\\ \mathbb{N}\ar[rr]_f & & \mathbb{Q} }\end{xy}$$ La conmutatividad del diagrama nos da de vuelta las ecuaciones inductivas que definen a $f$. Notemos que los constructores $0$ y $s$ aparecen “dentro” de la función $f$, que estamos definiendo: $f0=1$ y $fsn=fn$.
     Esto muestra cómo se puede usar la inicialidad para definir funciones por inducción: hay que dotar al codominio de la función en cuestión de un estructura algebraica apropiada que corresponda a las cláusulas inductivas que determinan a dicha función. Además, en las definiciones inductivas, los constructores aparecen “dentro” de la función que se desea definir. Resumiendo: definir por inicialidad a una función es dotar a su codominio de una estructura algebraica apropiada que nos da la existencia de la función a definir, el diagrama conmutativo nos da las ecuaciones inductivas que determinan a la función; recíprocamente, las ecuaciones inductivas que definen a una función nos dan la estructura algebraica apropiada del codominio de la función para obtener su existencia mediante la inicialidad.
     Volvamos a las coálgebras y veamos la correspondencia entre terminalidad y coinducción. La coálgebra terminal (o final) del funtor $A\times(-):\mathbf{Con}\rightarrow\mathbf{Con}$ es $(A^\mathbb{N},(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}}))$, donde $\mathrm{\textbf{cab}}\,\sigma=\sigma\,0$ y $\mathrm{\textbf{cola}}\,\sigma=\lambda x.\sigma(x+1)$. En efecto, considérense los siguientes diagramas: $$\begin{xy} \xymatrix{ & X\ar[d]^{(\mathrm{\textbf{val}},\mathrm{\textbf{sig}})}\ar[dl]_{\mathrm{\textbf{val}}}\ar@/^0.9pc/[dr]^{\mathrm{\textbf{sig}}} & & & X\ar[d]^\varphi &\\ A\ar[d]_1 & A\times X\ar[r]\ar[l]\ar[d]^{A\times\varphi} & X\ar[d]^\varphi & & A^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})}\ar@/^1.3pc/[dr]^{\mathrm{\textbf{cola}}}\ar[dl]_{\mathrm{\textbf{cab}}} &\\ A & A\times A^\mathbb{N}\ar[r]\ar[l] & A^\mathbb{N} & A & A\times A^\mathbb{N}\ar[r]\ar[l] & A^\mathbb{N}. }\end{xy}$$ De aquí, $$\begin{xy} \xymatrix{ X \ar[r]^\varphi \ar[d]_{(\mathrm{\textbf{val}},\mathrm{\textbf{sig}})} \ar@{}[rd]|{=} & A^\mathbb{N} \ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})} \ar@{}[drr]^(.65){\Leftrightarrow} & & & X\ar@<-.5ex>[dl]_{\mathrm{\textbf{val}}}\ar@<.5ex>@{}[dl]^{=} \ar[d]^\varphi \ar@{}[rd]|{=} & X \ar[l]_{\mathrm{\textbf{sig}}}\ar[d]^\varphi \\ A\times X \ar[r]_{A\times\varphi} & A\times A^\mathbb{N} & & A & A^\mathbb{N}\ar[l]^{\mathrm{\textbf{cab}}} & A^\mathbb{N}\ar[l]^{\mathrm{\textbf{cola}}} }\end{xy}$$ entonces, si $\varphi$ es un homomorfismo de coálgebras, $\varphi$ tiene que cumplir que para todo $n\in \mathbb{N}$ $$\begin{xy} \xymatrix{ X \ar[r]^\varphi \ar[d]_{\mathrm{\textbf{sig}}^n} & A^\mathbb{N} \ar[d]^{\mathrm{\textbf{cola}}^n} \\ X \ar[r]_\varphi \ar[rd]_{\mathrm{\textbf{val}}} & A^\mathbb{N} \ar[d]^{\mathrm{\textbf{cab}}} \\ & A }\end{xy}$$ conmuta; por lo tanto, $\varphi(x)(n)=\mathrm{\textbf{val}}(\mathrm{\textbf{sig}}^nx)$ para todo $n\in\mathbb{N}$, ya que $\varphi(x)(n)=\mathrm{\textbf{cab}}(\mathrm{\textbf{cola}}^n\varphi x)$ para todo $n\in\mathbb{N}$.
     Luego, $(A^\mathbb{N},(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}}):A^\mathbb{N}\rightarrow A\times A^\mathbb{N})$ es terminal.
     Observemos que pudimos haber obtenido el conjunto portador de la coálgebra terminal del funtor $A\times(-)$ como el conjunto de todos los posibles comportamientos de un elemento $x\in X$, el conjunto de los comportamientos que se podría observar de $x$; es decir, podemos obtener el portador de la coálgebra del funtor $A\times(-)$ al aplicar iteradamente los observadores $\mathrm{\textbf{cab}}:X\rightarrow A$ y $\mathrm{\textbf{sig}}:X\rightarrow X$ a cualquier elemento $x$ de una coálgebra cualquiera $(X,(\mathrm{\textbf{val}},\mathrm{\textbf{sig}}):X\rightarrow A\times X)$ de $A\times(-)$: todas las posibles listas infinitas $$(\mathrm{\textbf{val}}\,x,\mathrm{\textbf{val}}(\mathrm{\textbf{sig}}\,x),\mathrm{\textbf{val}}(\mathrm{\textbf{sig}}^2\,x),\ldots).$$ En general, el conjunto portador de la coálgebra terminal de un funtor $T$ se puede obtener a partir de los comportamientos observables.
     La técnica para definir una función $f:X\rightarrow A$ por terminalidad es la siguiente: se describen las observaciones directas junto con las pasos siguientes solos de $f$ como una estructura coalgebraica sobre $X$. La función $f$ entonces surge por repetición. De aquí, una definición coinductiva de $f$ no determina a $f$ en una sola vez, sino pasa a paso. Veamos esto con unos ejemplos.
     Para nuestro funtor $A\times(-)$ sea $A=\mathbb{N}$. Definamos por coinducción la función $\mathrm{\textbf{desde}}:\mathbb{N}\rightarrow\mathbb{N}^\mathbb{N}$, la cual manda un número natural $n\in\mathbb{N}$ a la sucesión $(n,n+1,n+2,n+3,\ldots)\in\mathbb{N}^\mathbb{N}$. Esto implica definir una estructura coalgebraica $\mathbb{N}\rightarrow\mathbb{N}\times\mathbb{N}$ sobre $\mathbb{N}$. La observación directa que podemos hacer acerca del “estado” $n\in\mathbb{N}$ es $n$ mismo y el estado siguiente es $n+1$ (acerca del cual podemos observar directamente $n+1$). La repetición entonces nos lleva a $\mathrm{\textbf{desde}}\, n$. Definimos entonces por terminalidad a $\mathrm{\textbf{desde}}$ en el siguiente diagrama: $$\begin{xy} \xymatrix{ \mathbb{N}\ar[rr]^{\mathrm{\textbf{desde}}}\ar[d]_{\lambda n.(n,n+1)} & & \mathbb{N}^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})}\\ \mathbb{N}\times\mathbb{N}\ar[rr]_{1\times\mathrm{\textbf{desde}}} & & \mathbb{N}\times\mathbb{N}^\mathbb{N}. }\end{xy}$$ Así que $\mathrm{\textbf{desde}}$ queda determinada por las ecuaciones coinductivas $$\mathrm{\textbf{cab}}(\mathrm{\textbf{desde}}\, n)=n\quad\text{y}\quad\mathrm{\textbf{cola}}(\mathrm{\textbf{desde}}\, n)=\mathrm{\textbf{desde}}(n+1).$$      Definamos otras tres funciones, dos por coinducción. Nuevamente, consideremos el funtor $A\times(-)$. Definamos por terminalidad y, en consecuencia, por coinducción la función $\mathrm{\textbf{non}}:A^\mathbb{N}\rightarrow A^\mathbb{N}$ que, dada una lista infinita, devuelve la lista que resulta de tomar sólo los elementos en las entradas impares de la lista original; dotemos entonces a $A^\mathbb{N}$ de una estructura coalgebraica que nos dé las observaciones que queremos: $$\begin{xy} \xymatrix{ A^\mathbb{N}\ar[rr]^{\mathrm{\textbf{non}}}\ar[d]_{\lambda\sigma.(\mathrm{\textbf{cab}}\,\sigma,\mathrm{\textbf{cola}}(\mathrm{\textbf{cola}}\,\sigma))} & & A^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})}\\ A\times A^\mathbb{N}\ar[rr]_{1\times\mathrm{\textbf{non}}} & & A\times A^\mathbb{N} }\end{xy}$$ La estructura coalgebraica sobre $A^\mathbb{N}$ a la izquierda da lugar, por terminalidad, a un único homomorfismo de coálgebras. Por conmutatividad, $\mathrm{\textbf{non}}$ queda determinada por las ecuaciones coinductivas $$\mathrm{\textbf{cab}}(\mathrm{\textbf{non}}\,\sigma)=\mathrm{\textbf{cab}}\,\sigma\quad\text{y}\quad\mathrm{\textbf{cola}}(\mathrm{\textbf{non}}\,\sigma)=\mathrm{\textbf{non}}(\mathrm{\textbf{cola}}(\mathrm{\textbf{cola}}\,\sigma)).$$ Ahora, definimos $\mathrm{\textbf{par}}:=\mathrm{\textbf{non}}\circ\mathrm{\textbf{cola}}$, que es la función que, dada una lista infinita, nos devuelve una lista que resulta de tomar sólo los elementos en las entradas pares de la lista original.
     Finalmente, definamos por terminalidad y, en consecuencia, por coinducción la función $\mathrm{\textbf{fus}}:A^\mathbb{N}\times A^\mathbb{N}\rightarrow A^\mathbb{N}$ que, dada dos listas infinitas $\sigma$ y $\tau$, nos devuelve una lista que resulta de tomar elementos de $\sigma$ y $\tau$ alternadamente, empezando por $\sigma$; dotemos entonces a $A^\mathbb{N}\times A^\mathbb{N}$ de una estructura coalgebraica que nos dé las observaciones que queremos: $$\begin{xy} \xymatrix{ A^\mathbb{N}\times A^\mathbb{N}\ar[rr]^{\mathrm{\textbf{fus}}}\ar[d]_{\lambda(\sigma,\tau).(\mathrm{\textbf{cab}}\,\sigma,(\tau,\mathrm{\textbf{cola}}\,\sigma))} & & A^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})}\\ A\times(A^\mathbb{N}\times A^\mathbb{N})\ar[rr]_{1\times\mathrm{\textbf{fus}}} & & A\times A^\mathbb{N}. }\end{xy}$$ El homomorfismo $\mathrm{\textbf{fus}}:A^\mathbb{N}\times A^\mathbb{N}\rightarrow A^\mathbb{N}$ queda entonces determinado por las ecuaciones coinductivas $$\mathrm{\textbf{cab}}(\mathrm{\textbf{fus}}(\sigma,\tau))=\mathrm{\textbf{cab}}\,\sigma\quad\text{y}\quad\mathrm{\textbf{cola}}(\mathrm{\textbf{fus}}(\sigma,\tau))=\mathrm{\textbf{fus}}(\tau,\mathrm{\textbf{cola}}\,\sigma).$$      Lo que podemos ver de nuestras tres definiciones por coinducción es (1) que definir por terminalidad a una función es dotar a su dominio de una estructura coalgebraica apropiada que nos da la existencia de la función a definir, el diagrama conmutativo nos da las ecuaciones coinductivas que determinan a la función; recíprocamente, las ecuaciones coninductivas que definen a una función nos dan la estructura coalgebraica apropiada del dominio de la función para obtener su existencia mediante la terminalidad, y (2) que la función que queremos definir ocurre “dentro” de los observadores (o destructores) de la coálgebra terminal.
     En resumen, en una definición inductiva de una función $f$, uno define los valores de $f$ al hacerlo en todos los constructores de un álgebra inicial y en una definición coinducitva de $f$ uno define los valores de todos los observadores en cada resultado $fx$.
     Retomando la cóalgebra final del funtor $A\times(-)$ y los homomorfismos de coálgebras $\mathrm{\textbf{fus}},\mathrm{\textbf{non}}$ y $\mathrm{\textbf{par}}$, demostremos por coinducción que $$\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}\,\sigma,\mathrm{\textbf{par}}\,\sigma)=\sigma;$$ es decir, hagamos uso de la unicidad dada por la terminalidad. Basta mostrar entonces que $\mathrm{\textbf{fus}}\circ(\mathrm{\textbf{non}},\mathrm{\textbf{par}}):A^\mathbb{N}\rightarrow A^\mathbb{N}$ es un homomorfismo de coálgebras $(A^\mathbb{N},(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}}))\rightarrow(A^\mathbb{N},(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}}))$; para esto, basta mostrar que $(\mathrm{\textbf{non}},\mathrm{\textbf{par}})$ es un homomorfismo de coálgebras. Notemos que la estructura coalgebraica sobre $A^\mathbb{N}\times A^\mathbb{N}$ la podemos reescribir como $(\mathrm{\textbf{cab}}\circ p_1,\mathrm{\textbf{int}})$, donde $p_1$ es la proyección izquierda de $A^\mathbb{N}\times A^\mathbb{N}$ e $\mathrm{\textbf{int}}(\sigma,\tau):=(\tau,\mathrm{\textbf{cola}}\,\sigma)$. El siguiente diagrama conmuta: $$\begin{xy} \xymatrix{ A^\mathbb{N}\ar[rr]^{(\mathrm{\textbf{non}},\mathrm{\textbf{par}})}\ar[d]_{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})} & & A^\mathbb{N}\times A^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}}\circ p_1,\mathrm{\textbf{int}})}\\ A\times A^\mathbb{N}\ar[rr]_(.42){1\times(\mathrm{\textbf{non}},\mathrm{\textbf{par}})} & & A\times(A^\mathbb{N}\times A^\mathbb{N}), }\end{xy}$$ pues $\mathrm{\textbf{non}}\circ\mathrm{\textbf{cola}}=\mathrm{\textbf{par}}$ y $\mathrm{\textbf{cola}}\circ\mathrm{\textbf{non}}=\mathrm{\textbf{non}}\circ\mathrm{\textbf{cola}}\circ\mathrm{\textbf{cola}}$.
     El principio de coinducción como principio de demostración puede formularse de otra manera, mediante el concepto de bisimulación.
     Retomemos la coálgebra final del funtor $A\times(-)$. Una bisimulación sobre $A^\mathbb{N}$ es una relación $R$ sobre $A^\mathbb{N}$ tal que $$R(\sigma,\tau)\Rightarrow \begin{cases} \mathrm{\textbf{cab}}\,\sigma=\mathrm{\textbf{cab}}\,\tau\,\text{ y}\\ R(\mathrm{\textbf{cola}}\,\sigma,\mathrm{\textbf{cola}}\,\tau). \end{cases} $$ Ahora, $A^\mathbb{N}$ cumple el principio coinductivo de demostración: para todo $\sigma,\tau\in A^\mathbb{N}$, $$\text{si }R(\sigma,\tau)\text{ para alguna bisimulación }R\text{ sobre }A^\mathbb{N},\text{ entonces }\sigma=\tau.$$ Demostremos, otra vez, que $\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}\,\sigma,\mathrm{\textbf{par}}\,\sigma)=\sigma$. Definamos la relación $$R:=\{(\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}(\sigma),\mathrm{\textbf{par}}(\sigma)),\sigma)\mid\sigma\in A^\mathbb{N}\}$$ sobre $A^\mathbb{N}$. Se tiene que $R$ es una bisimulación, pues $$\mathrm{\textbf{cab}}(\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}\,\sigma,\mathrm{\textbf{par}}\,\sigma))=\mathrm{\textbf{cab}}\,\sigma$$ y $$\mathrm{\textbf{cola}}(\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}\,\sigma,\mathrm{\textbf{par}}\,\sigma))=\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}(\mathrm{\textbf{cola}}\,\sigma),\mathrm{\textbf{par}}(\mathrm{\textbf{cola}}\,\sigma)),$$ y esto último nos dice que $R(\mathrm{\textbf{cola}}(\mathrm{\textbf{fus}}(\mathrm{\textbf{non}}\,\sigma,\mathrm{\textbf{par}}\,\sigma)),\mathrm{\textbf{cola}}\,\sigma)$, así que, por el principio coinductivo de demostración basado en una bisimulación, se obtiene la igualdad.
     El principio funciona por lo siguiente. Dado un funtor $T:\mathbf{Con}\rightarrow\mathbf{Con}$, una bisimulación sobre la $T$-coálgebra $(X,\chi)$ es una relación $R$ sobre $X$ para la que existe una estructura $T$-coalgebraica $\gamma:R\rightarrow TR$ tal que las proyecciones $\pi_1:R\rightarrow X$, $\pi_2:R\rightarrow X$ son homomorfismos de $T$-coálgebras. Si $(X,\chi)$ es la coálgebra final de la categoría de $T$-coálgebras, entonces $\pi_1=\pi_2$.
     En el caso anterior, una relación $R$ es una bisimulación si y sólo si el siguiente diagrama conmuta: $$\begin{xy} \xymatrix{ A^\mathbb{N}\ar[d]_{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})} & R\ar[r]^{\pi_2}\ar[l]_(.45){\pi_1}\ar[d]^{(\mathrm{\textbf{val}},\mathrm{\textbf{sig}})} & A^\mathbb{N}\ar[d]^{(\mathrm{\textbf{cab}},\mathrm{\textbf{cola}})}\\ A\times A^\mathbb{N} & A\times R\ar[r]_{1\times\pi_2}\ar[l]^(.45){1\times\pi_1} & A\times A^\mathbb{N} }\end{xy}$$ si y sólo si $\mathrm{\textbf{cab}}\,\sigma=\mathrm{\textbf{val}}(\sigma,\tau)=\mathrm{\textbf{cab}}\,\tau$ con $\mathrm{\textbf{cola}}\,\sigma=\pi_1\,\mathrm{\textbf{sig}}(\sigma,\tau)$ y $\mathrm{\textbf{cola}}\,\tau=\pi_2\,\mathrm{\textbf{sig}}(\sigma,\tau)$, es decir, $R(\mathrm{\textbf{cola}}\,\sigma,\mathrm{\textbf{cola}}\,\tau)$.

Referencias