Indução Estrutural

A indução estrutural pode ser entendida como uma generalização da indução matemática convencional.  A indução estrutural é usada para provar uma propriedade P para todos os elementos de algum objeto definido recursivamente. A indução matemática é fortemente baseada na estrutura recursiva(indutiva) dos números naturais, com a indução estrutural podemos ampliar a aplicação para outras estruturas definidas indutivamente.

Exemplo básico:

Seja S um conjunto definido da seguinte maneira:

• 3 $\in$ S.
• Se x $\in$ S e y $\in$ S então x+y $\in$ S.

Podemos provar certas propriedades do conjunto S sem precisar listar extensivamente todos os elementos, como por exemplo, x $\in$ S então x é divisível por 3.

Caso Base: 3 $\in$ S e 3 é divisível por S

Por hipótese de indução, vamos supor x é divisível por 3 e y é divisível por 3. Logo, x = 3$k_1$ e y = $k_2$ e x+y = 3($k_1+k_2$). Assim, x+y também é divisível por 3.

Considere a seguinte definição recursiva de árvore binária:

Árvores binárias.

(a) A árvore vazia é uma árvore.

(b) se T1 e T2 são árvores então T’ é um árvore.

Traduzindo para Haskell

data Arvore t = Nulo | No t (Arvore t) (Arvore t) deriving (Eq, Ord, Show)

Propriedade número de folhas

Seja A um conjunto de árvore de um tipo t, considere uma função f : A $\rightarrow$ $\mathbb{N}$ definida da seguinte maneira:

f( Nulo )             = 0

f( No t Esq Dir ) = 1, se Esq = Dir = Nulo

                          = f(Esq) + f(Dir) , caso contrário

Prove que f(A) é o número de folhas da árvore A.

Base: f(Nulo) = 0, a árvore vazia não tem folhas.

Hipótese de Indução: f(Esq) é o número de folhas da árvore Esq e f(Dir) é o número de folhas da árvore Dir.

Passo de Indução:

Caso 1: Esq = Dir = Nulo

Neste caso, x é um folha. O número de folhas da árvore  No x Esq Dir é 1.

Caso 2: Esq != Nulo e Dir != Nulo

Neste caso, x não é folha. O número de folhas da árvore será o número de folhas da subárvore Esq mais o número de folhas da subárvore Dir.

data Arvore t = Nulo | No t (Arvore t) (Arvore t) deriving (Eq, Ord, Show)

folhas Nulo         = 0

folhas (No x esq dir) | (esq == Nulo) && (dir==Nulo)= 1

      | otherwise = folhas esq + folhas dir

*Main> folhas Nulo

0

*Main> folhas (No 2 Nulo Nulo)

1

*Main> folhas (No 2 (No 3 Nulo Nulo) Nulo)

1

*Main> folhas (No 2 (No 3 Nulo Nulo) (No 4 Nulo Nulo))

2