Inducción y coinducción

Avanzado · Actualizado el 16 de agosto de 2026

Este apéndice repasa las técnicas de demostración por inducción que se usan en las pruebas de corrección de todo lo anterior, motiva después la necesidad de la coinducción y formula el principio general que se deriva del teorema de Tarski del apéndice «A». La coinducción es la herramienta que falta para razonar sobre programas que no terminan, caso muy frecuente en ingeniería inversa: servidores, bucles de eventos, controladores.

B.1 Demostración por inducción

Inducción matemática. El principio más conocido. Para demostrar que una propiedad Q(n) se cumple para todo natural n, se establece

   Q(0)          y          para todo n: Q(n) => Q(n+1)

y se concluye ∀n : Q(n). Formalmente, su corrección se apoya en que todo número natural es o bien 0 o bien el sucesor n+1 de otro: el principio de demostración refleja la forma en que los naturales se construyen.

Inducción estructural. Permite hacer inducción sobre el tamaño de cualquier estructura para la que pueda definirse una noción de tamaño, es decir, una aplicación de la estructura en los naturales. Considérese un tipo de datos algebraico

d in D
d ::= Base | Con1(d) | Con2(d, d)

donde Base es un caso base, Con₁ un constructor unario y Con₂ uno binario. Puede definirse la medida

size(Base)        = 0
size(Con1(d))     = 1 + size(d)
size(Con2(d1,d2)) = 1 + size(d1) + size(d2)

y proceder por inducción matemática sobre size(d). Alternativamente, la inducción matemática puede ocultarse dentro de un principio de inducción estructural: para demostrar ∀d : Q(d) basta establecer

   Q(Base)
   para todo d:      Q(d) => Q(Con1(d))
   para todos d1,d2: Q(d1) and Q(d2) => Q(Con2(d1,d2))

Una vez más, el principio de demostración refleja la forma en que los datos se construyen.

Inducción sobre la forma. Supóngase ahora que Base representa el 0, que Con₁(d) representa d + 1 y que Con₂(d₁, d₂) representa d₁ + d₂. Puede definirse una semántica natural d ⇒ n para evaluar d al número n que representa:

[base]  ------------
        Base => 0

              d => n
[con1]  ----------------
        Con1(d) => n+1

        d1 => n1     d2 => n2
[con2]  -----------------------
        Con2(d1,d2) => n1 + n2

Esto define una noción de árboles de derivación: hay un caso base y dos casos inductivos. Se puede hacer inducción sobre el tamaño de los árboles de derivación, pero suele ser más cómodo ocultarla dentro de un principio de inducción sobre la forma de los árboles de inferencia:

   Q(Base => 0)

   para todo (d => n):  Q(d => n) => Q( Con1(d) => n+1 )

   para todos (d1 => n1), (d2 => n2):
        Q(d1 => n1) and Q(d2 => n2) => Q( Con2(d1,d2) => n1+n2 )

de donde se concluye ∀(d ⇒ n) : Q(d ⇒ n). Como cabía esperar, el principio de demostración refleja la forma en que se construyen los árboles de evaluación.

Éste es el principio que se usa en las demostraciones de corrección semántica del capítulo «20», y es la razón de que en aquel capítulo la corrección se demuestre «por inducción sobre la derivación».

Inducción por curso de valores. Todos los principios anteriores son constructivos, en el sentido de que establecen un predicado para los casos base y luego lo mantienen en todos los constructores. Una variante los reúne en un solo paso:

   para todo n:  ( para todo m < n: Q(m) )  =>  Q(n)

de donde se concluye ∀n : Q(n). Aquí el caso base está incluido en el mismo paso que el inductivo: cuando n = 0 la hipótesis es vacíamente cierta.

Formalización

Inducción bien fundada

La generalización de todo lo anterior. Dado un conjunto parcialmente ordenado (D, ≼), se dice que ≼ es un orden bien fundado (well-founded ordering) si no existe ninguna sucesión decreciente infinita

d₁ ≻ d₂ ≻ d₃ ≻ …

donde d ≻ d' significa d' ≼ d ∧ d ≠ d'. Esto es exactamente la condición de cadena descendente del apéndice «A».

El principio de inducción bien fundada dice entonces:

( ∀d : (∀d' ≺ d : Q(d')) ⟹ Q(d) ) ⟹ ∀d : Q(d)

Todos los principios de esta sección son casos particulares: la inducción matemática toma (ℕ, ≤); la estructural, el orden inducido por size; la inducción sobre la forma, el orden de subárbol.

Y obsérvese la conexión con el capítulo «5»: la DCC es lo que hace legítima la inducción, y la ACC es lo que hace terminar la iteración de punto fijo. Son la misma condición aplicada en direcciones opuestas.

B.2 Por qué hace falta la coinducción

Considérese un programa de la forma

if f(27, m) then "algo bueno" else "algo malo"

donde f toma parejas de naturales y devuelve valores de verdad. Queremos garantizar que el programa nunca ejecuta «algo malo». Como el valor de m no se conoce, no es factible demostrar que f(27, m) ≠ false evaluándolo; hace falta una demostración. Definamos, pues, el predicado

Q_f(n) ⟺ ∀m : f(n, m) ≠ false

Consideremos cuatro funciones definidas por recursión:

f0(0, m)   = true          f1(0, m)   = f1(0, m)
f0(n+1, m) = f0(n, m)      f1(n+1, m) = f1(n, m)

f2(0, m)   = true          f3(0, m)   = f3(0, m)
f2(n+1, m) = f2(n+1, m)    f3(n+1, m) = f3(n+1, m)

Para f₀, la inducción matemática funciona sin problema: se demuestra Q_f₀(0) y ∀n : Q_f₀(n) ⟹ Q_f₀(n+1), y se concluye ∀n : Q_f₀(n).

Pero f₁, f₂ y f₃ nunca terminan. ¿Deberían considerarse aceptables? Intuitivamente sí: nunca ejecutan «algo malo», simplemente porque nunca ejecutan nada. Sin embargo no se puede establecer el caso base —para f₁ y f₃— ni el paso inductivo —para f₂ y f₃—.

El argumento intuitivo de por qué son aceptables es el siguiente: todas las ocurrencias de fᵢ en las partes derechas de las definiciones satisfacen Qᵢ; luego se sigue que las fᵢ de las partes izquierdas también lo hacen. Suena peligrosamente circular: se supone el resultado que se quiere demostrar. Pero con la definición apropiada es un argumento válido, y ese argumento es la coinducción.

Obtención de un funcional. Reescribamos las cláusulas de forma que Qᵢ aparezca a la izquierda y las definiciones de fᵢ a la derecha:

Q0(0)   si true             Q1(0)   si Q1(0)
Q0(n+1) si Q0(n)            Q1(n+1) si Q1(n)

Q2(0)   si true             Q3(0)   si Q3(0)
Q2(n+1) si Q2(n+1)          Q3(n+1) si Q3(n+1)

Cada uno de estos sistemas puede leerse como una ecuación

Q_i = 𝒬_i(Q_i)

donde 𝒬ᵢ es un funcional: una función que toma un predicado y devuelve un predicado. Y 𝒬ᵢ es monótono sobre el retículo completo

( ℕ → \{true, false\}, ⊑ )

de predicados, con Q₁ ⊑ Q₂ si ∀n : Q₁(n) ⟹ Q₂(n), elemento mínimo ⊥ = λn. false y máximo ⊤ = λn. true. Por el teorema de Tarski del apéndice «A», cada 𝒬ᵢ tiene un menor punto fijo lfp(𝒬ᵢ) y un mayor punto fijo gfp(𝒬ᵢ), en general distintos.

Formalización

Los cuatro casos, calculados

Menor punto fijo. Del apéndice «A» se sigue ⊔ₖ 𝒬ᵢᵏ(⊥) ⊑ lfp(𝒬ᵢ), y como las cláusulas usan un número finito de Q en cada parte derecha, la continuidad da la igualdad:

⊔_k 𝒬_i^k(⊥) = lfp(𝒬_i)

Esto justifica la intuición anterior: el predicado ⊔ₖ 𝒬ᵢᵏ(⊥) se cumple en n si y sólo si hay a lo sumo k axiomas y reglas que demuestran Qᵢ(n). Es decir, una demostración por inducción se corresponde con el menor punto fijo.

Ahora bien, para 𝒬₃ se tiene lfp(𝒬₃) = ⊥, porque 𝒬₃(⊥) = ⊥. Eso explica por qué lfp(𝒬₃)(27) = false y por qué ninguna demostración inductiva sirve para establecer Q₃(27). Lo mismo ocurre, en variantes, con 𝒬₁ y 𝒬₂.

Mayor punto fijo. En cambio, gfp(𝒬₃) = ⊤, porque 𝒬₃(⊤) = ⊤. Y gfp(𝒬₃)(27) = true proporciona el fundamento formal de nuestra creencia de que f₃ no hará ningún daño en el ejemplo. Argumentos análogos valen para 𝒬₁ y 𝒬₂.

Y para 𝒬₀ los dos coinciden: lfp(𝒬₀) = gfp(𝒬₀), porque la inducción matemática sobre n basta para demostrar lfp(𝒬₀)(n) = gfp(𝒬₀)(n). No es sorprendente: f₀ termina. Que los dos puntos fijos coincidan es precisamente lo que distingue a 𝒬₀ de los otros tres.

La razón técnica de fondo se relaciona con el teorema del punto fijo de Banach: una función contractiva sobre un espacio métrico completo tiene un punto fijo único. La contractividad de 𝒬₀, frente a la de 𝒬₁, 𝒬₂ y 𝒬₃, se sigue de que la cláusula de 𝒬₀(n) sólo hace llamadas a Q con argumentos estrictamente menores que n. Que es, de nuevo, la condición de buena fundación.

B.3 El principio de coinducción

Con el aparato del apéndice «A», el principio se enuncia y se demuestra en dos líneas.

Formalización

Inducción y coinducción como principios duales

Sea L un retículo completo y F : L → L monótona.

Principio de inducción. Para demostrar lfp(F) ⊑ Q, basta encontrar Q con

F(Q) ⊑ Q

es decir, basta que Q ∈ Red(F). En efecto, lfp(F) = ⊓Red(F) ⊑ Q.

Principio de coinducción. Para demostrar Q ⊑ gfp(F), basta encontrar Q con

Q ⊑ F(Q)

es decir, basta que Q ∈ Ext(F). En efecto, Q ⊑ ⊔Ext(F) = gfp(F).

A un Q que cumple Q ⊑ F(Q) se le llama F-consistente, o post-punto-fijo. El principio de coinducción dice, pues: para demostrar que algo está por debajo del mayor punto fijo, basta exhibir un testigo consistente que lo contenga.

Y ahí está formalizada la «circularidad» que parecía sospechosa en la «sección B.2 · Por qué hace falta la coinducción»: no se supone lo que se quiere demostrar, se exhibe un conjunto cerrado bajo la regla y se apela a la maximalidad del mayor punto fijo.

La asimetría de uso entre ambos principios es la siguiente:

	Inducción	Coinducción
Punto fijo	menor, `lfp(F)`	mayor, `gfp(F)`
Condición sobre el testigo	`F(Q) ⊑ Q`	`Q ⊑ F(Q)`
Qué se demuestra	`lfp(F) ⊑ Q`	`Q ⊑ gfp(F)`
Datos que modela	finitos, bien fundados	infinitos, circulares
Condición de cadena asociada	DCC	ACC
Ejemplos	árboles de derivación, terminación	trazas infinitas, bisimulación

B.4 Dónde aparece esto

En las demostraciones de corrección. Todas las pruebas de los capítulos «5», «6», «7», «8», «20» y «21» —terminación del punto fijo, corrección local, transferencia del punto fijo, corrección semántica de los sistemas de tipos y efectos— son inducciones, sobre la estructura de la sintaxis, sobre la derivación, o sobre el número de iteraciones.

En la elección de menor o mayor punto fijo. El capítulo «5» estableció que el resultado del análisis es el menor punto fijo, con el argumento de que es el más preciso. Ese argumento vale para los análisis may, donde ⊥ significa «nada ocurre». Para los análisis must el retículo está invertido, y el «menor punto fijo respecto de ⊑» es el mayor respecto de ⊆: de ahí el nombre MFP —Maximal Fixed Point— del capítulo «7», que tanta confusión causa. Este apéndice explica por qué la elección no es arbitraria: depende de si la propiedad que se analiza es un dato bien fundado o un dato circular.

En la semántica de trazas. El capítulo «21» mencionó que la semántica colectora es a su vez abstracción de una semántica de trazas. Las trazas de un programa que no termina son infinitas, y su conjunto se define como mayor punto fijo, no como menor. Razonar sobre ellas es razonar por coinducción.

En ingeniería inversa

Programas que no terminan

El caso f₃ de la «sección B.2 · Por qué hace falta la coinducción» —el programa que no hace nada malo porque no hace nada— parece un artificio académico. En ingeniería inversa es el caso normal.

Un servidor, un controlador de dispositivo, un bucle de eventos de una interfaz gráfica, un bootloader, el bucle principal de un intérprete embebido: ninguno termina, y todos son objetivos habituales de análisis. Las preguntas interesantes sobre ellos son coinductivas:

«¿puede este bucle de eventos llegar alguna vez a un estado en que ignore la entrada?» — propiedad de viveza sobre trazas infinitas;
«¿mantiene este controlador siempre el invariante de que el descriptor está abierto?» — propiedad de seguridad sobre trazas infinitas, demostrable exhibiendo un invariante consistente, que es exactamente un testigo F-consistente;
«¿son estas dos versiones del binario equivalentes?» — bisimulación, la relación coinductiva por excelencia.

Ninguna de las tres se responde con un análisis de flujo de datos ordinario, y saber que el objeto matemático correcto es el mayor punto fijo y no el menor evita perder tiempo buscando la demostración inductiva que no existe.

Nótese además que lo que aquí se trata es, en toda su extensión, análisis de propiedades de seguridad (safety): «nunca ocurre algo malo». Las propiedades de viveza (liveness) —«acabará ocurriendo algo bueno»— quedan fuera, y es una restricción deliberada que ya se anunció en el capítulo «2». Su tratamiento requiere el aparato de la verificación de modelos y de las lógicas temporales, que es otra disciplina.

B.5 Notas

Para el tratamiento de propiedades de viveza y de las lógicas temporales, la referencia estándar es la literatura de verificación de modelos.