Περιγραφή εβδομάδας

  • Γενικά

    Διδάσκων: Γιώργος Κολέτσος


    Έναρξη μαθήματος: 28/2/2023


    Διαλέξεις: Τρίτη 13:15-15:00, Τετάρτη 13:15-15:00, αιθ. 1.1.29, παλ. κτ. ΗΜΜΥ.


    Περιγραφή

    Η εφαρμογή των αφαιρετικών μεθόδων στα μαθηματικά, στο δεύτερο ήμισυ του 19 ου αιώνα

    (π.χ. Dedekind, Cantor), και η εμφάνιση των παραδόξων δημιούργησε τη λεγόμενη κρίση

    των θεμελίων. Η επιστήμη των μαθηματικών έγινε αντικείμενο μελέτης από τους

    μαθηματικούς και φιλοσόφους (Frege, Russell, Brouwer, Hilbert). Δημιουργήθηκαν σχολές

    στην προσπάθεια να ερμηνευτεί η φύση των μαθηματικών αλλά και να επιτευχθεί η

    στέρεη, χωρίς αντιφάσεις, θεμελίωσή τους. Η μελέτη των μαθηματικών θεωριών, τα

    λεγόμενα μεταμαθηματικά, γίνεται μέσω των τυπικών «εκπροσώπων» τους που είναι τα

    λογικά τυπικά συστήματα. Έτσι δημιουργείται και αναπτύσσεται η επιστήμη της

    μαθηματικής λογικής. Η συστηματική αυτή μελέτη οδηγεί στην ανακάλυψη των σχέσεων

    των συντακτικών μορφών και των ερμηνειών τους, των ορίων της αξιωματικής μεθόδου

    αλλά οδηγεί επίσης και στην ανακάλυψη μιας καινούργιας επιστήμης, της πληροφορικής

    που στο τυπικό επίπεδο αντιπροσωπεύεται από τις μηχανές Turing (το εκτελεστικό κομμάτι

    του υπολογισμού) και τον λάμβδα λογισμό του Church (την καταγραφή των

    προγραμμάτων). Οι δύο αυτές επιστήμες (λογική-μαθηματικά από τη μια και πληροφορική

    από την άλλη) συνυπάρχουν και αλληλοεπηρεάζονται έως ότου αποκαλύπτεται μια δομική

    σχέση που τις συνδέει, έως ισοδυναμίας-ταύτισης, ο ισομορφισμός Curry-Howard.

    Αποκαλύπτεται ότι κάθε απόδειξη αντιστοιχεί ισομορφικά σε ένα πρόγραμμα, η πρόταση

    που αποδεικνύεται αντιστοιχεί στον τύπο (specification) του προγράμματος, και η

    «απλοποίηση» της απόδειξης στην αποτίμηση (evaluation) του προγράμματος! Αρχικά ο

    ισομορφισμός καθιερώνεται μεταξύ της ιντουισιονιστικής (κατασκευαστικής) λογικής και

    της καθαρής αποτίμησης των συναρτησιακών προγραμμάτων αλλά αργότερα (Griffin 1990)

    εκπληκτικά επεκτείνεται και μεταξύ της κλασική λογικής και του προγραμματισμού με τη

    χρήση control operators και continuations. Η εις άτοπον απαγωγή, που είναι κλασικά αλλά

    όχι και κατασκευαστικά αποδεκτή, αντιστοιχεί σε προγραμματιστικές διαδικασίες τύπου

    abort!

    Το μάθημα θα είναι μια εισαγωγή στις κύριες πλευρές της θεωρίας αποδείξεων και της

    θεωρίας τύπων και προγραμμάτων (λ-λογισμός χωρίς ή και με τύπους) που σχετίζονται με

    τον ισομορφισμό Curry-Howard.


    Περιεχόμενα

    •  Εισαγωγή στον λ-λογισμό χωρίς τύπους.
    •  Κατασκευαστικότητα στα μαθηματικά και ιντουισιονιστική λογική.
    •  Σημασιολογία της λογικής, άλγεβρες Heyting και μοντέλα Kripke.
    • λ-λογισμός με απλούς τύπους.
    • Εισαγωγή στον ισομορφισμό Curry-Howard.
    • Αποδείξεις ως συνδυαστές (Hilbert style και combinators).
    • Κλασική λογική και σημασιολογία.
    • Τελεστές ελέγχου, control, call/cc, abort, continuations.
    • λ-λογισμός με τελεστές ελέγχου και ισομορφισμός Curry-Howard.
    • Ο λμ-λογισμός του Parigot.


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

    • https://repository.kallipos.gr/bitstream/11419/4527/3/merged_document_3-KOY.pdf (αναφορά, λ-λογισμός κολέτσος)
    • H.P. Barendregt, The Lambda Calcutta. Its Syntax and Semantics. North- Holland, second, revised edition, 1984.
    • J.-L. Krivine. Lambda-Calculus, Types and Models. Ellis Horwood Series in Computers and their Applications. Masson and Ellis Horwood, 1993.
    • M.H.B. Sorensen and P. Urzyezyn. Lectures on the Curry-Howard isomorphism, studies in logic and the foundations of mathematics, vol. 149, Elsevier 2006.
    • A.S. Troelstra and H, Sehwichtenberg, Basic Proof Theory, volume 43 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, second edition, 2000.
    • J-Y. Girard, Y. Lafont, and P. Taylor, Proofs and Types, volume 7 of Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 1989.
    • A.S. Troelstra and D. van Dalen. Constructivism in Mathematics. An Introduction, Volume I and II, volume 121 and 123 of Studies in Logic and the Foundations of Mathematics. North-Holland, 1988.
    • T.G. Griffin, A formulae-as-types notion of control. In Symposium on Principles of Programming Languages, pages 47-58. ACM Press, 1990.


    Για την εργασία: Ενδεικτικές προτάσεις θεμάτων


    1) Ενασχόληση με τον καθαρό (ή/και με τον με τύπους) λάμβδα λογισμό. Αποδείξεις

    των θεμελιωδών θεωρημάτων όπως, Church-Rosser, κανονικοποίηση με αριστερή

    β-αναγωγή, η-αναγωγή, ισχυρή κανονικοποίηση όταν υπάρχουν τύποι ή όταν

    προσημειώνονται κάποια redexes κ.α. Όλα αυτά θα μπορούσαν να γίνουν και στο

    πλαίσιο της τυποποίησης, γνωστής ως τυποποίηση με τύπους τομής.

    2) Τα συστήματα Τ του Gödel και F του Girard. Αποδείξεις ισχυρής κανονικοποίησης

    με τη μέθοδο της αναγωγιμότητας. Τύποι δεδομένων και προγραμματισμός σ’ αυτά

    τα συστήματα. Συναρτησιακή απεικόνιση στην αριθμητική και στην ανάλυση

    αντίστοιχα.

    3) Συστήματα επέκτασης του ισομορφισμού Curry-Howard στην κλασική λογική. Ο λμ-

    λογισμός του Parigot και αντίστοιχα συστήματα κλασικής λογικής.

    4) Κάποια θεωρία αποδείξεων και θεωρήματα απαλοιφής των τομών (Gentzen).

    5) Γραμμική λογική.

    6) Και βέβαια οποιαδήποτε άλλη πρόταση θέματος που σχετίζεται με το περιεχόμενο

    του μαθήματος.

    Σημείωση: κάποια θέματα μπορούν να αναληφθούν και από δύο ή τρία άτομα

    εφόσον η έκτασή τους το δικαιολογεί. Η παρουσίασή τους θα γίνει τμηματικά από

    του συμμετέχοντες.

  • 28 February - 6 March

    28 Φεβρουαρίου

    Γενική επισκόπηση του μαθήματος, Η έννοια της συνάρτησης και η εξέλιξή της, με τις δύο πλευρές της ως γράφημα και ως κανόνας, στα μαθηματικά. Η ενσάρκωση της συνάρτησης-πρόγραμμα στο λάμβδα λογισμό.

    • 7 March - 13 March

      7 Μαρτίου

      λ-λογισμός, όροι, ελεύθερες και δεσμευμένες μεταβλητές, α-ισοδυναμία, απλή και σωστή αντικατάσταση, λήμματα αντικατάστασης β-αναγωγή [βιβλιογραφία: λ-λογισμός κολέτσος, krivine lambda calculus types and models.


      • 14 March - 20 March

        14 Μαρτίου 

        Δεν πραγματοποιήθηκε

        • 21 March - 27 March

          Τρίτη 22 Μαρτίου

          λ-λογισμός: αριθμοί, πρωταρχικοί αναδρομικές ορισμοί συναρτήσεων (π.χ. pred)


          Τετάρτη 23 Μαρτίου

          λ-λογισμός: θεώρημα σταθερού σημείου


          • 28 March - 3 April

            Τρίτη 28 Μαρτίου 

            Τελευταία ενότητα σε λ-λογισμό: δημιουργία ζεύγους, αλήθειας, ψεύδους, θεώρημα σταθερού σημείου


            Τετάρτη 29 Μαρτίου

            Κατασκευαστική λογική, ιντουισιονισμός, φυσικές επαγωγές (Gentzen's natural deductions)


            • 4 April - 10 April

              Τρίτη 4 Απριλίου

              Συνέχεια στην ιντουισιονιστικη λογική. Lattices. Άλγεβρες Boole. Άλγεβρα Lindenbaum. Άλγεβρα Heyting.


              • 11 April - 17 April

                • 18 April - 24 April

                  • 25 April - 1 May

                    • 2 May - 8 May