Επαλήθευση Ιδιοτήτων Πολυπλοκότητας Δυαδικών Δέντρων Αναζήτησης σε Liquid Haskell

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