Cálculo pointfree

[20_LESI]

Boas! Estou a fazer um trabalho sobre a cadeira de Cálculo de Programas (antiga MP1) na Universidade do Minho. Quem lá esteve, sabe que não é pêra doce...

Eis a parte que interessa do enunciado:

O objectivo do projecto deste ano é desenvolver um programa capaz de automatizar o cálculo de programas no estilo point­free. Mais especificamente, dada uma quação para demonstrar, o programa deverá listar a sequência de passos necessária para efectuar a respectiva prova. Por exemplo, caso se pretenda demonstrar que

swap . swap = id, o programa poderá gerar o seguinte resultado:

    swap . swap = id

<=> { Def-swap }

    (snd /\ fst) . (snd /\ fst) = id

<=> { Fusion-prod }

    snd . (snd /\ fst) /\ fst . (snd /\ fst) = id

<=> { Cancel-prod }

    fst /\ snd = id

<=> { Reflex-prod }

    id = id

Dado que a mesma prova pode ser efectuada de muitas formas distintas, é natural que o resultado apresentado pelo vosso programa para este exemplo seja ligeiramente diferente. Para obter aprovação no projecto, o programa deverá ser capaz de resolver automaticamente todas as alíneas da pergunta 3 da Ficha 2 (para além do exemplo acima).

Mais info aqui: http://wiki.di.uminho.pt/twiki/bin/view/Education/CP/

Em material de apoio está o formulário que precisamos de implementar, bem como as fichas

Já defini as leis que são precisas para resolver as alíneas mencionadas, e penso que estão a funcionar (quase) todas bem. Defini uma função que as aplica a todas, mas queria poder sair desta função logo após encontrar uma lei que possa ser aplicada à expressão. Não estou a conseguir fazer isso... Aqui deixo o código dessa função:

-- Simplificar uma expressão
simplifica :: Exp -> [Exp] -> [Exp]
simplifica e1 l = let x1  = aplicaregra fusaoX (last l) l
                               x2  = aplicaregra defX (last x1) x1
                               x3  = aplicaregra fusaoX (last x2) x2
                               x4  = aplicaregra cancelX (last x3) x3
                               x5  = aplicaregra assocO (last x4) x4
                               x6  = aplicaregra defX (last x5) x5
                               x7  = aplicaregra natId (last x6) x6
                               x8  = aplicaregra reflexX (last x7) x7
                               x9  = aplicaregra natFst (last x8) x8
                               x10 = aplicaregra absorX (last x9) x9
                               x11 = aplicaregra functorX (last x10) x10
                               x12 = aplicaregra natSnd (last x11) x11
                               x13 = aplicaregra natId (last x12) x12
                          in x13

-- Aplicar uma regra à última expressão da lista de expressões que contém a prova
aplicaregra :: (Exp -> Exp) -> Exp -> [Exp] -> [Exp]
aplicaregra lei ex l = let res = lei ex
	       in if (res == ex) then l
		                 else l++[res]

e a definição de Exp:

data Def = Exp:=:Exp

deriving (Read,Eq)


data Exp = Id

         | Exp:.:Exp    		--composiçao

 | Fst

 | Snd

 | Exp:/\:Exp   		--split

 | Exp:><:Exp    		--produto

	 | Func String

 | Num Int

deriving (Read,Eq)

Como podem ver, repito leis. O motivo é o mesmo pelo qual abri esta thread: faça eu o que fizer, não consigo sair da função simplifica quando alguma lei surte efeito. Penso que este seja um problema rápido de resolver, mas estou mesmo enferrujado em haskell...

[Rui Carlos]

Sugestão: cria uma função que recebe uma expressão e uma lista de leis, e depois vai tentando aplicar cada uma das leis, até que alguma altere a expressão original (i.e., tenta aplicar leis até que obtenhas um output diferente do input).

Acho que essa função que aplica uma sequência de regras rígida, não faz qualquer sentido, mas também não percebi o quão genérico terá que ser o programa.

[20_LESI]

Sugestão: cria uma função que recebe uma expressão e uma lista de leis, e depois vai tentando aplicar cada uma das leis, até que alguma altere a expressão original (i.e., tenta aplicar leis até que obtenhas um output diferente do input).

Acho que essa função que aplica uma sequência de regras rígida, não faz qualquer sentido, mas também não percebi o quão genérico terá que ser o programa.

A tua ajuda fui útil, e mostrou o quão enferrujado eu estou em Haskell... Fiz isto, mas empanquei:

-- Simplificar uma expressão
simplifica :: [string] -> Exp -> [Exp] -> [(Exp,String)]
simplifica [] exp prova    = prova
simplifica (h:t) exp prova = let l = (aplicaregra h (last prova) prova)

Estou a pensar retornar uma lista de pares, contendo cada par a expressão e a regra que usei para atingir tal expressão.

O que não consigo fazer:

-> um if dentro do let que me permita comparar a lista antes de aplicar a regra, e após a aplicação desta, para saber se a regra teve ou não, sucesso

[nata79]

para ver se a regra teve ou não successo podes por as regras a retornar um Maybe.

se der Just qq coisa é pq funcionou, se der Nothing não fez nd

[20_LESI]

para ver se a regra teve ou não successo podes por as regras a retornar um Maybe.

se der Just qq coisa é pq funcionou, se der Nothing não fez nd

Isso não é monádico? Ando a evitar monads ao máximo...

Já descobri como usar aqui a construçao let ... in:

-- Simplificar uma expressão
simplifica :: [string] -> Exp -> [Exp] -> [(Exp,String)]
simplifica [] exp prova    = prova
simplifica (h:t) exp prova = let l = (aplicaregra h (last prova) prova)
                                            in if( l \= (last prova) ) then (l,h)
                                                else simplifica t exp prova

Isto deve funcionar...

[nata79]

acho que não tem nd a ver com isso... pelo menos eu n faço ideia do que são monads...

[Rui Carlos]

Alguma razão para evitar monads?

Se te incomoda o facto de Maybe ser um monad, cria um tipo do género:

date NomeDoMeuTipo a= Value a | Null

Isto é exactamente a mesma coisa que o Maybe, só que não é um monad (a menos que tu queiras) 🙂

[Baderous]

Isso não é monádico? Ando a evitar monads ao máximo...

http://haskell.org/ghc/docs/latest/html/libraries/base/Data-Maybe.html#t%3AMaybe

[20_LESI]

Alguma razão para evitar monads?

Se te incomoda o facto de Maybe ser um monad, cria um tipo do género:

date NomeDoMeuTipo a= Value a | Null

Isto é exactamente a mesma coisa que o Maybe, só que não é um monad (a menos que tu queiras) 🙂

O problema é que o uso de monads complica bastante programar em haskell... Tenho essa vaga ideia, de quando fiz PP1 há dois anos e pouco! Do Maybe em concreto só me lembro mesmo de que era o mais fácil, tal como dá para ver pela tua definição xD

Isto já compila, mas ando às cabeçadas com a lista de leis lol. Quando tiver uma dúvida concreta, venho aqui postar! Obrigado a todos

[Rui Carlos]

Não, o problema é mesmo vos ensinarem a pensar que o uso de monads é complicado...

O monads não são necessariamente complicados. Infelizmente, no meu caso, só no 3º ano (e apenas numa aula) é que me ensinaram a usar monads de uma forma simples. Até aí, também achava os monads complicados.

[20_LESI]

Se calhar... Mas eu raramente fui às aulas de PP1. Estudei por mim, e fui tirando dúvidas na net. Quando tive que usar monad IO para o trabalho cheguei a pensar que não ia conseguir entregar a tempo...  Mas lá me safei...

[20_LESI]

Tenho estas definições no meu código:

instance Show Exp where
show (a :.: b) = show a ++ "." ++ show b
show (Fst) = "fst"
show (Snd) = "snd"
show (e1 :/\: e2) = "(" ++ show e1 ++ " /\\ " ++ show e2 ++ ")"
show (e1 :><: e2) = "(" ++ show e1 ++ " >< " ++ show e2 ++ ")"
show (Func x) = x
show (Num x)  = show x
show (Id) = "id"

type Prova = (Exp, (Exp -> Exp))

-- Função que transforma a lei numa string que contém o nome da string
traduzLei :: (Exp -> Exp) -> String
traduzLei inicio      = "inicio"
traduzLei absorX  = "absor-x"
traduzLei functorX = "functor-x"
traduzLei natFst    = "nat-Fst"
traduzLei natSnd  = "nat-Snd"
traduzLei cancelX  = "cancel-x"
traduzLei assocO  = "assoc-o"
traduzLei fusaoX  = "fusao-x"
traduzLei reflexX  = "reflex-x"
traduzLei natId      = "nat-id"
traduzLei defX      = "def-x"

Agora pretendo instanciar algo do tipo "Prova" para obter o seguinte output:

swap . swap = id

<=> { Def-swap }

(snd /\ fst) . (snd /\ fst) = id

<=> { Fusion-prod }

snd . (snd /\ fst) /\ fst . (snd /\ fst) = id

<=> { Cancel-prod }

fst /\ snd = id

<=> { Reflex-prod }

id = id

Mas não estou a conseguir! Não é possível fazer Show de types?

EDIT: Realmente parece não ter muita lógica fazer Show daquilo... Mas também não consigo fazer uma função que imprima isto...

[Rui Carlos]

Os types são apenas nomes alternativos para um outro tipo. No máximo poderias fazer Show para o tipo original (que normalmente já tem um Show).

[20_LESI]

Nã consigo pôr nada a funcionar porque tudo se queixa da falta de instanciação para o tipo (Exp -> Exp)... Quer seja para a classe Show, quer seja para a classe Eq...

Por exemplo:

    No instance for (Eq (Exp -> Exp))

O que posso fazer? Como sempre, o google não é grande ajuda no que a Haskell diz respeito...

EDIT: Fui obrigado a mudar de estratégia, pois esta além de mais difícil, era menos eficiente! Podem fechar a thread...