Estudiando teoría de tipos me he cruzado con el concepto de coinducción. Es un concepto fácil y con interesantes consecuencias.
Inducción
Tanto en la inducción como en la coinducción queremos saber qué elementos de un conjunto universo U cumplen una propiedad P. Llamemos precisamente P al conjunto de elementos que cumplen P. Obviamente
[$$ P\subseteq U $$]En el caso de la inducción partimos con unos casos base B que son elementos de los que tenemos constancia directa de su propiedad P. De nuevo y obviamente
Ahora necesitamos el paso de inducción. El paso de inducción nos dice que si conocemos que ciertos elementos cumplen la propiedad, entonces otros también la cumplen. El paso clásico es
Sin embargo, generalizamos pensando que si he comprobado que los elementos de X cumplen la propiedad, entonces los elementos de F(X) también la cumplen. F(X) representa a los elementos del siguiente paso. Es decir,
[$$ X\subseteq F(X) $$]El resultado es que cada vez X se hará más y más grande... hasta encontrar un punto fijo (por el teorema de Kleene es el mínimo punto fijo)
[$$ X=F(X)=\mu F $$]En ese momento P=X.
Nota adicional: Si hacemos que
[$$ F(\emptyset )=B $$]Se captura también la idea de caso base en el formalismo de F (llamada función generadora). Una restricción para esta F es que debe ser monótona.
[$$ U\subseteq V \rightarrow F(U)\subseteq F(V) $$]Esto es lógico porque si hemos probado que un elemento x cumple la propiedad P(x) está claro que debe seguir cumpliéndola conforme avancemos en la demostración.
Coinducción
Algunas propiedades no se pueden demostrar por inducción. Sólo podremos demostrar por inducción aquellas en las que exista una función generadora F cuyo mínimo punto fijo sea P. Como ya hemos escrito,
[$$ \mu F=P $$]Sin embargo, tenemos otro punto fijo que es el máximo punto fijo. En este punto fijo, empezamos por asumir que todos los elementos de U cumplen la propiedad y luego, con la F, vamos quitándolos. Eso es la coinducción.
Partimos de unos casos bases de los que estamos seguros que fuera de ellos no se cumple P. Luego vamos refinando esos casos quitando poco a poco, usando F otra vez, hasta llegar al máximo punto fijo.
[$$ \nu F=F(X)=X=P $$]Todo esto está muy bien, ¿pero para qué sirve?
Principalmente para nada si ambos puntos fijos son el mismo, pero si no son el mismo obtenemos propiedades distintas ya usemos la inducción o la coinducción.
Aplicación a los subtipos recursivos
Supongamos que tenemos una lista definida de la manera usual en tipos algebráicos paramétricos.
Lista(X) = vacía | par X Lista(X)
Es decir, una lista es o bien la lista vacía o bien un par de un elemento del contenido de la lista (tipo X) con el resto de la lista.
Ahora tendremos dos tipos, los enteros y los reales. Está claro que un entero es un subtipo de un real de sólo lectura ( Entero <: Real ), pero ¿es una lista de enteros una lista de reales? ( Lista(Entero) <: Lista(Real) ).
Vayamos por partes.
Una lista vacía es una lista vacía así que no vamos a tener problemas ahí.
Si un par X Y es subtipo de otro par S T entonces X ha de ser subtipo de S e Y de T. Es decir
[$$ par\ X\ Y\ <:\ par\ S\ T\ \ \leftrightarrow\ \ X<:S\ \ \wedge\ \ Y<:T $$]
Cuando comparamos las listas de enteros y reales los primeros términos del par son precisamente Entero y Real por lo que todo va bien. Sin embargo, en el segundo término volvemos a tener Lista(Entero) y Lista(Real) que es justo lo que queríamos comprobar.
Estamos usando tipos recursivos y es normal que esto pase.
Si usáramos inducción deberíamos decir "Como no he comprobado que Lista(Entero)<:Lista(Real) entonces lo asumo falso y concluyo que una lista de enteros no es una lista de reales".
Si usáramos coinducción deberíamos decir "Como no he comprobado que Lista(Entero)<:Lista(Real) entonces lo asumo cierto y concluyo que una lista de enteros es una lista de reales".
En los lenguajes de programación que usan tipos recursivos, el uso de la coinducción es necesario ya que de otra forma estos tipos recursivos no cumplirían ninguna propiedad.
0 comentarios:
Publicar un comentario