Τελευταία ενημέρωση: 26/11/2007

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

Β' εξάμηνο 2005-2006, Διδάσκοντες: Γιώργος Κολέτσος & Γιώργος Σταυρινός

Πληροφορίες:
Γιώργος Κολέτσος, e-mail: koletsos AT math DOT ntua DOT gr
Γιώργος Σταυρινός, e-mail: g.stavrinos AT math DOT ntua DOT gr
ιστοσελίδα: http://www.math.ntua.gr/logic/proof-theory/lcalc.htm

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

  1. Καθαρός λ-λογισμός.
  2. λ-λογισμός με τύπους.
  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. Χ. Χαρτώνας, "Λογισμοί λ", Εκδόσεις Ζήτη, 2000.
  5. K.H. Rose, "Explicit substitution - tutorial & survey", BRICS Lecture Series, 1996.
  6. J.R. Hindley, "Basic Simple Type Theory", Cambridge University Press, 1997.
  7. C. Hankin, "Lambda Calculi", Clarendon Press, 1994.
Σχετικές ιστοσελίδες: