Lambda-Cálculo e Lógica Combinatória

2015.2

Ementa e Programa


Instrutores: Ruy de Queiroz e Anjolina de Oliveira

Horário e Sala de Aula
2
a 08-10h, Sala E-113
4
a 10-12h, Sala E-113

Forum: lambda-l  @    cin.ufpe.br

Ementa: O lambda-cálculo. Estrutura de termos e substituição. Redução. Lógica Combinatória. Redução fraca. O Poder Expressivo de Lambda e dos Combinadores. O teorema do ponto-fixo. Representando as funções recursivas. O teorema da indecidibilidade. Lambda-cálculo com tipos. Isomorfismo de Curry-Howard.

Livro-Texto:


Outros recursos bibliográficos:

1. Lambda Calculi with Types, Henk Barendregt

2. Lambda-Calculus, Types and Models, by J.L. Krivine, Masson, Paris, 1993 (English xlation) ISBN 0-13-062407-1.

3. Introduction to Lambda Calculus, Henk Barendregt and Erik Barendsen

4. An introduction to lambda calculi and arithmetic, Harold Simmons. 

5. http://www.safalra.com/science/lambdacalculus/index.html 

6. On-line books, aulaure notes, etc (Lambda Calculus) 

7. Alonzo Church Papers 

8. Church, Alonzo, The calculi of lambda-conversion. Imprint: Princeton, Princeton University Press, 1941 [i.e. 1963]. (Series: Annals of mathematical studies, no. 6) 



Leitura adicional:

1. `Funktion und Begriff', Vortrag, gehalten in der Sitzung vom 9. Januar 1891 der Jenaischen Gesellschaft für Medizin und Naturwissenschaft, Jena: Hermann Pohle. Translated as `Function and Concept' by P. Geach in Translations from the Philosophical Writings of Gottlob Frege, P. Geach and M. Black (eds. and trans.), Oxford: Blackwell, third edition, 1980. 

2. Grundgesetze der Arithmetik, Jena: Verlag Hermann Pohle, Band I, 1893. Partial translation as The Basic Laws of Arithmetic by M. Furth, Berkeley: U. of California Press, 1964. Full translation as Gottlob Frege: Basic Laws of Arithmetic, 1st Edition, translated by Philip A. Ebert & Marcus Rossberg. Oxford University Press. December 2013. 680 pages. ISBN-13: 978-0199281749.


Calendário

24 Ago

Motivação: Church e o lambda calculus 

Frege e o `curso-de-valores') 


26 Ago

Visão geral do resultado original de Church

Termos lambda e combinadores: definições básicas

(Transparencia1) 


31 Ago

Lambda cálculo: conversão, redução, Church-Rosser

(Transparencia2) 


02 Set

Lambda cálculo: conversão, redução, Church-Rosser (cont.) 


09 Set

Lambda cálculo: conversão, redução, Church-Rosser (cont.) 


14 Set

Teorema de Church-Rosser para beta-redução

(Transparencia3)


16 Set

Lógica Combinatória: Termos, Conversão, Igualdade

(Transparencia4)


10 Out

Lógica Combinatória: Termos, Conversão, Igualdade (Cont.) 


15 Out

O Poder do Lambda e dos Combinadores

(Transparencia5)


17 Out

Representando as Funções Recursivas

(Transparencia6)

(Cap. 7 do livro de van Dalen) 


22 Out

Representando as Funções Recursivas (cont.)


24 Out

Termos tipados

(Transparencia7) 


29 Out

Atribuição de tipos em lógica combinatória

(Transparencia8) 


31 Out

Inferência de tipos


05 Nov

Tipos principais


07 Nov

Proposições como tipos: Curry-Howard


12 Nov

O teorema da indecidibilidade (cont.)


14 Nov

Axiomáticas lambda-beta e CLw


19 Nov

Modelos conjunto-teóricos do lambda-calculus


21 Nov

Modelos conjunto-teóricos do lambda-calculus (cont.)


26 Nov

Domínios


28 Nov

Ordens parciais completas


03 Dez

O modelo D-infinito


05 Dez

A Dialectica-interpretação de Gödel


Cursos anteriores


Última atualização: 24 Agosto 2015, 06:18pm GMT-3