Inducción estructural

La inducción estructurada es un método de demostración utilizado en lógica matemática, teoría de los grafos, computación y otras áreas. Se trata de una generalización de la inducción matemática.

Dado un conjunto con un orden parcial bien fundamentado sobre sus elementos, la prueba de una propiedad para todo elemento de se realiza por inducción estructural basándose en la siguiente regla de inferencia:

La prueba por inducción estructural consiste en demostrar que una proposición se cumple para todos los elementos mínimos del tipo, y que si la propiedad se cumple para todas las subestructuras de una cierta estructura S, entonces se debe cumplir también para S. Por ejemplo, si la estructura es una lista, normalmente se introduce el orden parcial '<' tal que L < M siempre que exista x tal que x::L=M Bajo este orden, la lista vacía [] es el único elemento mínimo. Así, una prueba por inducción estructural de una proposición P(l) consta de dos partes: Una prueba de P([]) y una prueba de P(L) implica P(x::L).

Ejemplo

Sea (EQ) la siguiente propiedad sobre listas:

    longitud (L ++ M) = longitud L + longitud M  (EQ)

donde ++ denota la operación de concatenación de listas.

Para demostrar esta propiedad, hace falta conocer las definiciones de las operaciones longitud y concatenar.

    longitud []     = 0                (long1)
    longitud (h:t)  = 1 + longitud t   (long2)
    [] ++ list = list                 (concat1)
    (h::t) ++ list = h :: (t ++ list) (concat2)

La proposición P(l) en este ejemplo es que EQ es verdadero cualquiera sea la lista L como valor del l. Se debe demostrar P(l) cualquiera sea la lista y para ello se utiliza inducción estructural sobre listas.

Primero se demuestra P([]), es decir EQ es cierto para qualquier lista M cuando L es [].

    longitud ([]++ M) =      { concat1 }
    longitud M  =            { long1, aritmética }
    longitud [] + longitud M

Ahora se demuestra P(l) cuando l es una lista no vacía. Como l es no vacía, debe ser de la forma x::xs para un elemento x y una lista xs. La hipótesis inductiva dice en este caso que EQ se cumple para todo valor de M cuando L es xs:

    longitud (xs ++ M) = longitud xs + longitud M (hip.)  

Ahora se debe demostrar que EQ se cumple también para todo valor de M cuando L es x::xs:

    longitud ((x:xs)++ M)  =       { concat2 }
    longitud (x:(xs ++ M)) =       { long2 }
    1 + longitud (xs ++ M) =       { hip. }
    1 + longitud xs + longitud M = { long2 }
    longitud (x:xs) + longitud M
Other Languages