Archive for the ‘Teoria’ Category

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.

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.

Dependências Funcionais

junho 21, 2010

Nesta série de posts, apresentarei os fundamentos de dependências funcionais e sua aplicação ao processo de especialização de tipos na linguagem Haskell. Dependências funcionais foram originalmente introduzidas há anos no estudo de bancos de dados relacionais [1]. Antes de apresentarmos a aplicação de dependências funcionais para a verificação / inferência de tipos, será feita uma breve revisão destes conceitos sob o enfoque da teoria de bancos de dados relacionais.

1 – Relações e Bancos de Dados Relacionais.

Um banco de dados relacional pode ser descrito como um conjunto de relações, onde cada uma destas pode ser vista como uma tabela com zero ou mais tuplas. A seguinte tabela, por exemplo, representa dados de uma consulta que representa os resultados de um questionário hipotético realizado com funcionários de uma empresa.

Nome Bairro Transporte
Alice Harbortown Automóvel
Alice Harbortown A pé
Bob Hillville Bicicleta
Bob Hillville Ônibus
Bob Hillville Automóvel
Carol Hubford Ônibus
David Hubford Trem

Esta tabela possui três colunas (campos) e sete tuplas (registros). Cada registro pode ser descrito por uma tupla (e,b,t) onde e é o nome de um empregado, b é um bairro e t é um meio de transporte. De maneira mais geral, um banco de dados pode ser descrito por um esquema que atribui um nome para cada tabela e também um nome (e possivelmente um tipo) para cada coluna.

Mais formalmente, uma tabela T é uma relação sobre uma família indexada de conjuntos \{D_{i}\}_{i\in I}, onde I é um conjunto de índices (i.e. conjunto de nomes de colunas) e D_{i} é o tipo dos valores da coluna i. Na tabela de exemplo apresentada anterioremente, o conjunto de índices  seria I=\{Nome, Bairro, Transporte \}. Os elementos desta tabela são tuplas, onde cada uma destas é uma família indexada de valores \{t_{i}\}_{i\in I} tal que t_{i}\in D_{i} para cada i\in I. Note que, se I=\{1,...,n\}, então (t_{1},t_{2},...,t_{n})\in D_{1}\times D_{2}\times ...\times D_{n}. Se i \in I, então escrevemos t_{i} para o i-ésimo componente de t. Similarmente, se X\subseteq I, então t_{X}  representa a projeção da tupla $t$ sobre as colunas c_{i}\in X.

2 – Dependências Funcionais

Um esquema de banco de dados irá tipicamente impor certas restrições de integridade para caracterizar a estrutura da informação que é permitida em tabelas do banco. Na tabela de exemplo apresentada anteriormente, é razoável assumir que cada funcionário resida em somente um bairro, isto é, na tabela acima um funcionário deverá estar associado a somente um bairro. Tal restrição é capturada através de uma dependência funcional, representada como \{ Nome \}\rightsquigarrow\{Bairro\}, que garante que dois registros do mesmo empregado devem ter o mesmo bairro associado. Todavia, não existe dependência similar entre os campos Nome e Transporte, uma vez que alguns funcionários utilizam mais de um meio de transporte. É tarefa do SGDB garantir que dependências são mantidas a medida que registros são incluídos ou atualizados. Como exemplo, considere a situação em que o funcionário David se mudasse do bairro Hubford para o bairro Hillville. Neste caso teríamos que a tupla t_{1}=(David, Hubford, Trem) deveria ser alterada para t_{2}=(David, Hillville, Trem), o que não violaria a dependência \{ Nome \}\rightsquigarrow\{Bairro\}. Mas, não poderíamos simplesmente incluir o registro t_{2}, uma vez que esta inclusão não atenderia a restrição especificada por \{ Nome \}\rightsquigarrow\{Bairro\}.

2.1 – Formalizando Dependências Funcionais

Formalmente, se T é uma tabela indexada por um conjunto I, então uma dependência funcional é um par X \rightsquigarrow Y, X determina Y, onde tanto X quanto Y são subconjuntos de I. Se X, Y são conjuntos de elementos conhecidos, isto é X=\{x_{1},x_{2},...,x_{n}\} e Y=\{y_{1},y_{2},...,y_{m}\}, podemos escrever a dependência X \rightsquigarrow Y como x_{1},x_{2},...,x_{n}\rightsquigarrow y_{1},y_{2},...,y_{m}. Se a tabela T satisfaz a dependência X \rightsquigarrow Y, então toda tupla em Y é unicamente determinada pelos valores correspondentes daquela tupla em X. Esta noção pode ser formalizada da seguinte maneira:

T\models X\rightsquigarrow Y \Leftrightarrow \forall t,s \in T. (t_{x} = s_{x})\Rightarrow (t_{y} = s_{y})

A relação T\models X\rightsquigarrow Y pode ser entendida como: “a tabela T satisfaz a dependência X\rightsquigarrow Y“. Uma extensão útil para esta notação é quando consideramos um conjunto de dependências:

T\models F \Leftrightarrow \forall (X \rightsquigarrow Y) \in F. T\models X\rightsquigarrow Y

Outra maneira de entender as dependências funcionais é por meio de regras de inferência para reflexividade, transitividade e acréscimo:

\frac{Y\subseteq X}{X\rightsquigarrow Y}

\frac{X\rightsquigarrow Y\,\,\,\, Y\rightsquigarrow Z}{X\rightsquigarrow Z}

\frac{X\rightsquigarrow Y}{X\cup Z\rightsquigarrow Y\cup Z}

Estas regras são frequentemente denominadas de axiomas de Armstrong, uma vez que William Armstrong[2] foi o primeiro a mostrar que estas são corretas e completas. Estas regras também podem ser estendidas para um conjunto de dependências; dizemos que F_{1}\vdash F_{2} se todas as dependências de F_{2} podem ser deduzidas a partir das dependências de F_{1}. Se F_{1}\vdash F_{2} e F_{2}\vdash F_{1} então os conjuntos de dependências F_{1} e F_{2} são equivalentes e podemos nos referir a uma destes como sendo a cobertura do outro conjunto de regras.

O fecho, J_{F}^{+}, de um conjunto J\subseteq I com respeito a um conjunto de dependências funcionais F é o menor conjunto tal que:

  • J\subseteq J_{F}^{+}
  • Se X\rightsquigarrow Y\in F, e X\subseteq J_{F}^{+}, então Y\subseteq J_{F}^{+}.

Intuitivamente, o fecho J_{F}^{+} é apenas o conjunto de índices que são unicamente determinados, seja direta ou indiretamente, pelos índices em J e as dependências em F.

Conclusão

Dependências funcionais são um conceito consolidado da teoria de bancos de dados relacionais. Neste post foi apresentado uma breve introdução aos principais conceitos relacionados a teoria de bancos de dados relacionais. Nos próximos posts será apresentada a aplicação destes conceitos para verificação / inferência de tipos na linguagem Haskell.

Referências

1 – E. F. Codd. A relational model of data for large shared data banks. Communications of the ACM, 13(6): 377-387, 1970.

2 – W.W. Armstrong. Dependency structures of data base relationships. In IFIP Congress, 580-583, 1974.