Lambda-Cálculo e Lógica Combinatória
2016.2
Ementa e Programa
Horário e Sala de Aula
2a 10-12h, Sala E-123
4a 08-10h, Sala E-123
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.
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)
8. Church, Alonzo, The calculi of lambda-conversion. Imprint: Princeton, Princeton University Press, 1941 [i.e. 1963]. (Series: Annals of mathematical studies, no. 6)
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.
08 Ago
Motivação: Church e o lambda calculus
Frege e o `curso-de-valores')
10 Ago
Visão geral do resultado original de Church
Termos lambda e combinadores: definições básicas
22 Ago
Lambda cálculo: conversão, redução, Church-Rosser
24 Ago
Lambda cálculo: conversão, redução, Church-Rosser (cont.)
29Ago
Lambda cálculo: conversão, redução, Church-Rosser (cont.)
31 Ago
Teorema de Church-Rosser para beta-redução
16 Set
Lógica Combinatória: Termos, Conversão, Igualdade
10 Out
Lógica Combinatória: Termos, Conversão, Igualdade (Cont.)
15 Out
O Poder do Lambda e dos Combinadores
17 Out
Representando as Funções Recursivas
(Cap. 7 do livro de van Dalen)
22 Out
Representando as Funções Recursivas (cont.)
24 Out
Termos tipados
29 Out
Atribuição de tipos em lógica combinatória
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
Última atualização: 05 Agosto 2016, 05:44pm GMT-3