Provando a Comutatividade da Adição em Agda

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 uma operação binária sobre um conjunto A. Dizemos que é comutativa se e somente se:

Isso é, se a ordem de aplicação dos parâmetros n e m for irrelevante para , 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:

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 temos que:

Seja e suponha que . Temos que:

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 ! 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 , para qualquer valor x.

A igualdade possui algumas propriedades interessantes. A primeira delas é a transistividade, isto é, se e então . 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:

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:

• 
• 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 é:

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 () é direto. Já que , temos que:

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 , se . Novamente, como o resultado deste caso é, em última instância, uma igualdade da forma , 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 . 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 é:

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 . 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 , 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.

Agda – Uma linguagem com tipos dependentes

Um problema recorrente em linguagem com suporte a arrays é a tentativa de acesso a uma posição inválida. Um pequeno exemplo deste inconveniente acontece neste simples algoritmo para busca sequencial em Java:

public int search(int [] vector, int key) {
     for(int i = 0; i <= vet.length; i++)
         if (vet[i] == key) return i;
     return -1;
}

É fácil ver que este código causará um ArrayIndexOutOfBoundsException, já que a variável que controla a condição de parada do loop é inicializada em zero e é testada se é menor ou igual ao número de elementos do arranjo. Em Java e C/C++ o intervalo de elementos em um array vai de zero ao número de elementos do arranjo menos um. Com isso, ao tentarmos acessar a n-ésima posição do array estaremos acessando uma área de memória inválida, causando a já acima citada exceção ou um possível segmentation fault ou outros erros mirabolantes em C/C++.

Idealmente erros como este deveriam ser capturados pelo compilador durante a verificação estática do programa no processo de compilação. Porém, verificar se o valor de indexação de um array está dentro dos limites deste é um problema indecidível, já que é equivalente ao problema da parada.

Então devemos conviver com estes tipos de erros esdrúxulos e ser mais atentos quando usamos arrays? Na verdade, isso não é necessário. Existem linguagens de programação que podem remediar esta situação utilizando os chamados tipos dependentes (dependent types) adicionando “mais informação” aos tipos de arranjos, permitindo assim, que o compilador capture estaticamente um acesso a uma posição inválida de um arranjo. Atualmente, existem diversas linguagens que dão suporte a tipos dependentes, estas são utilizadas principalmente como assistentes de provas.

Neste post, pretendo apresentar a linguagem Agda, uma linguagem funcional com suporte a tipos dependentes.

Tipos de dados em Agda.

Pessoas que já desenvolveram algum programa ou pelo menos conhecem a linguagem Haskell, não encontrarão dificuldades em aprender Agda, já que a sintaxe dessa linguagem é baseada na sintaxe de Haskell. Como um primeiro exemplo, considere a seguinte definição do tipo de dados Bool em Haskell (infelizmente o wordpress não fornece syntax highlighting para Haskell e Agda):

data Bool = True | False

A definição acima é usual. O tipo de dados Bool possui dois construtores, a saber: True e False. A mesma definição em Agda é:

data Bool : Set where
    true  : Bool
    false : Bool

Apesar de similares, as definições possuem algumas diferenças. Primeiramente, na definição em Agda, o tipo Bool é seguido por uma anotação de Sort. Podemos pensar em um Sort, como sendo um “tipo de tipos”. Anotar um tipo com o sort “Set” indica que este é um tipo. Na sequência, logo após a palavra reservada where, temos a especificação dos construtores de dados deste tipo. Note que estes construtores são também anotados, mas, com o tipo Bool.

Ao contrário de outras linguagens de programação, em Agda, todos os tipos de dados podem ser construídos a partir de princípios simples. Por exemplo, na linguagem o tipo de números naturais é definido na biblioteca padrão da linguagem como:

data Nat : Set where
   Z : Nat
   S : Nat -> Nat

Em Agda, números naturais são representados utilizando os axiomas de Peano, onde números naturais são representados por sucessivas aplicações da função sucessor ao número zero. A definição anterior apresenta o tipo de dados Nat que representa números naturais de acordo com a axiomática de Peano. O tipo Nat possui dois construtores: Z que representa o número natural zero e S, que representa a função sucessor. Para facilitar a utilização, os compiladores Agda reconhecem que , isto é, a linguagem ofecere um suporte a definição de números formados algarismos arábicos convencionais. Internamente, o compilador realiza a conversão entre estes números e o tipo de dados Nat.

Funções em Agda

Por ser uma linguagem funcional, Agda permite a definição de funções sobre tipos de dados por meio de casamento de padrão. A seguinte função codifica a soma de dois números naturais:

_+_ : Nat -> Nat -> Nat
Z + m = m
(S n) + m = S (n + m)

A definição recursiva da soma de dois números naturais é direta: Caso o primeiro deles seja zero, o resultado da soma é o segundo. Caso o primeiro seja um número diferente de zero (isto é, um número da forma para algum ) o resultado da soma será o sucessor da soma de com o segundo parâmetro .

Tipos dependentes

A motivação apresentada no início deste post era evitar que operações de acesso a elementos de arranjos pudessem acessar posições inválidas desses arranjos. Para podermos contornar esta situação, é necessário que a linguagem permita combinar valores e tipos para definir novos tipos. Tipos dependentes são tipos que “dependem” de valores e não apenas de outros tipos como o caso de construtores de tipos em linguagens que suportam polimorfismo paramétrico. A definição a seguir apresenta um tipo de dados que representa vetores de um determinado tamanho:

data Vec (A : Set) : Nat -> Set where
      [ ] : Vec A Z
      _::_ : {n : Nat} -> A -> Vec A n -> Vec A (S n)

Esta declaração possui um número de coisas “interessantes”. Primeiramente, o tipo Vec não é um valor do
sort Set, mas sim uma família de tipos indexada por um valor de tipo Nat, isto é, Nat -> Set. Intuitivamente, o tipo Vec A n representa o tipo de vetores de valores de tipo A com exatamente n elementos. Este tipo é formado por dois construtores de dados:

• [ ] :: Vec A Z, que representa um vetor com zero elementos de tipo A.
• _::_ : {n : Nat} -> A -> Vec A n -> Vec A (S n), que representa a inserção de um elemento de tipo A em um vetor com n elementos, produzindo um vetor de n + 1 elementos.

Oberve que o tipo dos construtores captura invariantes sobre as funções que os definem. O construtor de lista vazia, codifica em seu tipo, o fato de que não possui nenhum elemento e o construtor _::_ captura o invariante de que após a inserção de um elemento em um vetor contendo n elementos este passa a possuir n + 1 elementos.

Com este tipo, é possível obter uma função “segura” que obtem o primeiro elemento de uma lista. Em Haskell, tal função pode causar problemas, pois sua implementação na biblioteca Prelude é:

head :: [a] -> a
head [ ] = error "Prelude.head: empty list."
head (x:_) = x

Se a função head for aplicada a uma lista vazia, ocorrerá a interrupção da execução do programa devido a chamada da função error. Em Agda, tal situação é contornada, evitando em tempo de compilação que uma função similar a head seja aplicada a um vetor vazio. O código desta função é apresentado a seguir:

vhead : {A : Set} {n : Nat} -> Vec A (S n) -> A
vhead (x :: xs) = x

Neste exemplo, pode-se observar que a aplicação da função vhead a um vetor vazio não é possível pois esta função exige como parâmetro um vetor que possua pelo menos um elemento (fato representado pelo tipo do parâmetro: Vec A (S n)). Totalmente demais!

Representando provas

O sistema de tipos de Agda é suficientemente expressivo para permitir que expressemos proposições lógicas arbitrárias como tipo e seus valores como provas. Como exemplo, podemos definir os seguintes tipos que representam, respectivamente, proposições verdadeiras e falsas:

data True : Set where
     trivial : True

data False : Set where

No trecho de código acima, podemos observar que uma proposição verdadeira (representada pelo tipo True) possui uma prova trivial (representada pelo construtor trivial). Por sua vez, uma proposição falsa, representada pelo tipo False não possui prova, já que, consideramos como falso algo que não possui prova de que é verdadeira (considerando a lógica intuicionista).

Com isso, podemos definir uma função que representa proposições decidíveis (isto é, que são verdadeiras ou falsas):

isTrue : Bool -> Set
isTrue true = True
isTrue false = False

Com isso temos que, isTrue b é o tipo de provas de que b é igual a true. Com isto, podemos implementar uma função segura para obter o n-ésimo elemento de uma lista. Para isso, primeiramente devemos definir um tipo que expressa quando um número natural n é menor que outro número natural m. Este tipo é apresentado a seguir:

_<_ : Nat -> Nat -> Bool
_  < zero = false
zero  < m = true
(S n) < (S m) = n < m 

Além disso, vamos precisar de uma função que calcula o número de elementos de uma lista. A implementação desta função é trivial:

 length : {A : Set} -> List A -> Nat
length [ ] = Z
length (x :: xs) = S (length xs)

Agora possuímos todo o arsenal necessário para codificar uma função segura para obter o n-ésimo elemento em uma lista. Podemos conjecturar que a função de obter o n-ésimo elemento de uma lista é segura se e somente se n < length xs. Tal fato pode ser codificado pelo tipo:

lookup : {A : Set}(xs : List A)(n : Nat) ->
           isTrue (n < length xs) -> A

onde o parâmetro isTrue (n < length xs) representa uma prova da proposição n < length xs. O código completo da função lookup é apresentado a seguir:

lookup : {A : Set}(xs : List A)(n : Nat) ->
             isTrue (n < length xs) -> A
lookup [] n  ()
lookup (x :: xs) zero p = x
lookup (x :: xs) (suc n) p = lookup xs n p

Temos as seguintes possibilidades para esta definição: se n é maior que o tamanho da lista xs então não é possível obter uma prova de isTrue (n < length xs). Na definição de lookup, a primeira equação representa a situação de quando não é possível obter uma prova de n < length xs. A notação () representa uma padrão absurdo permitindo assim, que o lado direito da equação seja omitido. As duas equações seguintes lidam com a possibilidade de ser possível obter uma prova para n < length xs.

Conclusão

Neste post foi apresentado uma pequena introdução a linguagem Agda. Tipos dependentes apresentam uma possibilidade interresante para o desenvolvimento por permitiram a codificação de invariantes que podem ser verificados estaticamente pelo compilador.

Este post foi inspirado no artigo Dependently Typed Programming in Agda por Ulf Norell. Maiores informações sobre Agda, downloado do compilador da linguagem podem ser encontrados no site http://wiki.portal.chalmers.se/agda/pmwiki.php.

Consequências Computacionais da lei do Terceiro Excluído

Recentemente em meu doutorado tenho dedicado grande esforço em compreender e utilizar a lógica intuicionista. Sendo extremamente simplista, a lógica intuicionista é um sistema formal que difere da lógica clássica em apenas um ponto: a lei do terceiro excluído e eliminação da dupla negação não são axiomas.

A lei do terceiro excluído é de simples compreensão: Toda proposição lógica deve ser verdadeiro ou falsa. Mais formalmente:

Aparentemente tal afirmação ingênua (e por sinal bastante lógica!) não possui nenhum tipo de complicação inerente ou mesmo qualquer relação com os fundamentos da computação. De acordo com o isomorfismo de Curry-Howard, caso sejamos capazes de construir uma prova para uma proposição qualquer, é possível extrair desta prova um programa funcional cujo tipo é isomórfico à proposição provada. Sendo assim, assuma o seguinte predicado que é verdadeiro se um determinado programa pára e falso caso contrário. Considere, então, agora a seguinte proposição:

Se o isomorfismo de curry howard estiver correto, podemos construir uma prova para esta afirmativa e esta poderia ser utilizada para obtermos um algoritmo que decide para um programa arbitrário se este pára ou não. É fato bem conhecido, que o chamado problema da parada é indecidível e portanto não é possível obter tal programa. Então, qual o problema? O isomorfismo de Curry Howard está incorreto? O grande “pulo-do-gato” é que o isomorfismo de Curry-Howard é restrito à lógica intuicionista, que requer uma prova para afirmar que uma determinada proposição é verdadeira ou falsa.

É evidente que a adoção da lei do terceiro excluído é problemática em termos computacionais, já que esta implicaria na solução do problema da parada.

Sobre o título deste blog

Geralmente todo blogueiro possui algum motivo especial para a escolha do título de seu blog. Eu não poderia ser escapar a esta regra.

Neste blog, além de discorrer sobre assuntos diversos, prentendo publicar textos sobre lógica e programação funcional. Então porque o título “Esta frase é falsa”?

Este consiste de um conhecido paradoxo da lógica, que apesar de sua simplicidade, mostra os “diabos” que residem nos cantos obscuros da matemática.

Se a proposição “esta frase é falsa” for verdadeira, temos que ela será falsa, já que a proposição afirma que ela própria é falsa. Por sua vez se a considerarmos falsa, temos que ela será verdadeira, pois ela própria afirma que é falsa, sendo assim só pode ser verdadeira.