Cálculo de Programas

Licenciatura em Engenharia Informática

Tópicos

Avisos

27 Set As notas da época especial foram publicadas na secção de funcionamento. O aluno que não preencheu o nome deve contactar pessoalmente o responsável da disciplina com a máxima urgência.

17 Jul O exame da época especial será no dia 21 de Setembro às 14h00 na sala 2206.

25 Jul As notas dos exames de recurso foram publicadas na secção de funcionamento. Os exames podem ser consultados na 3ª feira, dia 28 de Julho às 11h00 na sala DI 0.02. As orais para os alunos com notas de 8 e 9 serão no mesmo dia e sala às 14h00.

9 Jul A consulta dos testes será na sala DI 0.02.

Arquivo

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 equaçã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-x }
   snd . (snd /\ fst) /\ fst . (snd /\ fst) = id
<=> { Cancel-x }
   fst /\ snd = id
<=> { Reflex-x }
   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).

Extras

Para obter notas superiores a 16 poderá ser realizado algum dos seguintes extras:

  • Possibilidade de parametrizar o programa com a lista de leis a usar (enumeradas num ficheiro de acordo com uma sintaxe a definir).
  • Possibilidade de ajudar o programa nalgumas provas mais complexas. Por exemplo, sempre que a prova não pode prosseguir de forma óbvia, poderá ser dada a possibilidade ao utilizador de indicar manualmente qual a próxima lei a aplicar. Neste caso poderá ser útil implementar uma funcionalidade de undo, para permitir ao utilizador tentar uma lei diferente.
  • Inferência de tipos: determinar automaticamente o tipo de uma expressão. Esta funcionalidade poderia servir para alertar o utilizador caso o mesma introduza expressões semanticamente incorrectas, tais como fst . inl. Também poderá ser útil para detectar a possibilidade de aplicar certas leis: por exemplo, a lei universal do tipo 1 diz que qualquer função h :: a -> 1 pode ser imediatamente substituída por bang.
  • Conversão automática de definições point-free para o estilo pointwise.

Logística

O projecto deverá ser realizado em grupos de 2 alunos. Poderão usar a linguagem de programação que quiserem. O projecto deverá ser apresentado aos docentes nos dias 11 e 12 de Maio. Em princípio, também poderá ser apresentado numa das semanas anteriores em data a definir. A apresentação terá a duração de 30m. Para além do programa, deverão trazer para a apresentação um pequeno relatório onde descrevem sucintamente a estratégia que adoptaram para resolver este problema. Caso seja detectado plágio ou cópia, todos os grupos envolvidos ficarão imediatamente reprovados à disciplina, sem direito a qualquer recurso.

FAQ

O input para o programa vai ser uma string com a equação a provar?

Não necessariamente. A forma mais simples de resolver este problema consiste em representar a equação usando uma árvore de expressão (onde os nós representam combinadores e as folhas representam variáveis ou funções primitivas). Passar de uma string para esta árvore de expressão é um problema complicado (designado parsing), que só vai ser estudado com profundidade em Processamento de Linguagens no 3º ano. Assim sendo, admitimos que a equação seja passada ao programa directamente sob a forma de uma árvore. No entanto, o resultado da demonstração deve ser mostrado de forma semelhante à apresentada no enunciado. O parsing é precisamente um dos extras possíveis.

As 3 primeiras alíneas da pergunta 3 da Ficha 2 correspondem a leis do formulário. A prova consiste apenas na aplicação de uma lei?

Não. Tal como explicado nas aulas, não faz qualquer sentido provar uma lei usando a própria lei. Para ser um pouco mais preciso, o programa deve ser capaz de demonstrar todas as alíneas da pergunta 3 sem usar as leis Absor-x, Functor-x, e Functor-Id-x.

É mais fácil resolver este problema em Haskell ou em C?

Depende da vossa proficiência em cada uma das linguagens. Em ambas é relativamente simples representar árvores de expressão e implementar as funções básicas para manipular essas árvores. O mesmo se aplica a qualquer outra linguagem decente.

r4 - 24 Mar 2009 - 17:49:53 - AlcinoCunha
This site is powered by the TWiki collaboration platform Copyright © by the contributing authors. Ideas, requests, problems? Send feedback.
Syndicate this site RSSATOM