Encoding a Well-founded Relation over pairs in Coq Proof Assistant

abril 23, 2012

This will be my very first post in English in this blog. Therefore, I would like to apologize in advance for any errors.

This post will assume that the reader knows what is a well-founded relation and has a basic knowledge of Coq proof assistant.

First of all, we will need some library definitions of what is a well-founded relation and what is an accessible term (considering some relation). Both definitions are in the module Wellfounded of Coq standard library. So, we start our development importing this module.

</p><p>Require Import Wellfounded.</p><p>

How we can define a well-founded relation for pairs? First, the elements of the given pairs must support some kind of ordering. So, we will parametrize our definition by a type of these elements and a ordering relation between them.  We will assume that the parameter is a strict partial order, but no changes are needed to use an partial order. These definitions are given next:

 

</p><p>Section LexicographicOrdering.</p><p>       Variable A : Type.</p><p>       Variable ltA : A -&gt; A -&gt; Prop.</p><p>

Given a strict ordering relation < and a equality = over values a given set A, we could order pairs of A using the following definition:

\forall x\, x'\, y\,y'\in A. x < x' \lor (x = x' \land y < y') \rightarrow (x,y) < (x',y').

The previous mathematical formula can be encoded using the following inductive type:

</p><p>  Inductive lexprod : A * A -&gt; A * A -&gt; Prop :=<br />  | left_lex : forall (x1 x2 y1 y2 : A),<br />     ltA x1 x2 -&gt; lexprod (x1, y1) (x2, y2)<br />  | right_lex : forall (x1 x2 y1 y2 : A),<br />     x1 = x2 -&gt; ltA y1 y2 -&gt; lexprod (x1, y1) (x2, y2).</p><p>

The type lexprod uses the ordering relation ltA, previously defined. The constructor left_lex, encodes the condition that if x < x' then the pair (x,y) < (x',y') for any values of y and y’. On the other hand, the constructor right_lex encodes the condition that if x = x' and $y < y’$ then the pair (x,y) < (x',y').

Now, it remains to prove that lexprod definition is a well founded relation, under the assumption that ltA is well founded. This can be easily proved by induction over the proof of accessibility relation for ltA, as shown by the next source code piece:

</p><p>  Lemma acc_A_lexprod : <br />   well_founded ltA -&gt;<br />   forall x, <br />    Acc ltA x -&gt;<br />    forall y, <br />     Acc ltA y -&gt; <br />     Acc lexprod (x, y).<br />  Proof.<br />   intros H x Hx.<br />   induction Hx as [x _ IHacc].<br />   intros y Hy.<br />   induction Hy as [y _ IHacc0].<br />   apply Acc_intro.<br />   intros (x1, y1).<br />   inversion 1; subst; auto.<br />  Qed.<br /><br />  Theorem wf_lexprod :<br />   well_founded ltA -&gt;<br />   well_founded lexprod.<br />  Proof.<br />   intros wfA ; unfold well_founded.<br />   intros (x, y); auto using acc_A_lexprod.<br />  Qed.</p><p>

With this definitions, we can easily define an well founded relation for pairs of natural numbers using:

</p><p>Definition lt2 := lexprod nat lt.<br /><br />Lemma wf_lt2 : well_founded lt2.<br />Proof.<br />  unfold lt2 ; auto using wf_lexprod with arith.<br />Qed.</p><p>

Mission accomplished! We these simple definitions we can define a well founded relation over products of a given type and its well founded relation. Ok, ok… the presentation isn’t in a tutorial style since, I believe, it has a very specific audience.

But why should I care about well founded relations? The reason is simple: Well founded relations can be used to prove termination of programs in Coq proof assistant. A topic that I will discuss in another post.

 

 

 

 

Últimas leituras, trabalho e estudos…

dezembro 10, 2011

Faz muito tempo que não posto nada neste blog. Estou deveras atarefado em meu doutorado e com meu trabalho na universidade. Grande parte deste trabalho envolveu o estudo e utilização do assistente de provas Coq. Em um próximo post, escreverei sobre este assistente de provas.

 

Leituras

 

Nos últimos meses li dois livros interessantíssimos:

  1. Notas do subsolo de Dostoevsky. Este livro, é um grande monólogo que mostra um homem incapaz de conviver com a realidade que o cerca, e por isso, vive no “subsolo”, à margem da sociedade. Na minha opinião é um excelente livro e vale a leitura, pela análise psicológica feita neste romance.
  2. Caim de José Saramago. Era enorme a minha curiosidade em relação a este livro por diversas razões. Em primeiro lugar, logo que ouvi falar, que Saramago iria lançar um novo romance cujo nome era “Caim”, previ, tal como com o “Evangelho segundo Jesus Cristo” polémica acrescida para além da que já é mais ou menos habitual em relação aos livros de Saramago. Mais uma vez iria mexer com a instituição Igreja; pelo menos assim dava a entender o título… Este livro começa com Adão e Eva no Jardim do Eden e a sua expulsão. Vai continuando em toada ligeira, eivada de humor, até à morte de Abel às mãos de Caim. Este, personagem central, vai-nos conduzindo no seu vaguear pelo mundo, pelos diversos “presentes” com que se vai deparando. Esses presentes não são mais do que episódios diversos, ligeiramente ficcionados, em que as personagens são as da própria bíblia, alvos de grande análise crítica e, atrever-me-ei mesmo a dizer novamente, de sentido de humor, que nos são narrados no Antigo Testamento. Todos eles revelam um deus caprichoso, intolerante, déspota e cruel, como qualquer pessoa que leia este documento considerado histórico (é através do Antigo testamento que ainda hoje se interpretam os vestígios arqueológicos da Mesopotâmia e se dá corpo a aspectos da sua História), sem o halo da crença, também o verá. Por fim, este é um livro polêmico para crentes. Evidentemente, recomendo a sua leitura.

Os próximos livros a serem lidos são o Andar do Bêbado — livro sobre a teoria de probabilidades — e os Três Mosqueteiros de Alexandre Dumas.

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.

Dicas de como escrever bem…

abril 25, 2011

Todos os dias acesso o site planet haskell, que todos os dias publica artigos sobre Haskell, lógica e matemática. Esta manhã fui supreendido com um artigo relatando sete regras de um vencedor de um prêmio Nobel de literatura de como escrever bem. Diante disso não pensei duas vezes e resolvi traduzir na íntegra estas sete dicas.

  1. Não escreva frases longas. Cada frase não deve ter mais que dez ou doze palavras.
  2. Cada sentença deve possuir um significado claro e deve adicionar algo às sentenças previamente realizadas. Um bom parágrafo é uma série de frases claras e ligadas entre si.
  3. Não use palavras grandes. Se seu editor de texto diz que o comprimento médio de palavras de seu texto é maior que cinco, algo está errado. Usar palavras curtas nos faz pensar sobre o que estamos escrevendo. Mesmo idéias complicadas podem ser quebradas em uma série de pequenas palavras.
  4. Não use palavras que você não possui certeza de seu significado.
  5. Evite usar adjetivos e advérbios.
  6. Evite ser abstrato. Seja objetivo e concreto.
  7. Pratique sua escrita todos os dias utilizando as regras anteriores durante pelo menos 6 meses.

Escrever bem é uma arte que por sinal, deveria ser dominada por todos.

Leituras…

abril 23, 2011

Tenho estado bastante ocupado com atividades administrativas na universidade, quase não estou tendo tempo para dedicar ao meu doutorado ou a leituras. Já deve fazer mais de um mês que terminei o livro “O guia do mochileiro das galáxias”, de Douglas Adams. Recomendo. O livro é extremamente engraçado com piadinhas bem interessantes envolvendo física, lógica e outros ramos da ciência.

No presente momento estou tentando terminar de ler “O restaurante no fim do universo”, também de Douglas Adams, mas o tempo está curto.

Vou torcer para esta maré de trabalho excessivo passe logo…

Efeitos Colaterais em Haskell

abril 23, 2011

Ser puro ou impuro? Eis a questão!

Atualmente a comunidade de pesquisa em linguagens funcionais debate incessantemente sobre o tema de qual a melhor maneira de manipular efeitos (estado, I/O, logging, continuações, …) .  Existem duas correntes principais:

  • Linguagens funcionais “puras”, como Haskell, que são baseadas na noção matemática de que uma função consiste no simples mapeamento de seus argumentos em seus respectivos resultados.
  • Linguagens funcionais impuras, como ML, que estendem esta noção com “efeitos” como atribuições, exceções, etc.

Linguagens puras são mais simples, por permitirem que raciocínio algébrico padrão da matemática seja utilizado em seus programas sem maiores problemas (o que facilita a prova de corretude de programas) . Além disso, essas linguagens permitem a utilização de avaliação sobre demanda. Porém linguagens impuras tendem a ser mais eficientes.

Diante de tal impasse, na década de 90 iniciaram-se diversas pesquisas visando integrar as abordagens puras e impuras, utilizando o conceito matemático de mônadas. Neste post, irei apresentar como mônadas podem ser utilizadas para permitir o desenvolvimento de programas effect-ivos (programas com efeitos) em Haskell.

Reutilizando padrões de computação

Mônadas são um exemplo de uma idéia recorrente em computação de reutilizar padrões de programas. Antes de considerarmos mônadas, vamos rever como podemos reutilizar padrões de computação em linguagens funcionais, utilizando dois exemplos simples:

   inc :: [Int] -> [Int]
   inc [ ] = [ ]
   inc (x:xs) = (x + 1) : inc xs

   sqr :: [Int] -> [Int]
   sqr [ ] = [ ]
   sqr (x:xs) = x ^ 2 : sqr xs

É simples observar que  as funções anteriores possuem a mesma estrutura, ambas quando aplicadas a uma lista vazia a retornam e quando a lista é não vazia, aplicam uma função à cabeça desta lista e repetem o processo para a cauda desta lista. A reutilização de tal padrão de computação nos leva a função map, presente na biblioteca de Haskell:

    map :: (a -> b) -> [a] -> [b]
    map f []     = []
    map f (x:xs) = f x : map f xs

Utilizando map, as duas funções anteriores podem ser descritas de maneira mais compacta:

    inc = map (+1)
    sqr = map (^2)

Avaliando expressões aritméticas

Sem sombra de dúvida, o exemplo mais utilizado para mostrar o poder de linguagens funcionais é a codificação de interpretadores de alguma linguagem. Considere, a seguinte linguagem simples de expressões que é constituída de constantes inteiras e um operador de divisão:

   data Expr = Val Int | Div Expr Expr

A função que avalia tais expressões possui uma implementação direta:

  eval :: Expr -> Int
  eval (Val n) =  n
  eval (Div x y) =  eval x `div` eval y

Porém,esta função não leva em consideração a possibilidade de uma divisão por zero, e irá produzir um erro em tempo de execução neste caso. Para lidar com este problema de maneira simples, podemos utilizar o tipo de dados Maybe

data Maybe a = Nothing | Just a

para definir uma versão “segura” (isto é, que não causa erros em tempo de execução) da divisão:

safediv :: Int -> Int -> Maybe Int
safediv n m =  if m == 0 then Nothing else Just (n `div` m)

e então realizar as mudanças necessárias na função que interpreta as expressões, como mostrado no trecho seguinte:

eval :: Expr -> Maybe Int
eval (Val n)   =  Just n
eval (Div x y) =  case eval x of
                    Nothing -> Nothing
                    Just n   -> case eval y of
                                 Nothing -> Nothing
                                 Just m  -> safediv n m

Assim como na seção anterior, pode-se observar um padrão nesta definição: um casamento de padrão sobre um valor do tipo Maybe, mapeando valores Nothing neles próprios, e valores da forma Just x em algum resultado que depende de alguma maneira de x.

Mas como este padrão pode ser reutilizado? Uma abordagem seria observar que a chave de avaliar uma divisão é realizar um casamento de padrão sobre dois valores do tipo Maybe que resultam de avaliar ambos os argumentos da divisão. Sendo assim, pode-se definir uma função para abstrair este casamento de padrão:

seqn  :: Maybe a -> Maybe b -> Maybe (a,b)
seqn Nothing   _        =  Nothing
seqn _         Nothing  =  Nothing
seqn (Just x)  (Just y) =  Just (x,y)

Usando seqn pode-se definir a avaliação de expressões de maneira mais elegante e compacta:

eval (Val n)   = Just n
eval (Div x y) = apply f (eval x `seqn` eval y)
                 where f (n,m) = safediv n m

A função apply é uma simples aplicação par ao tipo Maybe e é usada para processar o resultado de duas avaliações:

apply :: (a -> Maybe b) -> Maybe a -> Maybe b
apply f Nothing  =  Nothing
apply f (Just x) =  f x

Tudo parece muito bom! Porém a função seqn pode tornar o código uma “baderna”  se tentarmos manipular tuplas aninhadas.  Suponha, como exemplo, que nossa linguagem de expressões possuísse suporte a operadores de três argumentos. A avaliação de tal operador é apresentada no trecho de código seguinte:

eval (Op x y z) = apply f (eval x `seqn` (eval y `seqn` eval z))
                  where f (a,(b,c)) = ...

Reutilizando sequenciamento e processamento

O problema de tuplas aninhadas pode ser evitado ao novamente observar que isso nada mais é que “um casamento de padrão sobre valores do tipo Maybe, que preserva valores da forma Nothing e transforma valores da forma Just x em algo que depende de x.” A reutilização deste padrão é feita pelo operador definido a seguir:

(>>=) :: Maybe a -> (a -> Maybe b) -> Maybe b
Nothing  >>= _ = Nothing
(Just x) >>= f = f x

Se o primeiro argumento é da forma Nothing, então o segundo argumento é ignorado e Nothing é retornado como resultado. Caso contrário, se o primeiro argumento é da forma (Just x), então o segundo argumento é aplicado a x para obter um resultado de tipo Maybe b. Simples, não?

O operador >= evita o problema do aninhamento de tuplas de resultados porque o resultado do primeiro argumento é disponibilizado diretamente para processamento pelo segundo, ao invés de aguardar um segundo resultado para ser processado posteriormente. Desta maneira, >>= integra o sequenciamento de valores de tipo Maybe com o processamento de valores resultantes de computações sobre esse tipo. Em Haskell, o operador >>= é muitas vezes denominado “bind” (vincular), pois o segundo argumento é vinculado ao resultado do primeiro. Observe que >>= é idêntico a função apply definida anteriormente, a menos de que seus argumentos são “trocados”.

Usando o operador >>=, a função que avalia expressões aritméticas pode ser reescrita como:

eval (Val n)   = Just n
eval (Div x y) = eval x >>= (\n -> eval y >>=
                        (\m -> safediv n m))

A equação para a divisão pode ser lida da seguinte maneira: avalie x e chame o resultado desta avaliação de n, então avalie y e chame seu resultado de m, e finalmente combine estes dois resultados usando a função safediv.

Podemos generalizar a estrutura deste pequeno exemplo para expressões quaisquer que utilizam o operador >>=. Essas expressões possuem a seguinte estrutura:

     m1 >>= \x1 ->
     m2 >>= \x2 ->
         ...
     mn >>= \xn ->
         f x1 x2 ... xn

Traduzindo esta definição para português simples: Avalie cada uma das expressões m1, m2, …, mn e combine os resultados de cada uma delas aplicando a função f.

A definição de >>= garante que tal expressão somente retorna um valor de forma Just se nenhum mi na sequência retorna Nothing. Em outras palavras, não é necessário o programador se preocupar com eventuais falhas (representado no exemplo, por retornar um valor Nothing) em cada uma das expressões envolvidas, pois o operador >>= cuida desta manipulação de maneira simples.

Tais expressões são tão comuns em Haskell, que a linguagem possui uma notação especial permitindo que essas sejam escritas de uma forma mais legível:

do
    x1 <- m1
    x2 <- m2
    ...
    xn <- mn
    f x1 x2 ... xn

Utilizando esta notação, pode-se reescrever o avaliador de expressões de maneira bem simples e legível:

eval (Val n)   = Just n
eval (Div x y) = do
                    n <- eval x
                    m <- eval y
                    safediv n m

Mônadas em Haskell

O uso da notação do não é restrita a valores do tipo Maybe, a única restrição sobre essa notação é que ela deve somente ser utilizada em computações envolvendo tipos que constituem uma mônada. O conceito de mônada vem de um ramo da matemática chamado de teoria das categorias. Para a utilização de mônadas em Haskell não é necessário entender este conceito matemático. Na prática, uma mônada em Haskell, é um tipo m que possui duas funções:

return :: a -> m a

(>>=)  :: m a -> (a -> m b) -> m b

Por exemplo, se considerarmos que m  = Maybe, temos que os tipos de return e >>= são:

return :: a -> Maybe a

(>>=)  :: Maybe a -> (a -> Maybe b) -> Maybe b

Com estas duas funções, temos nossa primeira mônada.

Haskell suporta a definição de funções sobrecarregadas utilizando classes de tipos. Uma classe de tipo é uma coleção de tipos que possuem uma determinada interface de funções sobrecarregadas definidas sobre estes.

Por exemplo, a classe Eq de tipos que permitem o teste de igualdade, pode ser declarado da seguinte maneira:

class Eq a where
    (==) :: a -> a -> Bool
    (/=) :: a -> a -> Bool

    x /= y = not (x == y)

A definição declara que para um tipo “a” ser uma instância da classe Eq , ele deve suportar os operadores de teste de igualdade / desigualdade com os tipos especificados. Devido ao fato da classe possuir uma definição padrão para o operador de desigualdade (/=), é necessário apenas definir a igualdade para o tipo em questão. Como um exemplo, podemos definir uma instância para o tipo Bool:

instance Eq Bool where
    False == False = True
    True  == True  = True
     _     == _      = False

A noção de mônada pode ser representada utilizando a seguinte declaração de classe:

class Monad m where
    return :: a -> m a
    (>>=)  :: m a -> (a -> m b) -> m b

Isto é, uma mônada é um tipo “m” que implementa as funções return e >>= dos tipos especificados. A definição de uma instância para o tipo Maybe:


instance Monad Maybe where
     return x       =  Just x

     Nothing  >>= _ =  Nothing
     (Just x) >>= f =  f x

Agora que definimos esta instância para o tipo Maybe, podemos utilizar a notação do para computações envolvendo este tipo. Todo tipo que é instância da classe Monad, pode ser utilizado com a notação do.

A mônada de listas

A mônada de Maybe provê um simples modelo de computações que podem falhar, no sentido de que um valor de tipo Maybe é da forma Nothing, que pode ser pensado como uma falha, ou possui a forma Just x para algum x de tipo a, que pode ser entendido como um sucesso. A mônada de listas generaliza esta noção, permitindo múltiplos resultados no caso de sucesso.

Sendo mais preciso, um valor de tipo [a] ou é uma lista vazia [ ], que podemos ver como uma falha, ou possui a forma de uma lista não vazia [x_1, x_2, ..., x_n] para algum x_i de tipo a, que pode ser visto como o sucesso. De certa maneira, uma mônada de lista pode ser utilizada para modelar computações não determinísticas, onde mais de um resultado é produzido a cada passo. A definição de uma lista como sendo uma mônada é direta:

instance Monad [ ] where
    return x  =  [x]
    xs >>= f  =  concat (map f xs)

(Nota: Nesta definição, [ ] representa um tipo lista sem seu parâmetro a ). A função return simplesmente converte um valor qualquer em um resultado contendo este valor, enquanto >>= fornece uma maneira de sequenciar computações que podem retornar mais de um resultado: xs >>= f aplica a função f a cada um dos resultados da lista xs produzindo, assim, uma lista de listas de resultados que é posteriormente concatenada para formar uma única lista contendo todos os resultados.

Como exemplo da utilização da mônada de listas, uma função que retorna todas as maneiras de combinar pares de elementos de duas listas pode ser definida utilizando a notação do da seguinte maneira:

pairs     :: [a] -> [b] -> [(a,b)]
pairs xs ys =  do
                 x <- xs
                 y <- ys
                 return (x,y)

Isto é, considere cada possível valor x da lista xs, e cada valor y da lista ys, e retorne o par (x,y). Observe a definição da função pairs utilizando list comprehension:

pairs xs ys = [(x,y) | x <- xs, y <- ys]

Na verdade, list comprehensions e a notação do para listas são equivalentes. Ambas notações são maneiras diferentes de se utilizar o operador >>= para listas.

A mônada de estado

Agora consideremos o problema de implementar funções que manipulam algum tipo de estado, representado por um tipo cujos detalhes internos podemos, por agora, ignorar. Pode-se considerar que este tipo possui a seguinte forma:

type State = ...

A mais básica função sobre um estado é o que chamamos de “transformador de estado” (abreviado como ST , do inglês state transformer), que recebe como parâmetro o estado atual, e produz um estado possivelmente modificado e um resultado.

type ST a = State -> (a, State)

A figura a seguir ilustra a aplicação de tal função a um estado s, produzindo um novo estado s’ e um resultado v.

Transformador de estado

Um transformador de estados pode receber argumentos adicionais. Todavia, não é necessário alterar o tipo ST, porque este comportamento pode obtido por currying. Por exemplo, um transformador de estados que recebe um caractere (Char) e retorna um inteiro (Int) possui o tipo Char -> ST Int, que é uma abreviação para Char -> State -> (Int, State). Isto pode ser representado graficamente por:

Retornando às mônadas, é fácil observar que ST constitui uma mônada de simples definição:

 instance Monad ST where
    return x  =  \s -> (x,s)
    st >>= f  =  \s -> let (x,s') = st s in f x s'

Isto é, return converte um valor em um transformador de estado que apenas retorna aquele valor sem modificar o estado. Graficamente:

Visão diagramática da função return

Por sua vez, (>>=) provê uma maneira de sequenciar transformadores de estados: st >>= f aplica o tranformador de estado st a um estado inicial s, então aplica a função f ao resultado x para produzir um segundo transformador de estado (f x), que é então aplicado ao novo estado s’ para produzir o resultado final. Graficamente:

Sequenciando transformadores de estado

Perceba que return poderia ser definido como:

return x s = (x,s)

Todavia, a definição anterior é preferida por ocultar o parâmetro de estado s. Um pequeno detalhe sobre a instância para a mônada ST definida anteriormente: Haskell não permite a definição de instâncias para sinônimos de tipos. Portanto, podemos definir o tipo ST da seguinte forma alternativa (mas equivalente):

newtype ST a = ST { runST :: State -> (a, State) }

A definição da mônada ST pode ser feita da seguinte maneira:

instance Monad ST where
    return x   = ST (\s -> (x,s))
    st >>= f   = ST (\s -> let
                             (x,s') = runST st s
                           in runST (f x) s')

Mônada de estado: Um Exemplo

Como um simples exemplo de utilização de uma mônada de estado, vamos considerar a tarefa de rotular cada nó de uma árvore binária com um número inteiro que o identifica unicamente. Para isso, será necessário definir um tipo de dados para árvores binárias:

data Tree a = Leaf a | Node (Tree a) (Tree a)

Segue um pequeno exemplo de uma árvore:

tree :: Tree Char
tree =  Node (Node (Leaf 'a') (Leaf 'b')) (Leaf 'c')

Agora iremos considerar nosso problema original: de rotular cada nó com um número inteiro correspondente ao valor deste nó. Primeiramente, deve-se definir o tipo do estado a ser manipulado. Como o objetivo é adicionar um número inteiro para cada nó da árvore, toda vez que passarmos por um nó devemos “incrementar nosso” contador, que representa o estado a ser manipulado. Portanto, nada mais natural que definir o estado como sendo um número inteiro:


type State = Int

Considerando que o estado armazenado seja um número inteiro e que a cada nó visitado o estado deve ser atualizado com o sucessor deste número, temos que implementar um transformador de estado que retorna o estado atual como seu resultado e incrementa este número para formar o novo estado. Isto é:

fresh :: ST Int
fresh =  S (\n -> (n, n+1))

Usando esta função e as funções monádicas para ST fica fácil definir uma função que recebe uma árvore como argumento e retorna um transformador que produz a mesma árvore onde cada nó é rotulado com um inteiro:

mlabel :: Tree a -> ST (Tree (a,Int))
mlabel (Leaf x)   =  do
                       n <- fresh
                       return (Leaf (x,n))
mlabel (Node l r) =  do
                       l' <- mlabel l
                       r' <- mlabel r
                       return (Node l' r')

Observe que não é necessário que o programador se preocupe com a tarefa tediosa e propensa a erros de lidar com a criação de novos rótulos para cada componente da árvore, já que isso é diretamente manipulado pela mônada de estado!

Tendo este transformador de estado em mãos, podemos definir uma função que rotula uma árvore simplesmente aplicando o transformador tendo o inteiro 0 como estado inicial e descartando o estado final.

label  :: Tree a -> Tree (a,Int)
label t = fst (apply (mlabel t) 0)

A aplicação da função label à árvore tree resulta em:

Node (Node (Leaf ('a',0)) (Leaf ('b',1))) (Leaf ('c',2))

A mônada de I/O

Programas interativos em Haskell são escritos utilizando o tipo IO a que retorna um valor de tipo a, mas pode realizar alguma entrada / saída. A biblioteca Prelude possui diversas funções para construir valores de tipo IO:

return  :: a -> IO a
(>>=)   :: IO a -> (a -> IO b) -> IO b
getChar :: IO Char
putChar :: Char -> IO ()

Veja só… o tipo IO  possui as funções return  e (>>=), o que quer dizer que o tipo IO é uma mônada, e portanto, podemos utilizar a notação do para escrever programas interativos. Como exemplo, considere a seguinte função que lê uma sequência de caracteres a partir do teclado:

getLine :: IO String
getLine = do
            x <- getChar
            if x == '\n' then []
              else do
                    xs <- getLine
                    return (x:xs)

É interessante notar que a mônada de IO pode ser interpretada como um caso especial de uma mônada de estado, na qual o estado interno da mônada representa o estado de “todo o mundo”:

type World = ...
type IO a  = World -> (a,World)

Isto é, uma ação (um valor de tipo IO a) pode ser visto como uma função que recebe o estado atual do mundo como seu argumento, e produz um valor e este estado possivelmente modificado (refletindo possíveis resultados de entrada e saída executados pela ação). Internamente, o compilador GHC utiliza uma representação similar a esta para codificar valores de tipo IO.

Conclusão

Este post foi extenso, mas serviu apenas para “arranhar” o tópico sobre mônadas e programação funcional. Como o tema é deveras extenso, não é possível abordar todas as nuances deste. Recomendo os seguintes artigos, para leitores que desejam aprofundar seus conhecimentos:

  1. The Essence of Functional Programming – Philip Wadler
  2. Monadic Parsing Combinators – Graham Hutton

Além disso tem havido interesse em arrows  e funtores aplicativos que são generalizações de mônadas. Referências sobre estes temas são

  1. Generalizing monads to arrows – John Hughes
  2. Applicative Programming with Effects – Connor McBride.

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.

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…

 


Seguir

Obtenha todo post novo entregue na sua caixa de entrada.