indução estrutural

A indução estrutural é um método de demonstração que é usado na lógica matemática (por exemplo, para provar teoremas), em ciência da computação, em teoria dos grafos, e alguns outros campos da matemática. Podemos dizer que é uma generalização do método de indução matemática. A recursão estrutural é um método de recursão que está para a indução estrutural assim como a recursão ordinária está para a indução matemática usual. Em geral, a ideia é que se deseja demonstrar alguma proposição P(x), onde x é alguma instância de algum tipo de estrutura recursivamente definida, tais como listas ou árvores. Uma ordem parcial (Well-founded) é definida sobre as estruturas. Indução estrutural é um método de demonstração em que a proposição vale para todas as estruturas minimais, e que se valer para as subestruturas de uma determinada estrutura S, então deverá valer para S também. Uma função estruturalmente recursiva usa a mesma ideia de modo a definir uma função recursiva: "os casos base" dão conta de cada estrutura minimal e se há regras para o caso recursivo. A recursão estrutural é geralmente demonstrada correta através da indução estrutural; em casos mais triviais, a etapa indutiva é deixada frequentemente de fora da prova. A função comprimento (length) e a função concatenação são estruturalmente recursivas e mostradas no exemplo abaixo. Por exemplo, imagine que as estruturas que vamos utilizar sejam listas, agora introduza uma ordem parcial ‘<’ na qual L < M. Essa ordem parcial indica que a lista L é a cauda da lista M. Segundo esta ordem parcial, o único elemento minimal é quando temos a lista vazia [ ]. Uma demonstração por indução estrutural de alguma proposição P(L) consiste então em duas partes: Uma demonstração de que P([ ]) é verdadeiro, e uma demonstração que se P(L) for verdadeiro para alguma lista L, e seL < M (L for a cauda de uma lista M), então P(M) também deve ser verdadeiro.