Inducció estructural

La inducció estructurada és un método de demostració utilisat en llògica matemàtica, teoria dels grafos, computació i atres àrees. Es tracta d'una generalisació de l'inducció matemàtica.

Donat un conjunt $C$ en un orde parcial ben fonamentat $<$ sobre els seus elements, la prova d'una propietat $P(x)$ per a tot element $x$ de $C$ es realisa per inducció estructural basant-se en la següent regla d'inferència:

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

La prova per inducció estructural consistix en demostrar que una proposició es complix per a tots els elements mínims del tipo, i que si la propietat es complix per a totes les subestructura d'una certa estructura S, llavors es deu complir també per a S. Per eixemple, si l'estructura és una llista, normalment s'introduïx l'orde parcial '<' tal que L < M sempre que existixca x tal que x::L=M Baixe este orde, la llista buida [] és l'únic element mínim. Aixina, una prova per inducció estructural d'una proposició P(l) consta de dos parts: Una prova de P([]) i una prova de P(L) implica P(x::L).

Eixemple

Siga (EQ) la següent propietat sobre llistes:

    llongitut (L ++ M) = llongitut L + llongitut M  (EQ)

a on ++ denota l'operació de concatenació de llistes.

Per a demostrar esta propietat, fa falta conéixer les definicions de les operacions llongitut i concatenar.

    llongitut []     = 0                (long1)
    llongitut (h:t)  = 1 + llongitut t   (long2)

    [] ++ list = list                 (concat1)
    (h::t) ++ list = h :: (t ++ list) (concat2)

La proposició P(l) en este eixemple és que EQ és verdader qualsevol siga la llistaL com a valor del l. Es deu demostrar P(l) qualsevol siga la llista i per a això s'utilisa inducció estructural sobre llistes.

Primer es demostra P([]), és dir EQ és cert per a qualsevol llistaM quan L és [].

    llongitut ([]++ M) =      { concat1 }
    llongitut M  =            { long1, aritmètica }
    llongitut [] + llongitut M

Ara es demostra P(l) quan l és una llista no buida. Com a l és no buida, deu ser de la forma x::xs per a un element x i una llista xs. L'hipòtesis inductiva diu en este cas que EQ es complix per a tot valor de M quan L és xs:

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

Ara es deu demostrar que EQ es complix també per a tot valor de M quan L és x::xs:

    llongitut ((x:xs)++ M)  =       { concat2 }
    llongitut (x:(xs ++ M)) =       { long2 }
    1 + llongitut (xs ++ M) =       { hip. }
    1 + llongitut xs + llongitut M = { long2 }
    llongitut (x:xs) + llongitut M

Orde ben fonamentat

De la mateixa manera que en l'inducció en els naturals, l'inducció estructural es basa en l'orde ben fonamentat sobre el conjunt en a on s'aplica. Si el conjunt de tots els valors d'un cert tipo admeten un orde parcial ben fonamentat, llavors tot subconjunt no buit deu tindre un element mínim (per la definició d'orde parcial ben fonamentat).

Eixemple de que es pot tindre conjunts sense element minimo

Si existixen contraeixemples a una teorema que es desija demostrar deu existir un contraeixemple mínim. Si es pot demostrar que l'existència d'un contraeixemple mínim implica l'existència d'un contraeixemple encara més chicotet s'aplega a una contradicció per lo que el conjunt de contraeixemples deu ser buit.

Eixemple

Es pot considerar el conjunt dels arbres binarios. Es pot demostrar que el número de fulls en un arbre binario complet és el número de nodos interiors més un. Supongam que existix un contraeixemple; llavors deu existir un contraeixemple en el mínim número de nodos possible. En este contraeixemple, el número de nodos interns diferix del número de fulls més un, pero no pot ser l'arbre més menut, ya que este complix en la propietat. Llavors, el contraeixemple mínim té a lo manco un full que el seu ancestro és un nodo intern. En reemplaçar eixe nodo intern pel germà del full en el contraeixemple mínim s'obté un arbre més chicotet que també és un contraeixemple, lo que representa una contradicció. L'orde parcial utilisat és S < T si S té menys nodos que T.

Vore també

• Tipo de senyes algebraic