# Indução estrutural e provas de programas

Conjuntos recursivos, invariantes de palavras, listas, concatenação, reverse e map.

Página: https://resumos.rgo.pt/cadeiras/md/inducao-estrutural/

Na indução sobre naturais, o passo constrói $n+1$ a partir de $n$. Na **indução estrutural**, seguimos os construtores do objeto: uma palavra pode nascer de outra palavra, uma lista pode nascer de uma cabeça e uma cauda, uma expressão pode nascer de duas subexpressões. Assumimos a ideia de base e passo da lição anterior, aplicada a cada construtor.

Uma definição indutiva descreve os objetos obtidos por um número finito de aplicações das regras. Não inclui objetos adicionais só porque não foram explicitamente proibidos.

## Indução num conjunto recursivo

Se $S$ é o menor conjunto com $3\in S$ e $x,y\in S\Rightarrow x+y\in S$, queremos mostrar:

$$
S=\{3n:n\in\mathbb N^+\}.
$$

Para $S\subseteq\{3n:n\in\mathbb N^+\}$, fazemos indução estrutural:

*   Base: $3=3\cdot1$ é um múltiplo positivo de 3.
*   Construtor: se $x=3a$ e $y=3b$ com $a,b>0$, então $x+y=3(a+b)$, também múltiplo positivo de 3.

Isto prova que as regras nunca produzem outro tipo de valor, mas ainda falta a inclusão inversa. Por indução no natural positivo $n$, $3\cdot1\in S$ e, se $3n\in S$, então $3(n+1)=3n+3\in S$; mostrar que todos os elementos construídos têm uma propriedade não prova que todos os objetos com essa propriedade se constroem, por isso verifica as duas direções numa igualdade de conjuntos.

## Palavras e invariantes

Considera palavras sobre $\{a,b\}$ construídas por estas regras: a palavra vazia $\varepsilon$ pertence a $L$; se $x\in L$, então $axb,bxa\in L$; se $x,y\in L$, então $xy\in L$.

Para construir `aabb`, partimos de $\varepsilon$, aplicamos $x\mapsto axb$ e obtemos `ab`. Aplicamos o mesmo construtor a `ab` e obtemos `aabb`. Não existe nas regras uma operação que acrescente apenas um `a`; o par exterior entra numa única aplicação.

Vamos provar que cada palavra de $L$ tem tantos $a$ como $b$. O caso base tem zero de cada. Se $x$ tem $k$ de cada, $axb$ e $bxa$ têm $k+1$ de cada. Se $x$ tem $k$ de cada e $y$ tem $m$ de cada, a concatenação tem $k+m$ de cada. Tratámos todos os construtores.

Uma propriedade que se conserva em cada construção chama-se **invariante**. Pode servir para mostrar que uma palavra não pertence ao conjunto: `aaabb` não pode pertencer a $L$, porque tem contagens diferentes. Para mostrar que pertence, fornece uma construção a partir das bases.

## Parênteses equilibrados

Se as regras são $()\in E$, $x\in E\Rightarrow(x)\in E$ e $x,y\in E\Rightarrow xy\in E$, todas as expressões têm igual número de aberturas e fechos, mas podemos provar uma propriedade mais forte: em cada prefixo, o número de fechos não excede o de aberturas. Define o saldo como aberturas menos fechos.

*   Em `()`, os prefixos têm saldos 0, 1 e 0.
*   Em $(x)$, o primeiro parêntese acrescenta 1 ao saldo de cada prefixo de $x$. O último fecha a abertura exterior.
*   Em $xy$, um prefixo fica em $x$ ou atravessa $x$ e entra em $y$. No segundo caso, o saldo total de $x$ é zero e o saldo restante é o do prefixo de $y$.

Contagens totais iguais não chegam para esta propriedade: `)(` tem uma abertura e um fecho, mas o seu primeiro prefixo já tem saldo negativo. Para ver a diferença, seguimos o saldo após consumir $n$ símbolos de cada palavra. $n=0$ corresponde ao prefixo vazio; uma célula vazia indica que a palavra já terminou.

| $n$ | Saldo de `(())` | Saldo de `)(` |
| --- | --- | --- |
| 0 | 0 | 0 |
| 1 | 1 | −1 |
| 2 | 2 | 0 |
| 3 | 1 |  |
| 4 | 0 |  |

O saldo final é zero nos dois casos. Só a primeira palavra mantém todos os prefixos com saldo não negativo. A definição de $E$ não inclui a palavra vazia: cada expressão começa em `()` e tem pelo menos dois símbolos, embora o prefixo vazio seja usado no teste do saldo.

## Indução sobre listas finitas

Uma lista finita tem dois construtores: `[]`, a lista vazia, e `x:xs`, uma cabeça `x` seguida da cauda `xs`. Para provar uma propriedade de todas as listas finitas:

1.  Prova o caso `[]`.
2.  Para uma cabeça arbitrária `x` e uma cauda arbitrária `xs`, assume a propriedade de `xs` e prova-a para `x:xs`.

A hipótese pertence à cauda, não à lista inteira. Não usamos este princípio para listas infinitas de Haskell.

Em Haskell, `f x` aplica a função `f` a `x`; `[x]` abrevia `x:[]`; `++` concatena listas. As definições seguintes são equações para listas finitas:

```
length [] = 0
length (x:xs) = 1 + length xs

[] ++ ys = ys
(x:xs) ++ ys = x : (xs ++ ys)

reverse [] = []
reverse (x:xs) = reverse xs ++ [x]
```

Na concatenação, a recursão analisa a primeira lista. Por isso, induzir nessa lista costuma permitir aplicar logo a equação recursiva.

## Comprimento de uma concatenação

Queremos `length (xs ++ ys) = length xs + length ys` para quaisquer listas finitas. Fazemos indução em `xs`, mantendo `ys` arbitrária.

Na base:

```
length ([] ++ ys)
= length ys                        definição de ++
= 0 + length ys                    aritmética
= length [] + length ys            definição de length
```

No passo, a hipótese é `length (xs ++ ys) = length xs + length ys`:

```
length ((x:xs) ++ ys)
= length (x : (xs ++ ys))           definição de ++
= 1 + length (xs ++ ys)             definição de length
= 1 + length xs + length ys         hipótese de indução
= length (x:xs) + length ys         definição de length
```

Nomear a equação usada em cada passagem permite conferir a prova sem executar o programa.

## Uma função acrescenta dois elementos por passo

Considere-se uma função que coloca um separador depois de cada elemento da lista:

```
interleave x [] = []
interleave x (y:ys) = y : x : interleave x ys
```

`interleave 0 [2,3]` dá `[2,0,3,0]`. O separador também aparece depois do último elemento. Queremos provar `length (interleave x ys) = 2 * length ys` para todas as listas finitas, com `x` arbitrário.

A base dá `length [] = 2 * length []`, isto é, `0 = 0`. No passo, toma uma cabeça `y` e uma cauda `ys`. A hipótese só fornece a igualdade para essa cauda:

```
length (interleave x (y:ys))
= length (y : x : interleave x ys)  definição de interleave
= 1 + 1 + length (interleave x ys)  duas aplicações de length
= 2 + 2 * length ys                hipótese de indução
= 2 * (1 + length ys)              distributividade
= 2 * length (y:ys)                definição de length
```

A chamada recursiva recebe apenas `ys`; é aí que a hipótese se aplica. Mesmo quando `x=y`, foram acrescentadas duas posições, não uma: listas conservam repetições.

## Associatividade da concatenação

Para `(xs ++ ys) ++ zs = xs ++ (ys ++ zs)`, induzimos em `xs`, com `ys,zs` arbitrárias. Na base, ambos os lados reduzem a `ys ++ zs`; no passo:

```
((x:xs) ++ ys) ++ zs
= (x : (xs ++ ys)) ++ zs
= x : ((xs ++ ys) ++ zs)
= x : (xs ++ (ys ++ zs))            hipótese de indução
= (x:xs) ++ (ys ++ zs)
```

Também precisamos da identidade à direita `xs ++ [] = xs`. A base é `[] ++ [] = []`; no passo, `(x:xs) ++ [] = x:(xs ++ []) = x:xs` pela hipótese.

## Reverse de uma concatenação

O lema é:

```
reverse (xs ++ ys) = reverse ys ++ reverse xs
```

Na base `xs=[]`, o lado esquerdo é `reverse ys`; o direito é `reverse ys ++ []`, igual pelo lema da identidade à direita. No passo:

```
reverse ((x:xs) ++ ys)
= reverse (x : (xs ++ ys))
= reverse (xs ++ ys) ++ [x]
= (reverse ys ++ reverse xs) ++ [x]   hipótese de indução
= reverse ys ++ (reverse xs ++ [x])   associatividade de ++
= reverse ys ++ reverse (x:xs)
```

É este lema que falta quando tentamos provar que inverter duas vezes recupera a lista:

```
reverse (reverse (x:xs))
= reverse (reverse xs ++ [x])
= reverse [x] ++ reverse (reverse xs)  lema anterior
= [x] ++ xs                          hipótese de indução
= x:xs
```

A base é `reverse (reverse []) = []`. Os lemas são necessários porque a hipótese de indução só fala de `reverse (reverse xs)`, não de `reverse (reverse xs ++ [x])`.

## Fusão de map

`map f` aplica `f` a cada elemento. A composição `(f . g) x` é `f (g x)`:

```
map f [] = []
map f (x:xs) = f x : map f xs
(f . g) x = f (g x)
```

Podemos provar `map f (map g xs) = map (f . g) xs` por indução em `xs`. A base dá `[]` dos dois lados. No passo:

```
map f (map g (x:xs))
= map f (g x : map g xs)
= f (g x) : map f (map g xs)
= (f . g) x : map (f . g) xs         hipótese e definição de composição
= map (f . g) (x:xs)
```

A igualdade permite juntar duas travessias numa. A prova explica por que a transformação conserva os valores para todas as listas finitas, sem depender de exemplos escolhidos.

## Provar que uma ordenação ordena

Considere-se a ordenação por inserção de elementos com uma ordem total:

```
insert x [] = [x]
insert x (y:ys)
  | x <= y = x:y:ys
  | otherwise = y : insert x ys

sort [] = []
sort (x:xs) = insert x (sort xs)
```

Para provar que `sort xs` está ordenada, primeiro provamos o lema: inserir `x` numa lista ordenada conserva a ordenação.

A lista vazia produz `[x]`, ordenada. Para `y:ys` ordenada, se `x <= y`, o resultado começa em `x,y` e conserva a cauda. Se `x > y`, aplicamos a hipótese à inserção na cauda. Os valores de `ys` são todos pelo menos `y`, e o novo valor `x` também é maior que `y`; logo, a cabeça `y` continua antes de uma cauda ordenada.

Na prova de `sort`, a base é vazia. No passo, a hipótese garante que `sort xs` está ordenada, e o lema garante que `insert x (sort xs)` também está.

### Conservação das multiplicidades

Para um valor $v$, seja $\operatorname{conta}_v(xs)$ o número de ocorrências de $v$ na lista. Vale $\operatorname{conta}_v([])=0$ e

$$
\operatorname{conta}_v(y:ys)=\mathbf 1_{v=y}+\operatorname{conta}_v(ys),
$$

onde $\mathbf 1_{v=y}$ é 1 se $v=y$ e 0 no caso contrário. Queremos provar o lema

$$
\operatorname{conta}_v(\operatorname{insert}(x,ys)) =\operatorname{conta}_v(ys)+\mathbf 1_{v=x}.
$$

Fazemos indução em $ys$, com $x,v$ arbitrários. A base dá a lista $[x]$, com exatamente $\mathbf 1_{v=x}$ ocorrências. No passo $ys=y:zs$, se $x\le y$, a saída é $x:y:zs$ e contamos $\mathbf 1_{v=x}+\mathbf 1_{v=y}+\operatorname{conta}_v(zs)$. Se $x>y$, a saída é $y:\operatorname{insert}(x,zs)$; pela hipótese, a contagem é $\mathbf 1_{v=y}+\operatorname{conta}_v(zs)+\mathbf 1_{v=x}$. Ambas são a contagem original mais a ocorrência inserida.

Na indução sobre `sort`, a base conserva zero ocorrências. No passo, o lema acrescenta exatamente a ocorrência da cabeça $x$ às contagens de `sort xs`, que pela hipótese são as de `xs`. Assim, a contagem final coincide com a de `x:xs` para todo o $v$.

Ordenação não é toda a correção: a função que devolve sempre `[]` também devolve uma lista ordenada. Para provar que é uma ordenação do conteúdo original, precisamos ainda de mostrar que conserva os elementos e as suas multiplicidades.

## Exercícios

O conjunto gerado por uma regra

Seja $S$ o menor subconjunto de $\mathbb N$ que contém 3 e tal que $x\in S$ implica $x+2\in S$. Prova $S=\{2k+3:k\in\mathbb N\}$.

Pista

Uma igualdade de conjuntos exige as duas inclusões.

Mais uma pista

Usa indução estrutural para $S\subseteq T$ e indução em $k$ para $T\subseteq S$.

Solução

Base estrutural: $3=2\cdot0+3$. Se $x=2k+3$, então $x+2=2(k+1)+3$, logo todo o elemento gerado está em $T$. No sentido inverso, $k=0$ dá 3. Se $2k+3\in S$, a regra dá $2(k+1)+3\in S$. Assim cada elemento de $T$ pertence a $S$.

Confere a tua resposta:

*   Provei que tudo o que é gerado tem a forma indicada.
*   Provei que cada 2k + 3 pode ser gerado.
*   Usei o menor conjunto, não qualquer conjunto fechado pela regra.

Erros frequentes

Mostrar só que T contém 3 e é fechado pela regra permite concluir S ⊆ T, mas ainda não demonstra a inclusão inversa.

[Voltar à explicação](https://resumos.rgo.pt/cadeiras/md/inducao-estrutural/#indu%C3%A7%C3%A3o-num-conjunto-recursivo)

Uma transformação conserva o comprimento

Com $\operatorname{map}\ f\ []=[]$, $\operatorname{map}\ f\ (x:xs)=f(x):\operatorname{map}\ f\ xs$ e a definição usual de length, prova $\operatorname{length}(\operatorname{map}\ f\ xs)=\operatorname{length}(xs)$ para listas finitas.

Pista

O caso indutivo tem a forma $x:xs$. A imagem de x pode mudar, mas continua a ser um elemento.

Mais uma pista

Desenrola primeiro `map` e depois length; a hipótese aplica-se a $\operatorname{map}\ f\ xs$.

Solução

Base: $\operatorname{length}(\operatorname{map}\ f\ [])=\operatorname{length}([])=0$. Passo, com a hipótese para $xs$:

$$
\begin{aligned} \operatorname{length}(\operatorname{map}\ f\ (x:xs)) &=\operatorname{length}(f(x):\operatorname{map}\ f\ xs)\\ &=1+\operatorname{length}(\operatorname{map}\ f\ xs)\\ &=1+\operatorname{length}(xs)\\ &=\operatorname{length}(x:xs). \end{aligned}
$$

Logo a propriedade vale para todas as listas finitas e qualquer função $f$.

Confere a tua resposta:

*   Verifiquei a lista vazia.
*   Fixei um elemento x e uma cauda xs arbitrários.
*   Apliquei a hipótese só à cauda e terminei pela definição de length.

Erros frequentes

Não precisas de f ser injetiva. Valores repetidos continuam a ocupar posições distintas na lista.

[Voltar à explicação](https://resumos.rgo.pt/cadeiras/md/inducao-estrutural/#indu%C3%A7%C3%A3o-sobre-listas-finitas)

Justificar uma ordenação

Considera esta ordenação por inserção, sobre listas finitas cujos elementos têm uma ordem total:

```
insert x [] = [x]
insert x (y:ys)
  | x <= y = x:y:ys
  | otherwise = y : insert x ys

sort [] = []
sort (x:xs) = insert x (sort xs)
```

Prova por indução nas listas que, para cada valor $v$,

$$
\operatorname{conta}_v(\operatorname{insert}(x,ys)) =\operatorname{conta}_v(ys)+\mathbf 1_{v=x},
$$

com $\operatorname{conta}_v([])=0$ e $\operatorname{conta}_v(y:ys)=\mathbf 1_{v=y}+\operatorname{conta}_v(ys)$. O indicador é 1 quando a igualdade é verdadeira e 0 quando é falsa. Usa depois esse lema para provar que `sort` conserva todas as multiplicidades. Que outra propriedade falta para concluir a correção da ordenação?

Pista

Ordenada não significa necessariamente uma permutação da entrada.

Solução

O lema das contagens prova-se por indução em $ys$, com $x,v$ arbitrários. Na base, `insert x [] = [x]`, que tem $\mathbf 1_{v=x}$ ocorrências de $v$.

No passo $ys=y:zs$:

*   Se $x\le y$, `insert x (y:zs) = x:y:zs`. A contagem é $\mathbf 1_{v=x}+\mathbf 1_{v=y}+\operatorname{conta}_v(zs)$, a contagem de $ys$ mais $\mathbf 1_{v=x}$.
*   Se $x>y$, o resultado é `y : insert x zs`. A hipótese para a cauda dá $\mathbf 1_{v=y}+\operatorname{conta}_v(zs)+\mathbf 1_{v=x}$, o mesmo valor pedido.

Para `sort`, a base devolve `[]` e conserva todas as contagens. No passo, usando o lema e depois a hipótese para `xs`:

$$
\begin{aligned} \operatorname{conta}_v(\operatorname{sort}(x:xs)) &=\operatorname{conta}_v(\operatorname{insert}(x,\operatorname{sort}(xs)))\\ &=\operatorname{conta}_v(\operatorname{sort}(xs))+\mathbf 1_{v=x}\\ &=\operatorname{conta}_v(xs)+\mathbf 1_{v=x}\\ &=\operatorname{conta}_v(x:xs). \end{aligned}
$$

Falta ainda provar que a saída está ordenada. Isso usa o lema de que `insert` conserva a ordenação quando a lista recebida está ordenada. Conservar contagens não distingue `sort` da função identidade, que também conserva todos os elementos mas pode deixar a lista desordenada.

Confere a tua resposta:

*   Exigi que insert preserve ordenação quando recebe uma lista ordenada.
*   Provei o lema das contagens nos dois ramos de insert.
*   Usei o lema na prova das contagens de sort e distingui-a da ordenação.

Erros frequentes

Provar apenas ordenação aceita programas que apagam elementos ou duplicam valores. A correção exige também conservação das multiplicidades.

[Voltar à explicação](https://resumos.rgo.pt/cadeiras/md/inducao-estrutural/#provar-que-uma-ordena%C3%A7%C3%A3o-ordena)