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.