| Περίληψη: | Εισαγωγή στο λ-λογισμό. Η έννοια της αναγωγής και της κανονικοποίησης. Τα προγράμματα ως λ-όροι. Αναπαραστασιμότητα των συναρτήσεων. Στοιχειώδης προγραμματισμός. Ο λ-λογισμός ως πλαίσιο υπολογισμού ανάλογο των μηχανών Turing.<br/>Προγραμματισμός με τύπους, ο λ-λογισμός με τύπους. Το σύστημα των απλών τύπων, το σύστημα T του Gödel και το σύστημα F του Girard. Εκφραστικότητα των συστημάτων με τύπους. Αναδρομικές συναρτήσεις με απόδειξη τερματισμού.<br/>Περιγραφή του ισομορφισμού Curry-Howard. Οι φόρμουλες της λογικής ως τύποι της πληροφορικής και οι αποδείξεις μιας φόρμουλας ως προγράμματα αυτού του τύπου. Απόδειξη της ισοδυναμίας, η οποία διατηρεί ισομορφικά την κανονικοποίηση των προγραμμάτων και αντίστοιχα των αποδείξεων.
|
|---|
