Inducción Estructural

De Cuba-Wiki

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:

Los generadores de Secuencia son:

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:

Luego, debemos probar:

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:

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