Sumários
20 Fevereiro, 11h00
Apresentação da disciplina, método de avaliação e equipa docente.
Aulas Téoricas
27 Fevereiro, 11h00
Revisões de conceitos básicos de programação funcional: programas, tipos, linguagens, estado, execução estrita e lazy,
Introdução ao cálculo de programas funcionais.
2 Março, 15h00
Continuação do assunto da aula anterior: funções; assinaturas; aplicação de funções; igualdade extensional de funções; composição de funções; funções-identidade; funções constante.
Introdução do conceito de diagrama comutativo. Polimorfismo e famílias de funções indexadas por tipos. Propriedades: associatividade da composição; identidade como elemento neutro da composição; fusão de funções-constante.
Isomorfismos: definição; interpretação ao nível dos tipos de dados.
6 Março, 11h00
Tipos-produto. Funções de projecção. O combinador split: definição e propriedades: cancelamento, fusão, reflexão. O combinador produto de funções. Propriedades functoriais e de absorção.
9 Março, 15h00
Tipos-coproduto. Funções de injecção. O combinador either: definição e propriedades: cancelamento, fusão, reflexão. O combinador soma de funções. Propriedades functoriais e de absorção.
13 Março, 11h00
Os isomorfismos swap e assocr/assocl. Exemplos de provas no cálculo com produtos e coprodutos. Conversão de expressões do cálculo em expressões de uma linguagem funcional com variáveis (vulgo conversão pontwise – pointfree).
16 Março, 15h00
Propriedades universais dos tipos produto e coproduto. Derivação das leis equacionais estudadas em aulas anteriores. Lei da troca. Guardas e o Condicional de McCarthy.
20 Março, 11h00
Tipos-exponenciação. Função de aplicação. O combinador curry: definição e propriedades: cancelamento, fusão, reflexão. O combinador exponenciação de funções. Propriedades functoriais e de absorção.
23 Março, 15h00
Produtos e coprodutos finitários. Tipos de dados elementares: 0 e 1; isomorfismos envolvendo estes tipos. Tipos da forma 1+A. Os tipos 2 e n.
27 Março, 11h00
Tipos de dados indutivos. Álgebras e Coálgebras. Caracterização equacional de tipos recursivos. Resolução de equações de tipo recursivas.
3 Abril, 11h00
Continuação do assunto da aula anterior; soluções abstractas e concretas para equações recursivas de tipos de dados. Soluções isomorfas.
Functores: definição; exemplo: functores de tipo.
10 Abril, 11h00
Functores constante e identidade. Functor exponenciação. Noção de bifunctor. Bifunctores produto e coproduto. Pontos fixos de functores; functor-base de um tipo de dados recursivo. "Lifting" do produto e coproduto para functores; definição de functor polinomial. Normalização de functores polinomiais.
20 Abril, 15h00
Tipos como pontos fixos de functores. Introdução aos catamorfismos: catamorfismos de listas. Exemplos.
24 Abril, 11h00
Catamorfismos genéricos. Propriedade Universal. Propriedades de Cancelamento e Reflexão. Exemplos: Catamorfimos de Árvores Binárias etiquetadas nos nós e nas folhas.
27 Abril, 15h00
Anamorfismos Genéricos. Propriedade Universal. Propriedades de Cancelamento e Reflexão. Anamorfismos de listas.
4 Maio, 15h00
Continuação do assunto da aula anterior. Exemplos: Anamorfismos de Árvores Binárias etiquetadas nos nós e nas folhas.
8 Maio, 11h00
Noção de Hilomorfismo. Hilomorfismos genéricos; hilomorfismos de listas. Lei de deflorestação de hilomorfismos. Exemplos de hilomorfismos: função factorial; algoritmo de ordenação merge-sort.
11 Maio, 15h00
Exemplos de hilomorfismos: algoritmo de ordenação quicksort. Programação com hilomorfismos: uma arquitectura para a construção de algoritmos. Exemplo: obtenção de novas funções por alteração do anamorfismo e do catamorfismo da função quicksort.
29 MAIO, 11H00
Conversão sistemática de código com variáveis em código point-free. Exemplos de aplicação.
1 JUNHO, 15H00
Conclusão do programa da disciplina. Catamorfismos de ordem superior. Considerações finais sobre domínios semânticos: conjuntos e CPOs. Implicações da escolha de uma semântica concreta sobre os tópicos estudados em vários pontos do programa.