Cálculo de Programas

LMCC - 2o. ano - 2005/06

Aulas Téoricas

Sumários

20 Fevereiro, 11h00

Apresentação da disciplina, método de avaliação e equipa docente. 

23 Fevereiro, 15h00 

Não houve aula. Motivo: simposium doutoral do DIUM.

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 pontwisepointfree).

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.

30 Março, 15h00

Não houve aula. Motivo: Presença do docente no workshop TERMGRAPH'06.

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.

6 Abril, 15h00

Não houve aula. Motivo: alunos não compareceram. 

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.

22 MAIO, 11H00

Lei de fusão dos catamorfismos. Exemplos: fusão de catamorfismos de listas.

25 MAIO, 15H00

Conversão de funções explicitamente recursivas em hilomorfismos. Casos de estudo.

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.

Departamento de informáticA UM