Τυποποίηση Και Τερματισμός Στο Λ-λογισμό

Abstract

Σκοπός της εργασίας είναι να δείξουμε πώς η τυποποίηση (απόδοση τύπων) μπορεί να χρησιμοποιηθεί ως ισχυρό εργαλείο για την απόδειξη θεωρημάτων στο λ-λογισμό, τα οποία σχετίζονται κυρίως με την κανονικοποίηση. Ως σύστημα τυποποίησης χρησιμοποιείται συνήθως το σύστημα τύπων τομής D, το οποίο παρουσιάζει την ενδιαφέρουσα ιδιότητα κάθε όρος που τυποποιείται σε αυτό να είναι ισχυρά κανονικοποιήσιμος. Για να δείξουμε όμως ότι η χρήση των τύπων τομής δεν είναι πάντοτε απαραίτητη καταλήγουμε σε μερικά συμπεράσματα και με τη χρήση τυποποίησης στο λ-λογισμό με απλούς τύπους. Τα περιεχόμενα των κεφαλαίων έχουν ως εξής:Κεφάλαιο 1 (Καθαρός λάμβδα λογισμός): Αναφερόμαστε, χωρίς να εμβαθύνουμε πολύ, σε έννοιες όπως οι ελεύθερες μεταβλητές, οι υποόροι, η β-αναγωγή και η ισχυρή κανονικοποίηση.Κεφάλαιο 2 (Τύποι): Αναφερόμαστε στη χρησιμότητα των τύπων στον προγραμματισμό και εισάγουμε τα δύο συστήματα τύπων με τα οποία θα ασχοληθούμε: λάμβδα λογισμός με απλούς τύπους και σύστημα D.Κεφάλαιο 3 (Αναπτύξεις): Εξηγούμε την έννοια της ανάπτυξης. Αποδεικνύουμε το θεώρημα των πεπερασμένων αναπτύξεων και βλέπουμε πώς αυτό μπορεί να μας οδηγήσει σε μια ικανή συνθήκη ισχυρής κανονικοποίησης.Κεφάλαιο 4Η ιδιότητα Church-Rosser. Με χρήση της μεθόδου της αναγωγιμότητας (reducibility method) αποδεικνύουμε την ισχύ της ιδιότητας Church-Rosser για τους τυποποιήσιμους όρους στο σύστημα D, ύστερα αποδεικνύουμε την ισχύ της ιδιότητας Church-Rosser για τις αναπτύξεις και τέλος αποδεικνύουμε το θεώρημα Church-Rosser για τον καθαρό λάμβδα λογισμό.Κεφάλαιο 5(Το Ω-θεώρημα): Παρουσιάζουμε μια απόδειξη του Ω-θεωρήματος με χρήση τυποποποίησης στο σύστημα D.Κεφάλαιο 6 (Ανοιχτά προβλήματα): Δίνουμε κατευθύνσεις για μελλοντική έρευνα σε τομείς που σχετίζονται με το αντικείμενο της παρούσας εργασίας.