Inducción Estructural

La inducción estructural es una herramienta útil para demostrar propiedades sobre Tipos Abstractos de Datos.

Supongamos por ejemplo que queremos probar una propiedad P, para toda secuencia s:

$1)(\forall {s:secu(\alpha )})P(s)\equiv true$

Los generadores de Secuencia son:

$2)<>:~\rightarrow secu(\alpha )$

$3)\bullet ~\bullet ~\bullet :~\alpha ~\times ~secu(\alpha )~\rightarrow ~secu(\alpha )$

Para demostrar la propiedad P, debemos verificar que se cumple para todo elemento generado a partir de un generador no recursivo. En el caso del TAD Secuencia, el único generador no recursivo es 2). Por lo tanto, debemos ver que:

$4)P(<>)\equiv true$

Luego, debemos probar:

$5)(\forall {s:secu(\alpha )})(P(s)\equiv true\Rightarrow P(s')\equiv true)$

Donde s' es cualquier instancia que pueda ser generada a partir de s con cualquiera de los generadores recursivos del TAD. Para el TAD Secuencia, el único generador recursivo es 3). Entonces, la proposición anterior nos quedaría:

$6)(\forall {s:secu(\alpha )})(P(s)\equiv true\Rightarrow ((\forall {a:\alpha })P(a\bullet s)\equiv true))$

El principio de inducción nos asegura que probando 4) y 6) probamos 1).