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

Lambda-Cálculo e Lógica Combinatória
2008.2
Ementa e Programa

Instrutores: Ruy de Queiroz e Anjolina de Oliveira

Horário e Sala de Aula
2^a 14-16, Sala D-001
4^a 16-18, Sala (a confirmar)

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:

Lambda-Calculus and Combinators: An Introduction

Introduction to Combinators and Lambda-Calculus

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

?? ???

Church

lambda calculus

curso-de-valores

?? ???
Visão geral do resultado original de Church
Termos lambda e combinadores: definições básicas
(Transparencia1)

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

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

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

05 Out
?? ???
Teorema de Church-Rosser para beta-redução
(Transparencia3)
(Lista2 a ser entregue em 12 Out)

08 Out
?? ???
Lógica Combinatória: Termos, Conversão, Igualdade
(Transparencia4)
(Lista3 a ser entregue em 19 Out)

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

19 Out
?? ???
O Poder do Lambda e dos Combinadores
(Transparencia5)
(Lista4 a ser entregue em 26 Out)

22 Out
?? ???
Representando as Funções Recursivas
(Transparencia6)
(Cap. 7 do livro de van Dalen)

26 Out
?? ???
Representando as Funções Recursivas (cont.)
(Lista5 a ser entregue em 05 Nov)

05 Nov
?? ???
Termos tipados
(Transparencia7)

?? ???
Atribuição de tipos em lógica combinatória
(Transparencia8)

?? ???
(no class)

?? ???
O teorema da indecidibilidade

?? ???
(no class)

?? ???
Axiomáticas lambda-beta e CLw

?? ???
Modelos conjunto-teóricos do lambda-calculus

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

?? ???
Domínios

?? ???
Ordens parciais completas

?? ???
A Dialectica-interpretação de Gödel

Cursos anteriores

Última atualização: 13 Agosto 2008, 04:49pm GMT-3