Please use this identifier to cite or link to this item:
http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/15862
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.author | Ιωάννης Κοκκίνης | |
dc.date.accessioned | 2018-07-23T16:41:34Z | - |
dc.date.available | 2018-07-23T16:41:34Z | - |
dc.date.issued | 2010-11-9 | |
dc.date.submitted | 2010-12-9 | |
dc.identifier.uri | http://artemis-new.cslab.ece.ntua.gr:8080/jspui/handle/123456789/15862 | - |
dc.description.abstract | Σκοπός της εργασίας είναι να δείξουμε πώς η τυποποίηση (απόδοση τύπων) μπορεί να χρησιμοποιηθεί ως ισχυρό εργαλείο για την απόδειξη θεωρημάτων στο λ-λογισμό, τα οποία σχετίζονται κυρίως με την κανονικοποίηση. Ως σύστημα τυποποίησης χρησιμοποιείται συνήθως το σύστημα τύπων τομής D, το οποίο παρουσιάζει την ενδιαφέρουσα ιδιότητα κάθε όρος που τυποποιείται σε αυτό να είναι ισχυρά κανονικοποιήσιμος. Για να δείξουμε όμως ότι η χρήση των τύπων τομής δεν είναι πάντοτε απαραίτητη καταλήγουμε σε μερικά συμπεράσματα και με τη χρήση τυποποίησης στο λ-λογισμό με απλούς τύπους. Τα περιεχόμενα των κεφαλαίων έχουν ως εξής:Κεφάλαιο 1 (Καθαρός λάμβδα λογισμός): Αναφερόμαστε, χωρίς να εμβαθύνουμε πολύ, σε έννοιες όπως οι ελεύθερες μεταβλητές, οι υποόροι, η β-αναγωγή και η ισχυρή κανονικοποίηση.Κεφάλαιο 2 (Τύποι): Αναφερόμαστε στη χρησιμότητα των τύπων στον προγραμματισμό και εισάγουμε τα δύο συστήματα τύπων με τα οποία θα ασχοληθούμε: λάμβδα λογισμός με απλούς τύπους και σύστημα D.Κεφάλαιο 3 (Αναπτύξεις): Εξηγούμε την έννοια της ανάπτυξης. Αποδεικνύουμε το θεώρημα των πεπερασμένων αναπτύξεων και βλέπουμε πώς αυτό μπορεί να μας οδηγήσει σε μια ικανή συνθήκη ισχυρής κανονικοποίησης.Κεφάλαιο 4Η ιδιότητα Church-Rosser. Με χρήση της μεθόδου της αναγωγιμότητας (reducibility method) αποδεικνύουμε την ισχύ της ιδιότητας Church-Rosser για τους τυποποιήσιμους όρους στο σύστημα D, ύστερα αποδεικνύουμε την ισχύ της ιδιότητας Church-Rosser για τις αναπτύξεις και τέλος αποδεικνύουμε το θεώρημα Church-Rosser για τον καθαρό λάμβδα λογισμό.Κεφάλαιο 5(Το Ω-θεώρημα): Παρουσιάζουμε μια απόδειξη του Ω-θεωρήματος με χρήση τυποποποίησης στο σύστημα D.Κεφάλαιο 6 (Ανοιχτά προβλήματα): Δίνουμε κατευθύνσεις για μελλοντική έρευνα σε τομείς που σχετίζονται με το αντικείμενο της παρούσας εργασίας. | |
dc.language | Greek | |
dc.subject | λ-λογισμός | |
dc.subject | τερματισμός | |
dc.subject | ισχυρή κανονικοποίηση | |
dc.subject | church-rosser | |
dc.subject | ω-θεώρημα | |
dc.subject | development | |
dc.subject | typing | |
dc.subject | reducibility method | |
dc.title | Τυποποίηση Και Τερματισμός Στο Λ-λογισμό | |
dc.type | Diploma Thesis | |
dc.description.pages | 47 | |
dc.contributor.supervisor | Κολέτσος Γεώργιος | |
dc.department | Τομέας Τεχνολογίας Πληροφορικής & Υπολογιστών | |
dc.organization | ΕΜΠ, Τμήμα Ηλεκτρολόγων Μηχανικών & Μηχανικών Υπολογιστών | |
Appears in Collections: | Διπλωματικές Εργασίες - Theses |
Files in This Item:
File | Size | Format | |
---|---|---|---|
DT2010-0278.pdf | 416.09 kB | Adobe PDF | View/Open |
Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.