Please use this identifier to cite or link to this item: http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/15862
Title: Τυποποίηση Και Τερματισμός Στο Λ-λογισμό
Authors: Ιωάννης Κοκκίνης
Κολέτσος Γεώργιος
Keywords: λ-λογισμός
τερματισμός
ισχυρή κανονικοποίηση
church-rosser
ω-θεώρημα
development
typing
reducibility method
Issue Date: 9-Nov-2010
Abstract: Σκοπός της εργασίας είναι να δείξουμε πώς η τυποποίηση (απόδοση τύπων) μπορεί να χρησιμοποιηθεί ως ισχυρό εργαλείο για την απόδειξη θεωρημάτων στο λ-λογισμό, τα οποία σχετίζονται κυρίως με την κανονικοποίηση. Ως σύστημα τυποποίησης χρησιμοποιείται συνήθως το σύστημα τύπων τομής D, το οποίο παρουσιάζει την ενδιαφέρουσα ιδιότητα κάθε όρος που τυποποιείται σε αυτό να είναι ισχυρά κανονικοποιήσιμος. Για να δείξουμε όμως ότι η χρήση των τύπων τομής δεν είναι πάντοτε απαραίτητη καταλήγουμε σε μερικά συμπεράσματα και με τη χρήση τυποποίησης στο λ-λογισμό με απλούς τύπους. Τα περιεχόμενα των κεφαλαίων έχουν ως εξής:Κεφάλαιο 1 (Καθαρός λάμβδα λογισμός): Αναφερόμαστε, χωρίς να εμβαθύνουμε πολύ, σε έννοιες όπως οι ελεύθερες μεταβλητές, οι υποόροι, η β-αναγωγή και η ισχυρή κανονικοποίηση.Κεφάλαιο 2 (Τύποι): Αναφερόμαστε στη χρησιμότητα των τύπων στον προγραμματισμό και εισάγουμε τα δύο συστήματα τύπων με τα οποία θα ασχοληθούμε: λάμβδα λογισμός με απλούς τύπους και σύστημα D.Κεφάλαιο 3 (Αναπτύξεις): Εξηγούμε την έννοια της ανάπτυξης. Αποδεικνύουμε το θεώρημα των πεπερασμένων αναπτύξεων και βλέπουμε πώς αυτό μπορεί να μας οδηγήσει σε μια ικανή συνθήκη ισχυρής κανονικοποίησης.Κεφάλαιο 4Η ιδιότητα Church-Rosser. Με χρήση της μεθόδου της αναγωγιμότητας (reducibility method) αποδεικνύουμε την ισχύ της ιδιότητας Church-Rosser για τους τυποποιήσιμους όρους στο σύστημα D, ύστερα αποδεικνύουμε την ισχύ της ιδιότητας Church-Rosser για τις αναπτύξεις και τέλος αποδεικνύουμε το θεώρημα Church-Rosser για τον καθαρό λάμβδα λογισμό.Κεφάλαιο 5(Το Ω-θεώρημα): Παρουσιάζουμε μια απόδειξη του Ω-θεωρήματος με χρήση τυποποποίησης στο σύστημα D.Κεφάλαιο 6 (Ανοιχτά προβλήματα): Δίνουμε κατευθύνσεις για μελλοντική έρευνα σε τομείς που σχετίζονται με το αντικείμενο της παρούσας εργασίας.
URI: http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/15862
Appears in Collections:Διπλωματικές Εργασίες - Theses

Files in This Item:
File SizeFormat 
DT2010-0278.pdf416.09 kBAdobe PDFView/Open


Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.