Λογική και Πληροφορική II: λ-λογισμός


Κωδικός 635
Εξάμηνο Εαρινό
Ώρες Διδασκαλίας - Ώρες Εργαστηρίου 4 - 0
Διδάσκοντες Γεώργιος Κολέτσος

Περιγραφή

Πρόκειται για μάθημα στο λ-λογισμό με κάποια έμφαση σε ζητήματα όπως ο κα¬θαρός λ-λογισμός, τα μαθηματικά μοντέλα του, η συνδυαστική λογική, καθώς και ο λ-λογισμός με τύπους και η σχέση που έχει με τη λογική, Ο λ-λογισμός είναι το αρχετυπικό σύστημα της ιδέας ότι τα προγράμματα είναι συναρτήσεις και ότι αυτό που τα προγράμματα υπολογίζουν είναι η κανονική μορφή του λ-ορού που τα αντιπροσωπεύει. Περιεχόμενα: Καθαρός λ-λογισμός, β-αναγωγή, η-αναγωγή, θεώρημα Church-Rosser. Αναπαράσταση των μερικών αναδρομικών συναρτήσεων στο λ-λογισμό, θεώρημα σταθερού σημείου, θεώρημα ανταποκρισημότητας Church, λ-λογισμός με τύπους. Τυποποίηση των όρων του λ-λογισμού, το σύστημα Coppo-Dezani. Τα θεωρήματα της κανονικοποίησης, τυποποίηση κανονικοποιήσιμων όρων. Το θεώρημα (και τα δέντρα του) του Bohm. Συνδυαστική Λογική, ισοδυναμία με λ-λογισμό. Μοντέλα του λ-λογισμού, κατασκευή του μοντέλου Doo του Scott. Το σύστημα F του Girard. Η απόδειξη του Goedel για τη συνέπεια της αριθμητικής.