Inducción estructural

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 en otras áreas. Se trata de una generalización de la inducción matemática.

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

\frac{\forall x:x\in C:(\forall y:y<x: P(y))\Rightarrow P(x)}{\forall x:x\in C:P(x)}

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

Orden bien fundamentado

Al igual que con la inducción en los naturales, la inducción estructural se basa en el orden bien fundamentado sobre el conjunto en donde se aplica. Si el conjunto de todos los valores de un cierto tipo admiten un orden parcial bien fundamentado, entonces todo subconjunto no vacío debe tener un elemento mínimo (por la definición de orden parcial bien fundamentado). Por tanto, si existen contraejemplos a un teorema que se desea demostrar debe existir un contraejemplo mínimo. Si se puede demostrar que la existencia de un contraejemplo mínimo implica la existencia de un contraejemplo aun más pequeño se llega a una contradicción por lo que el conjunto de contraejemplos debe ser vacío.

Como ejemplo de este argumento, se puede considerar el conjunto de los árboles binarios. Se puede demostrar que el número de hojas en un árbol binario completo es el número de nodos interiores más uno. Supongamos que existe un contraejemplo; entonces debe existir un contraejemplo con el mínimo número de nodos posible. En este contraejemplo, el número de nodos internos difiere del número de hojas más uno, pero no puede ser el árbol más pequeño, dado que éste cumple con la propiedad. Entonces, el contraejemplo mínimo tiene al menos una hoja cuyo ancestro es un nodo interno. Al remplazar ese nodo interno por el hermano de la hoja en el contraejemplo mínimo se obtiene un árbol más pequeño que también es un contraejemplo, lo que representa una contradicción. El orden parcial utilizado es S < T si S tiene menos nodos que T.

Véase también


Wikimedia foundation. 2010.

См. также в других словарях:

  • 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 en otras áreas. Se trata de una generalización de la inducción matemática. Dado un conjunto con un orden parcial bien… …   Enciclopedia Universal

  • Método formal — En ingeniería de software un método formal es un camino a la construcción y análisis de modelos matemáticos que permitan una automatización del desarrollo de sistemas informáticos. Los métodos formales se caracterizan por emplear técnicas y… …   Wikipedia Español

  • Tipo de datos algebraico — Saltar a navegación, búsqueda En matemáticas discretas es usual introducir definiciones de estructuras recursivas dando los casos de definición y un axioma de clausura indicando que ninguna otra cosa forma parte de lo definido. Por ejemplo, los… …   Wikipedia Español

  • Tipo de dato algebraico — En matemáticas discretas es usual introducir definiciones de estructuras recursivas dando los casos de definición y un axioma de clausura indicando que ninguna otra cosa forma parte de lo definido. Por ejemplo, los árboles con información en los… …   Wikipedia Español

  • Demostrador de teoremas Isabelle — Saltar a navegación, búsqueda El demostrador interactivo de teoremas Isabelle es una herramienta de ayuda a la demostración de teoremas escrita en el lenguaje de programación ML y desarrollada por Larry Paulson de la Universidad de Cambridge y… …   Wikipedia Español

  • Isabelle — El demostrador interactivo de teoremas Isabelle es una herramienta de ayuda a la demostración de teoremas escrita en el lenguaje de programación ML y desarrollada por Larry Paulson de la Universidad de Cambridge y Tobias Nipkow del Technische… …   Wikipedia Español

  • Enzima — Estructura de la triosafosfato isomerasa. Conformación en forma de diagrama de cintas rodeado por el modelo de relleno de espacio de la proteína. Esta proteína es una ef …   Wikipedia Español

  • Leucemia mieloide aguda — Células leucémicas …   Wikipedia Español

  • Claude Lévi-Strauss — Lévi Strauss (2005) Nacimiento 28 de noviembre de 1908 Bruselas (Bélgica) …   Wikipedia Español

  • Farmacocinética — Saltar a navegación, búsqueda …   Wikipedia Español


Поделиться ссылкой на выделенное

Прямая ссылка:
Нажмите правой клавишей мыши и выберите «Копировать ссылку»