Archive for maio \23\UTC 2011

Provando a Comutatividade da Adição em Agda

maio 23, 2011

Uma das primeiras demonstrações realizadas por todos que utilizam assistentes de provas (ou, linguagens com suporte a tipos dependentes), é a prova formal de que a adição é uma operação comutativa. Por isto, neste post, pretendo apresentar a prova de que a adição é comutativa utilizando a linguagem Agda.

Agda é uma linguagem com suporte a tipos dependentes. Por isso, permite a escrita de proposições e provas na mesma linguagem que escrevemos tipos e programas. Se você não conhece nada sobre Agda, pode julgar interessante este post.

1. Definindo o que é comutatividade.

A comutatividade é uma propriedade tão natural que muitas vezes esquecemos de sua definição formal.  Seja \circ uma operação binária sobre um conjunto A. Dizemos que \circ é comutativa se e somente se:

\forall\,n\,m\in\,A.\, n\,\circ\,m\,=\,m\,\circ\,n

Isso é, se a ordem de aplicação dos parâmetros n e m for irrelevante para \circ, dizemos que esta operação é comutativa.

Mas agora surge a seguinte questão: como provar que a adição é comutativa? Isso é o que abordarei a partir de agora.

2. Uma Prova Informal

Ao tentar utilizar um assistente de provas para a formalização de algum teorema é importante saber como construir a prova “no papel”.

Mas qual a razão disso, já que utilizamos assistentes de provas justamente para não realizar provas “no papel”?

Ao tentarmos provar algum teorema em um assistente de provas sem ter a mínima idéia de como prová-lo, corre-se o risco de simplesmente não conseguirmos provar nada. Isso acontece porquê ao utilizar assistentes de prova, temos que formalizar cada mínima etapa de raciocínio, o que muitas vezes fica sub-entendido em provas convencionais.

Para demonstrar que a adição é comutativa, devemos provar que:

\forall\,n\,m\in\,A.\, n\,\circ\,m\,=\,m\,\circ\,n

Portanto, devemos supor n e m arbitrários e na sequência proceder por indução sobre m (observação: esta indução poderia ser sobre n, mas faremos indução sobre m para ser coerente com a prova a ser apresentada em Agda).

No caso m = 0 temos que:

\begin{array}{lcll}n+m & = & n + 0 & \{\text{como m = 0}\}\\ & = & n & \{\text{por n + 0 = n}\}\\ & = & 0 + n & \{\text{por n = 0 + n}\}\\ & = & m + n _{\Box}& \{\text{como m = 0}\}\end{array}

Seja m = m_{1} + 1 e suponha que n + m_{1} = m_{1} + n. Temos que:

\begin{array}{lcll}n+m & = & n + (m_{1} + 1) & \{\text{como m = m1 + 1}\}\\ & = & (n + m_{1}) + 1 & \{\text{por associatividade}\}\\ & = & (m_{1} + n) + 1 & \{\text{pela h.i.}\}\\ & = & (m_{1} + 1) + n & \{\text{por (n+m)+1 = (n+1) +m}\}\\ & = & m + n _{\Box} &\{\text{por m1 + 1 = m}\} \end{array}

Simples, não? Aliás, é um resultado tão direto que não precisa de prova, mas para construir esta prova em Agda, teremos que provar diversos detalhes que na prova anterior foram aceitos como verdade a priori.

3. A Prova em Agda

Para mostrar, em Agda, que a adição é comutativa,  precisamos primeiro de algumas definições. A primeira delas é, evidentemente, o tipo que define números naturais:

data N : Set where
   zero : N
   succ : N -> N

e uma função para a adição, cuja definição é direta:

_+_ : N -> N -> N
zero + m = m
(succ n) + m = succ (n + m)

Ao contrário de outras linguagens, em Agda, devemos definir praticamente tudo “do zero”, inclusive definições simples como números naturais e adição. Uma funcionalidade que está disponível a priori em quase todas as linguagens de programação é a noção de igualdade. Em Agda, tal noção deve ser implementada manualmente. A próxima seção apresenta a definição de igualdade e alguns resultados sobre esta.

3.1. Igualdade em Agda

Quando lidamos com assistentes de provas, a igualdade é um assunto um pouco problemático. Isso ocorre porquê, em primeiro lugar, a igualdade não é definida (ou decidível) para todos os tipos. Neste post consideraremos apenas a forma mais simples de igualdade, chamada de igualdade proposicional.

A igualdade é codificada pelo seguinte tipo de dados Agda:

data _=_ {A : Set} (x : A) : A -> Set where
     refl : x = x

Isso é, para qualquer valor x de um tipo A qualquer, temos que o construtor refl representa provas de x = x. Para ficar um pouco mais claro, considere a seguinte definição:

oneequalone : 1 = 1
oneequalone = refl

A definição anterior mostra uma prova de que 1 = 1! A primeira vista, parece estranho… pois, para provar isto utilizamos apenas o construtor refl. Mas, de acordo com a definição deste construtor, ele representa provas de que x = x, para qualquer valor x.

A igualdade possui algumas propriedades interessantes. A primeira delas é a transistividade, isto é, se x = y e y = z então x = z. Esta propriedade é representada pelo seguinte teorema Agda:

trans : {A : Set}{x y z : A} -> x = y -> y = z -> x = z
trans refl refl = refl

Mas, isto é apenas uma definição de função! Mas, de acordo com o isomorfismo de Curry-Howard, tipos em linguagens funcionais podem ser pensados como fórmulas da lógica de primeira ordem.  Uma vez que tipos são vistos como fórmulas lógicas, funções de um tipo podem ser vistas como provas da fórmula representada por seu tipo.

No trecho de código anterior temos que o tipo:

trans : {A : Set}{x y z : A} -> x = y -> y = z -> x = z

representa a seguinte fórmula da lógica de primeira ordem:

\forall x\,y\,z\in\,A. x = y \rightarrow y = z \rightarrow x = z

Como o resultado do teorema trans é uma igualdade, temos que refl é o termo que representa esta prova.

Outra propriedade da igualdade que é útil é a chamada congruência, apresentada no trecho de código seguinte:

cong : {A : Set}{f : A -> Set}{x y : A} -> x = y -> f x = f y
cong f refl = refl

A congruência mostra que a igualdade é preservada pela aplicação de funções. Novamente, como a prova envolve uma igualdade, esta é simplesmente o termo refl.

Agora que temos a definição de igualdade e alguns lemas sobre esta podemos começar a demonstrar que a adição é comutativa.

3.2. Alguns Lemas

Se observarmos atentamente a prova informal da comutatividade da adição, podemos perceber que utilizamos alguns fatos que consideramos como verdade, sem demonstrações. Os fatos são:

  • \forall n\,\in\,\mathbb{N}.n+0 = n
  • associatividade da adição.

Estes fatos não podem ser aceitos a priori em Agda. Estes devem ser demonstrados. Como ambas as provas envolvem a adição, que é definida recursivamente sobre números naturais, então, nada mais natural que provar estas propriedades por indução sobe algum dos parâmetros da adição.

Provas por indução em Agda nada mais são que funções recursivas! Portanto, uma prova por indução sobre algum parâmetro da adição nada mais é que uma função recursiva sobre este parâmetro.

O primeiro lema a ser provado é:

\forall n\,\in\,\mathbb{N}.n+0 = n

Como o único parâmetro da adição que podemos utilizar recursão é n, temos que este lema nada mais é que uma função recursiva sobre n. A definição desta segue abaixo:

n+0=n : \forall (n : N) -> (n + 0) = n
n+0=n zero = refl
n+0=n (succ n') = cong succ (n+0=n n')

O caso base desta prova (n = 0) é direto. Já que n = 0, temos que:

\begin{array}{lcll}n+ 0 & = & 0 + 0 & \{\text{como n = 0}\}\\ & = & 0 & \{\text{como 0 + 0 = 0}\}\\ & = & n & \{\text{como n = 0}\}\end{array}

Todos os detalhes desta manipulação algébrica são realizados diretamente pelo próprio sistema de tipos de Agda, que é capaz de “entender” que, a partir da definição da adição, é possível inferir que n+0 = 0, se n= 0. Novamente, como o resultado deste caso é, em última instância, uma igualdade da forma 0 = 0, temos que o termo refl é a definição necessária.

A parte interessante dessa demonstração é o caso indutivo (recursivo). Em provas por indução em Agda, utilizar a chamada hipótese de indução é o mesmo que realizar uma chamada recursiva à função que implementa o teorema a ser provado. No lema anterior, temos que a chamada:

(n+0=n n’)

representa exatamente a utilização da hipótese de indução sobre um valor n’, que é tal que n= succ n'. Este termo, possui o seguinte tipo:

n’ + 0 = n’

Mas como n = succ n’, um termo deste tipo não constitui uma prova para o lema que desejamos provar. O termo que buscamos deve possuir o tipo:

n + 0 = n

parece que não há como prosseguir com a prova, não é mesmo? Se observamos estes dois tipos, vemos que estes são iguais a menos de uma aplicação da função de sucessor, isto é:

n + 0 = n \Leftrightarrow succ (n' + 0) = succ\, n'

Portanto, podemos resolver isso meramente utilizando congruência! Com isso temos que o caso indutivo deste lema é:

n+0=n (succ n’) = cong succ (n+0=n n’)

Simples não?

Para a provar a comutatividade não precisamos de uma versão “geral” da associatividade, mas sim uma versão mais simples. Cuja prova é apresentada a seguir. Faremos a prova por indução sobre n:

sn+m=sn+sm : \forall (n m : N) -> (n + (succ m)) = (succ (n + m))
sn+m=sn+sm zero m = refl
sn+m=sn+sm (succ n') m = cong succ (sn+m=sn+sm n' m)

esta prova possui estrutura similar ao primeiro lema apresentado. Aconselho ao leitor a tentar compreender o raciocínio utilizado. De posse destes dois lemas, podemos finalmente provar a comutatividade da adição.

3.3. Comutatividade da Adição – A prova.

De posse destes dois lemas, podemos provar a comutatividade da adição. Primeiramente, o tipo Agda que representa a fórmula lógica a ser provada é:

n+m=m+n : \forall (n m : N) -> n + m = m + n

A prova será por indução sobre m, de maneira similar a prova informal apresentada na seção 2. Para o caso base, utilizaremos o lema n+0=n, isto é:

n+m=m+n : \forall (n m : N) -> n + m = m + n
n+m=m+n n zero = n+0=n n

Para o caso indutivo, utilizaremos a hipótese de indução, junto com congruência:

n+m=m+n : \forall (n m : N) -> n + m = m + n
n+m=m+n n zero = n+0=n n
n+m=m+n n (succ m') = (cong succ (n+m=m+n n m'))

Porém o tipo de

cong succ (n+m=m+n n m’)

é:

succ (n+m’) = succ (m’+n)

que não é redutível a

n + m = m + n

considerando m = succ m'. Então o que está faltando? O tipo:

succ (n + m’) = succ (m’ + n)

de acordo com a definição de soma é idêntico a:

(succ n) + m’ = (succ m’) + n

que ainda não é igual ao tipo n + m = m + n… Então o que fazer? A solução para este dilema encontra-se em dois lemas ainda não utilizados: a transitividade da igualdade e a associatividade da adição. O lemma da associatividade prova a seguinte fórmula:

sn+m=sn+sm : \forall (n m : N) -> (n + (succ m)) = (succ (n + m))

e a hipótese de indução da comutatividade prova que:

succ (n + m’) = succ (m’ + n)

que é igual a:

succ (n + m’) = (succ m’) + n

e como m = succ\, m', temos que:

succ (n + m’) = m + n

Portanto, para terminar a prova, basta aplicar a transitividade da igualdade a estes dois lemas! A versão final do  teorema é:

n+m=m+n : \forall (n m : N) -> n + m = m + n
n+m=m+n n zero = n+0=n n
n+m=m+n n (succ m') = trans (sn+m=sn+sm n m')(cong succ (n+m=m+n n m'))

Totalmente demais!

4 . Conclusão

Neste post foi apresentada uma prova, passo-a-passo da comutatividade da adição em Agda. Provar teoremas em Agda é uma tarefa árdua (e viciante!) devido a falta de ferramentas que permitam a automação de provas simples (mas entendiantes) como esta que envolve meramente manipulação algébrica.

O principal objetivo do post foi mostrar como uma linguagem com tipos dependentes pode ser utilizada para formalizar teoremas matemáticos, utilizando o isomorfismo de Curry-Howard.