¿Qué es la coinducción?

He oído hablar de inducción (estructural). Le permite construir estructuras finitas a partir de otras más pequeñas y le ofrece principios de prueba para razonar sobre tales estructuras. La idea es lo suficientemente clara.

¿Pero qué pasa con la coinducción? ¿Como funciona? ¿Cómo se puede decir algo concluyente sobre una estructura infinita?

Hay (al menos) dos ángulos para abordar, a saber, la coinducción como una forma de definir las cosas y como una técnica de prueba.

Con respecto a la coinducción como una técnica de prueba, ¿cuál es la relación entre la coinducción y la bisimulación?

Primero, para disipar una posible disonancia cognitiva: el razonamiento sobre estructuras infinitas no es un problema, lo hacemos todo el tiempo. Mientras la estructura sea finitamente describible, eso no es un problema. Aquí hay algunos tipos comunes de estructuras infinitas:

• idiomas (conjuntos de cadenas sobre algún alfabeto, que pueden ser finitos);
• lenguajes de árboles (conjuntos de árboles sobre algún alfabeto);
• rastros de ejecución de un sistema no determinista;
• numeros reales;
• conjuntos de enteros;
• conjuntos de funciones de enteros a enteros; ...

Coinductividad como el punto de fijación más grande

Donde las definiciones inductivas construyen una estructura a partir de bloques de construcción elementales, las definiciones coinductivas dan forma a las estructuras de cómo pueden ser deconstruidas. Por ejemplo, el tipo de listas cuyos elementos están en un conjunto Ase define de la siguiente manera en Coq:

Inductive list (A:Set) : Set :=
  | nil : list A
  | cons : A -> list A -> list A.

Informalmente, el listtipo es el tipo más pequeño que contiene todos los valores construidos a partir de los constructores nily cons, con el axioma que . Por el contrario, podemos definir el tipo más grande que contiene todos los valores construidos a partir de estos constructores, manteniendo el axioma de discriminación:$\forall x \, y, \: \mathtt{nil} \ne \mathtt{cons} \: x \: y$

CoInductive colist (A:Set) : Set :=
  | conil : colist A
  | cocons : A -> colist A -> colist A.

listes isomorfo a un subconjunto de colist. Además, colistcontiene infinitas listas: listas con coconssobre cocons.

CoFixpoint flipflop : colist ℕ := cocons 1 (cocons 2 flipflop).
CoFixpoint from (n:ℕ) : colist ℕ := cocons n (from (1 + n)).

flipflopes la (lista circular) infinita ; es la lista infinita de números naturales 0 : : 1 : : 2 : : ... .$1::2::1::2::\ldots$from 0$0::1::2::\ldots$

Una definición recursiva está bien formada si el resultado se construye a partir de bloques más pequeños: las llamadas recursivas deben funcionar en entradas más pequeñas. Una definición corecursive está bien formada si el resultado crea objetos más grandes. La inducción mira a los constructores, la coinducción mira a los destructores. Observe cómo la dualidad no solo cambia de menor a mayor, sino también de entradas a salidas. Por ejemplo, la razón de la flipflopy fromdefiniciones anteriores están bien formadas-es que la llamada corecursive es vigilado por una llamada al coconsconstructor en ambos casos.

Cuando las declaraciones sobre objetos inductivos tienen pruebas inductivas, las declaraciones sobre objetos coinductores tienen pruebas coinductivas. Por ejemplo, definamos el predicado infinito en colistas; intuitivamente, los colistas infinitos son los que no terminan con conil.

CoInductive Infinite A : colist A -> Prop :=
  | Inf : forall x l, Infinite l -> Infinite (cocons x l).

Para demostrar que los colistas de la forma from nson infinitos, podemos razonar por coinducción. from nes igual a cocons n (from (1 + n)). Esto muestra que from nes mayor que from (1 + n), que es infinito por la hipótesis de la coinducción, por from nlo tanto, es infinito.

Bisimilaridad, una propiedad coinductora

La coinducción como técnica de prueba también se aplica a objetos finitarios. Intuitivamente hablando, las pruebas inductivas sobre un objeto se basan en cómo se construye el objeto. Las pruebas coductivas se basan en cómo se puede descomponer el objeto.

Cuando se estudian sistemas deterministas, es común definir la equivalencia a través de reglas inductivas: dos sistemas son equivalentes si puede pasar de uno a otro mediante una serie de transformaciones. Dichas definiciones tienden a no capturar las diferentes formas en que los sistemas no deterministas pueden terminar teniendo el mismo comportamiento (observable) a pesar de tener una estructura interna diferente. (La coinducción también es útil para describir sistemas no terminales, incluso cuando son deterministas, pero esto no es en lo que me centraré aquí).

Los sistemas no deterministas como los sistemas concurrentes a menudo se modelan mediante sistemas de transición etiquetados . Un LTS es un gráfico dirigido en el que se etiquetan los bordes. Cada borde representa una posible transición del sistema. Una traza de un LTS es la secuencia de etiquetas de borde sobre una ruta en el gráfico.

Dos LTS pueden comportarse de manera idéntica, ya que tienen los mismos rastros posibles, incluso si su estructura interna es diferente. El isomorfismo gráfico es demasiado fuerte para definir su equivalencia. En cambio, se dice que un LTS simula otro LTS B si cada transición del segundo LTS admite una transición correspondiente en el primero. Formalmente, dejemos que S sea ​​la unión disjunta de los estados de los dos LTS, L el conjunto (común) de etiquetas y → la relación de transición. La relación R ⊆ S × S es una simulación si ∀ ( p , q ) ∈ $\mathscr{A}$$\mathscr{B}$$S$$L$$\rightarrow$$R \subseteq S \times S$

$$\forall (p,q)\in R, %\forall p'\in S, \forall\alpha\in L, \text{ if } p \stackrel\alpha\rightarrow p' \text{ then } \exists q', \; q \stackrel\alpha\rightarrow q' \text{ and } (p',q')\in R$$

simula B si existe una simulación en la que todos los estados de B están relacionados con un estado en A . Si R es una simulación en ambas direcciones, se llamabisimulación. La simulación es una propiedad coinductora: cualquier observación en un lado debe tener una coincidencia en el otro lado.$\mathscr{A}$$\mathscr{B}$$\mathscr{B}$$\mathscr{A}$$R$

Hay potencialmente muchas bisimulaciones en un LTS. Diferentes bisimulaciones pueden identificar diferentes estados. Dadas dos bisimulaciones y R 2 , la relación dada al tomar la unión de los gráficos de relaciones R 1 ∪ R 2 es en sí misma una bisimulación, ya que los estados relacionados dan lugar a estados relacionados para ambas relaciones. (Esto también es válido para las uniones infinitas. La relación vacía es una bisimulación sin intromisión, como lo es la relación de identidad). En particular, la unión de todas las bisimulaciones es en sí misma una bisimulación, llamada bisimilaridad. La bisimilaridad es la forma más grosera de observar un sistema que no distingue entre estados distintos.$R_1$$R_2$$R_1 \cup R_2$

La bisimilaridad es una propiedad coinductora. Se puede definir como el punto de fijación más grande de un operador: es la relación más grande que, cuando se extiende para identificar estados equivalentes, permanece igual.

Referencias

• Coq y el cálculo de construcciones inductivas

  • Yves Bertot y Pierre Castéran. Prueba interactiva de teoremas y desarrollo de programas - Coq'Art: El cálculo de las construcciones inductivas . Springer, 2004. Cap. 13. [ sitio web ] [ Amazon ]
  • Eduardo Giménez. Una aplicación de tipos co-inductivos en coq: verificación del protocolo de bits alternos . En Taller sobre tipos de pruebas y programas , número 1158 en Lecture Notes in Computer Science , páginas 135–152. Springer-Verlag, 1995. [ Google Books ]
  • Eduardo Giménez y Pierre Castéran. Un tutorial sobre [Co-] Tipos inductivos en Coq. 2007. [ PDF ]

• Sistemas de transición etiquetados y bisimulaciones

  • Robin Milner Comunicación y concurrencia . Prentice Hall, 1989.
  • Davide Sangiorgi. Sobre los orígenes de la bisimulación y la coinducción . Transacciones de ACM sobre lenguajes y sistemas de programación (TOPLAS), volumen 31, número 4, mayo de 2009. [ PDF ] [ ACM ] Diapositivas del curso asociado: [ PDF ] [ CiteSeer ]

  • Davide Sangiorgi. El cálculo pi: una teoría de procesos móviles . Cambridge University Press, 2003. [ Amazon ]

    • Más referencias sugeridas por Anton Trunov

  • Un capítulo en Programación certificada con tipos dependientes por A. Chlipala

  • D. Sangiorgi. "Introducción a la bisimulación y coinducción". 2011. [ PDF ]
  • D. Sangiorgi y J. Rutten. Temas avanzados en Bisimulación y Coinducción . Cambridge University Press, 2012. [ CUP ]

Consideremos la siguiente definición inductiva:

$\qquad \displaystyle \begin{align*} &\phantom{\Rightarrow} \quad \varepsilon \in \mathcal{T} \\ w \in \mathcal{T} \quad &\Rightarrow \quad aw \in \mathcal{T}\\ aw \in \mathcal{T} \quad &\Rightarrow \quad baw \in \mathcal{T} \end{align*}$

$\mathcal{T}$$b$

$\qquad \displaystyle \mathcal{T} =\{\varepsilon, a, aa, ba, aaa, aba, \dots\} = \mathcal{L}\left((ba\mid a)^*\right) \subseteq \Sigma^*.$

$\mathcal{T}$$\mathcal{T}=\{a,b\}^*$

$f : 2^{\Sigma^\infty} \to 2^{\Sigma^\infty}$

$\qquad f(T) = T \cup \{\varepsilon\} \cup \{aw \mid w\in T\} \cup \{baw \mid aw \in T\}$

$\mathcal{T}$$f$$f$$\left(2^{\Sigma^\infty},\subseteq\right)$$\{\varepsilon\}$$\mathcal{T}$

$w$$aw$$aw$$w$$\mathcal{T}'$$\mathcal{T}'$$\Sigma^\infty$$bb$$\mathcal{T}'=\mathcal{L}\left((ba\mid a)^\omega\right)$

$f$$\mathcal{T}'$$\mathcal{T}'$$\{\varepsilon\}$$\Sigma^\infty$

---

Notación:

• $\Sigma^\infty = \Sigma^* \cup \Sigma^\omega$
• $\Sigma^\omega$$\Sigma$

---

$w \in \mathcal{T} \Rightarrow aw \notin \mathcal{T}$
$\{\varepsilon\}$