Please use this identifier to cite or link to this item:
http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/18232
Title: | Επαλήθευση Ιδιοτήτων Πολυπλοκότητας Δυαδικών Δέντρων Αναζήτησης σε Liquid Haskell |
Authors: | Οικονόμου, Χρυσούλα Παπασπύρου Νικόλαος |
Keywords: | Liquid Haskell Red-Black Δέντρα Δυαδικά Δέντρα Αναζήτησης Ανάλυση Κόστους Τυπική Επαλήθευση Εκλεπτυσμένοι Τύποι |
Issue Date: | 26-Mar-2021 |
Abstract: | Στην παρούσα διπλωματική εργασία, εξερευνούμε την χρηστικότητα και τις δυνατότητες της Liquid Haskell (LH) και επιχειρούμε να συνεισφέρουμε στην βιβλιοθήκη της. H LH είναι μία επέκταση στο σύστημα τύπων της γλώσσας προγραμματισμού Haskell. Η επέκταση αυτή αφορά την εισαγωγή των εκλεπτυσμένων τύπων (refinement types) στο υπάρχον σύστημα τύπων, με τους οποίους εκφράζουμε ιδιότητες ορθότητας και πολυπλοκότητας. Ένα υποσύνολο των εκλεπτυσμένων τύπων είναι οι Liquid Τύποι (Logical Qualified Data Types) οι οποίοι περιορίζουν ακόμη περισσότερο τη γλώσσα των κατηγορημάτων που μπορούν να υπάρχουν στους εκλεπτυσμένους τύπους, ώστε να επιτυγχάνεται αυτόματα ο συμπερασμός τύπων στα ενδιάμεσα στάδια ενός προγράμματος, χαρακτηριστικό πολύ χρήσιμο για ένα σύστημα τύπων. Συστήματα τύπων με αυτόματο συμπερασμό τύπων καθίστανται χρήσιμα πέρα από θεωρητικά και πρακτικά για την προγραμματίστρια. Η δική μας συνεισφορά επικεντρώνεται στην ανάλυση της πολυπλοκότητας και της ορθότητας κάποιων δημοφιλών δομών δεδομένων (Binary Search Trees, Red-Black Trees) με χρήση της Liquid Haskell. Για τις περισσότερες αποδείξεις αρκεί η intrinsic μέθοδος, δηλαδή τόσο το κόστος της συνάρτησης όσο και οι ιδιότητες ορθότητας που θέλουμε να αποδείξουμε δηλώνονται στον τύπο της μέσω εκλεπτυσμένων κατηγορημάτων και αποδεικνύονται αυτόματα από τον SMT Solver. Ωστόσο, όταν τα κατηγορήματα που συνθέτουν τους εκλεπτυσμένους τύπους δεν ανήκουν στην SMT-αποφασίσιμη λογική, χρησιμοποιούμε την extrinsic μέθοδο. Δηλαδή εκφράζουμε θεωρήματα και λήμματα για τα κόστη και τις ιδιότητες ορθότητας των συναρτήσεων χρησιμοποιώντας εκλεπτυσμένους τύπους και έπειτα γράφουμε αποδείξεις για αυτά σε Haskell, χρησιμοποιώντας συνδυαστές απόδειξης (proof combinators). Ο κώδικάς μας μπορεί να βρεθεί στη διεύθυνση: https://github.com/linen101/ticked-binary-search-trees |
URI: | http://artemis.cslab.ece.ntua.gr:8080/jspui/handle/123456789/18232 |
Appears in Collections: | Διπλωματικές Εργασίες - Theses |
Files in This Item:
File | Description | Size | Format | |
---|---|---|---|---|
theses-ChrysaOikonomou.pdf | 452.3 kB | Adobe PDF | View/Open |
Items in Artemis are protected by copyright, with all rights reserved, unless otherwise indicated.