Lambda-Cálculo e Lógica Combinatória
2012.2
Ementa e Programa
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.
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
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.
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.
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
07 Dez
Lambda cálculo: conversão, redução, Church-Rosser
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
16 Jan
Lógica Combinatória: Termos, Conversão, Igualdade
18 Jan
Lógica Combinatória: Termos, Conversão, Igualdade (Cont.)
23 Jan
O Poder do Lambda e dos Combinadores
25 Jan
Representando as Funções Recursivas
(Cap. 7 do livro de van Dalen)
30 Jan
Representando as Funções Recursivas (cont.)
01 Fev
Termos tipados
06 Fev
Atribuição de tipos em lógica combinatória
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
Última atualização: 12 Dezembro 2012, 10:09am GMT-3