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

2012.2

Ementa e Programa


Instrutores: Ruy de Queiroz e Anjolina de Oliveira

Horário e Sala de Aula
4a 08-10h, Sala A-010
6a 10-12h, Sala A-010

Rede Social: comunidade Lambda Cálculo 2012.2

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. An introduction to lambda calculi and arithmetic, Harold Simmons. 

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

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

4. Barendregt and Barendsen's shorter introduction to the lambda calculus 

5. Alonzo Church Papers 

6. Church, Alonzo, An unsolvable problem of elementary number theory, American Journal of Mathematics, 58 (1936), pp. 345.363. (This paper contains the proof that the equivalence of lambda expressions is in general not decidable.) 

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

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


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.


Calendário

05 Dez

Motivação: Church e o lambda calculus 

Frege e o `curso-de-valores') 


?? ???

Visão geral do resultado original de Church

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

(Transparencia1) 


07 Dez

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

(Transparencia2) 


12 Dez

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


14 Dez

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


19 Dez

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

(Transparencia3)


16 Jan

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

(Transparencia4)


18 Jan

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


23 Jan

O Poder do Lambda e dos Combinadores

(Transparencia5)


25 Jan

Representando as Funções Recursivas

(Transparencia6)

(Cap. 7 do livro de van Dalen) 


30 Jan

Representando as Funções Recursivas (cont.)


01 Fev

Termos tipados

(Transparencia7) 


06 Fev

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

(Transparencia8) 


15 Fev

O teorema da indecidibilidade


20 Fev

O teorema da indecidibilidade (cont.)


22 Fev

Axiomáticas lambda-beta e CLw


27 Fev

Modelos conjunto-teóricos do lambda-calculus


06 Mar

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


08 Mar

Domínios


13 Mar

Ordens parciais completas


15 Mar

A Dialectica-interpretação de Gödel


Cursos anteriores


Última atualização: 12 Dezembro 2012, 10:09am GMT-3