Archive for março \14\UTC 2011

Agda – Uma linguagem com tipos dependentes

março 14, 2011

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 1 = S\,\,Z, 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 S\,\,n para algum n) o resultado da soma será o sucessor da soma de n com o segundo parâmetro m.

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.

Anúncios

Notas sobre o “Ensaio sobre a cegueira”

março 9, 2011

Hoje, acabei de ler o ensaio sobre a cegueira (para ser mais preciso há 15 minutos atrás)…

Esta obra de Saramago  é uma crítica aos valores sociais, expondo o caos a que se chega quando a maioria da população cega. Uma característica interessante do texto é que os personagens não têm nomes, sendo descritas por características próprias – o primeiro cego, o médico, a mulher do primeiro cego, a rapariga de óculos, entre tantos outros que aparecem no desenrolar da narrativa, onde uma epidemia se alastra a partir de um homem que cega esperando o semáforo abrir.

A narrativa leva-nos a refletir sobre a moral e o preconceito, pois faz com que a mulher do médico se depare com situações inadmissíveis às pessoas em condições normais. Exposta à sujeira, a uma existência miserável em todos os sentidos, ela mata para preservar a si e aos demais, e se depara com a morte de maneira bizarra após a saída do hospício: os cadáveres se espalham pelas ruas, o fogo fátuo aparece debaixo das portas do armazém onde, dias antes, ela buscou comida.

Vários pontos ficaram sem explicação (provavelmente, de propósito…). No último parágrafo do texto, fica “no” que a mulher do médico (a única que enxergava durante toda a narrativa) ficou cega, mas nada é confirmado.
Um dos mais interessantes pontos da narrativa foi quando entrou na igreja, a mulher do médico se deparou com imagens de santos com vendas brancas em seus olhos. Talvez Saramago sejasse mostrar que “se os céus não vêem, que ninguém veja”…

Consequências Computacionais da lei do Terceiro Excluído

março 6, 2011

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:

\forall p . P \lor \neg P

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 halt(p) que é verdadeiro se um determinado programa p pára e falso caso contrário. Considere, então, agora a seguinte proposição:

\forall p. halt(p) \lor \neg halt(p)

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

Atrasos e novas leituras

março 4, 2011

Recentemente adquiri os 5 livros da saga “O Guia do Mochileiro das Galáxias” de Douglas Adams, no submarino por um precinho bem camarada e frete grátis. Mas, como eu deveria ter suposto inicialmente, o frete gratuito possui o desagradável incômodo da demora. Já fazem quinze dias e nada dos livros chegarem. Vou mandar um e-mail para o atendimento do submarino e verificar o que está acontecendo…

Nestes últimos dias, terminei o livro “O Evangelho segundo jesus cristo” de Saramago. Simplesmente espectacular. Para o leitor que não o tenha lido, recomendo fortemente. O ápice do romance está no diálogo entre deus, o diabo e jesus no mar… Realmente, Saramago soube como explorar uma história que já foi contada várias vezes.

Enquanto não chegam meus livros de Douglas Adams, iniciei a leitura de “Ensaio sobre a Cegueira”, também de José Saramago. Até o presente momento, o livro está prendendo bastante minha atenção, imaginar uma “cegueira branca” que é contagiosa e as diversas implicações de um surto de tal doença mostram, neste romance o quanto de escuridão pode haver dentro de cada ser humano.

Para finalizar, estes dias andei jogando um pouco de Wii e trabalhando um pouco com Agda, uma linguagem com suporte a tipos dependentes. Em breve, postarei algo sobre Agda…