Λ14.   λ-λογισμός
(ΜΠΛΑ, ΣΗΜΜΥ, ΣΕΜΦΕ)

Ωρολόγιο πρόγραμμα: Τρίτη 12:45-15:00,  αίθουσα 08, Πέμπτη 17:00-19:00, αίθουσα 013, Νέα κτήρια Ηλεκτρολόγων, ΕΜΠ

Πληροφορίες:
Γιώργος Κολέτσος, e-mail: koletsos AT math DOT ntua DOT gr

ιστοσελίδα: http://www.math.ntua.gr/logic/lambda

Περιγραφή:
Πρόκειται για μάθημα στο λ-λογισμό με κάποια έμφαση σε ζητήματα όπως ο καθαρός λ-λογισμός, τα μαθηματικά μοντέλα του, η συνδυαστική λογική, καθώς και ο λ-λογισμός με τύπους και η σχέση που έχει με τη λογική. Παρουσιάζει μεγάλο ενδιαφέρον για τους θεωρητικούς Πληροφορικούς και τους Μαθηματικούς καθώς έχει στενή σχέση με τις γλώσσες προγραμματισμού αλλά και για τη σύνδεση που εγκαθιστά μεταξύ της έννοιας του προγράμματος και της έννοιας της λογικής απόδειξης. Θα μπορούσε όμως να ενδιαφέρει και τους ασχολούμενους με τα θεμέλια των Μαθηματικών και την Επιστημολογία αφού αρχικά χρησιμοποιήθηκε για τη λογική θεμελίωση των Μαθηματικών.

1. Καθαρός λ-λογισμός.
• β-αναγωγή, η-αναγωγή, θεώρημα Church-Rosser.
• Αναπαράσταση των μερικών αναδρομικών συναρτήσεων στο λ-λογισμό, θεωρήματα σταθερού σημείου, θεώρημα αναποκρισιμότητας Scott-Curry.
2. λ-λογισμός με τύπους.
• Τυποποίηση των όρων του λ-λογισμού, το σύστημα Coppo-Dezani.
• Θεωρήματα της κανονικοποίησης, τυποποίηση κανονικοποιήσιμων όρων, πεπερασμένες αναπτύξεις, standard αναγωγή.
3. Θεώρημα του Bοhm, δέντρα του Bohm (αν υπάρχει χρόνος).
4. Συνδυαστική Λογική, ισοδυναμία με λ-λογισμό.
5. Μοντέλα του λ-λογισμού (κατασκευή του μοντέλου D_\infty του Scott).
6. Το σύστημα F του Girard.
7. Ρητές αντικαταστάσεις (αν υπάρχει χρόνος).

Βιβλιογραφία:

1. J.-L. Krivine, "Lambda-calcul, types et modeles", Masson, 1990. (Αγγλική μετάφραση: Ellis Horwood, 1993.)
2. H. Barendregt, "The lambda calculus", North Holland, 1984.
3. J.R. Hindley, J.P. Seldin, "Introduction to combinators and λ-calculus", Cambridge University Press, 1986.
4. Γ. Κολέτσος, Λογική και Πληροφορική ή Αποδείξεις και Προγράμματα, "Στιγμές και διάρκειες" (επιμ. Δ. Αναπολιτάνος), Εκδόσεις Νεφέλη, 2009
5. Χ. Χαρτώνας, "Λογισμοί λ", Εκδόσεις Ζήτη, 2000.
6. K.H. Rose, "Explicit substitution - tutorial & survey", BRICS Lecture Series, 1996.
7. J.R. Hindley, "Basic Simple Type Theory", Cambridge University Press, 1997.
8. C. Hankin, "Lambda Calculi", Clarendon Press, 1994.

Πρόχειρες προκαταρκτικές σημειώσεις: PDF

Εισαγωγικές σημειώσεις: PDF

Πρόχειρες χειρόγραφες σημειώσεις: PDF_1    PDF_2

Ασκήσεις

Σχετικές ιστοσελίδες:

• Henk Barendregt
• Jean-Louis Krivine
• Dana Scott
• Semantics and Logics of Computation
• Intersection Types and Related Systems
• Typed Lambda Calculi and Applications