Εξαρτώμενος τύπος

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
Μετάβαση σε: πλοήγηση, αναζήτηση

Στην επιστήμη των υπολογιστών και την λογική, ένας εξαρτώμενος τύπος είναι ένας τύπος που εξαρτάται από μία τιμή. Οι εξαρτώμενοι τύποι διαδραματίζουν κεντρικό ρόλο στην Ιντουισιονιστική θεωρία τύπων και στον σχεδιασμό συναρτησιακών γλωσσών προγραμματισμού σαν την ATS, την Agda και την Epigram.

Ένα παράδειγμα είναι ο τύπος των ν-άδων από πραγματικούς αριθμούς. Αυτός είναι ένας εξαρτώμενος τύπος επειδή ο τύπος εξαρτάται από την τιμή ν.

Ο έλεγχος ισότητας μεταξύ εξαρτώμενων τύπων σε ένα πρόγραμμα μπορεί να απαιτεί υπολογισμούς. Αν επιτραπεί η χρήση οποιονδήποτε τιμών στους εξαρτώμενους τύπους, τότε ο έλεγχος ισότητας τύπων μπορεί να περιέχει έλεγχο για το αν δύο τυχαία προγράμματα παράγουν το ίδιο αποτέλεσμα. Τότε ο έλεγχος τύπων γίνεται μη αποφασίσιμο πρόβλημα.

Απόρροια του ισομορφισμού Curry-Howard είναι ότι μπορούν να κατασκευαστούν τύποι που περιγράφουν οσοδήποτε πολύπλοκες μαθηματικές ιδιότητες. Αν ο χρήστης μπορεί να δώσει μια κατασκευαστική απόδειξη ότι ένας τύπος είναι κατοικήσιμος (δηλαδή ότι υπάρχει τιμή τέτοιου τύπου), τότε ένας μεταγλωττιστής μπορεί να ελέγξει την απόδειξη και να την μετατρέψει σε εκτελέσιμο κώδικα που υπολογίζει την τιμή ακολουθώντας την κατασκευή. Η δυνατότητα ελέγχου αποδείξεων καθιστά τις γλώσσες με εξαρτώμενους τύπους στενά συνδεδεμένες με βοηθούς αποδείξεων. Η πλευρά παραγωγής κώδικα αποτελεί μια ισχυρή προσέγγιση στην επαλήθευση προγραμμάτων, αφού ο κώδικας απορρέει απευθείας από μια μηχανικά επαληθευμένη μαθηματική απόδειξη.

Συστήματα του λάμδα κύβου[Επεξεργασία | επεξεργασία κώδικα]

Ο Henk Barendregt επινόησε τον λάμδα κύβο σαν ένα μέσο κατηγοριοποίησης των συστημάτων τύπων πάνω σε 3 άξονες. Κάθε μία από τις 8 κορυφές του παραγόμενου διαγράμματος κυβικού σχήματος αντιστοιχεί σε ένα σύστημα τύπων με τον λ-λογισμό με τύπους και τον λογισμό των κατασκευών στην λιγότερο και περισσότερο εκφραστική κορυφή του κύβου αντίστοιχα. Οι τρεις άξονες του κύβου αντιστοιχούν σε τρεις διαφορετικές επεκτάσεις του λ-λογισμού με απλούς τύπους: την προσθήκη εξαρτώμενων τύπων, την προσθήκη πολυμορφισμού και την προσθήκη κατασκευαστών τύπων υψηλότερης τάξης (πχ. συναρτήσεις από τύπους σε τύπους). Ο λάμδα κύβος γενικεύεται περαιτέρω από τα αμιγή συστήματα τύπων,

Θεωρία εξαρτώμενων τύπων πρώτης τάξης[Επεξεργασία | επεξεργασία κώδικα]

Το σύστημα \lambda \Pi των αγνών εξαρτώμενων τύπων πρώτης τάξεως, που αντιστοιχεί στο [LF]], παράγεται από την γενίκευση του τύπου του χώρου συναρτήσεων του λ-λογισμού με απλούς τύπου στον τύπο του εξαρτημένου γινομένου????

Η έκφραση \Pi n:{\mathbb N}.\mbox{Vec}({\mathbb R},n), όπου γράφουμε \mbox{Vec}({\mathbb R},n) για τις ν-άδες πραγματικών αριθμών, αποτελεί την τύπο των συναρτήσεων οι οποίες δεδομένου ενός φυσικού αριθμού n επιστρέφουν μια ν-άδα από πραγματικούς αριθμούς. Ο συνήθης χώρος συναρτήσεων προκύπτει σαν μια ειδική περίπτωση όταν το πεδίο τιμών δεν εξαρτάται από την είσοδο, πχ ο τύπος \Pi n:{\mathbb N}.{\mathbb R} είναι ο τύπος των συναρτήσεων από φυσικούς αριθμούς σε πραγματικούς αριθμούς, γραμμένος σαν {\mathbb N}\to{\mathbb R} στον λ-λογισμό με απλούς τύπους.

Θεωρία εξαρτώμενων τύπων δευτέρας τάξης[Επεξεργασία | επεξεργασία κώδικα]

Το σύστημα \lambda \Pi 2 των εξαρτώμενων τύπων δευτέρας τάξης παράγεται από το \lambda \Pi επιτρέποντας ποσοδείκτες πάνω στους κατασκευαστές τύπων. Σε αυτή τη θεωρία, ο τελεστής εξαρτώμενου γινομένου εμπεριέχει τόσο τον τελεστή \to από τον λ-λογισμό με απλούς τύπους όσο και τον ποσοδείκτη \forall του συστήματος F.

Πολυμορφικός λ-λογισμός με εξαρτώμενους τύπους υψηλής τάξης[Επεξεργασία | επεξεργασία κώδικα]

Το υψηλής τάξης σύστμα \lambda \Pi \omega επεκτείνει το \lambda \Pi 2 σε όλες τις δυνατές κατευθύνσεις του λάμδα κύβου: συναρτήσεις από όρους σε όρους, τύπους σε τύπους, τύπους σε όρους και όρους σε τύπους. Το σύστημα αυτό αντιστοιχεί στον λογισμό των κατασκευών, από τον οποίο παράγεται ο λογισμός των επαγωγικών κατασκευών που αποτελεί το σύστημα πίσω από τον βοηθό αποδείξεων Coq.

Αντικειμενοστραφής προγραμματισμός[Επεξεργασία | επεξεργασία κώδικα]

Πρόσφατη έρευνα[1] προσανατολίζεται στο συνδυασμό της θεωρίας εξαρτώμενων τύπων με τον αντικειμενοστραφή προγραμματισμό.

Δείτε επίσης[Επεξεργασία | επεξεργασία κώδικα]

Αναφορές[Επεξεργασία | επεξεργασία κώδικα]

  1. Anton Setzer (2007). «Object-oriented programming in dependent type theory». Στο: Henrik Nilsson. Trends in Functional Programming, vol. 7. Intellect. σελ. 91–108. http://www.cs.swan.ac.uk/~csetzer/articles/objectOrientedProgrammingInDepTypeTheoryTfp2006PostProceedings.pdf. 

Επιπλέον διάβασμα[Επεξεργασία | επεξεργασία κώδικα]

Εξωτερικοί σύνδεσμοι[Επεξεργασία | επεξεργασία κώδικα]

Στο λήμμα αυτό έχει ενσωματωθεί κείμενο από το λήμμα Dependent type της Αγγλικής Βικιπαίδειας, η οποία διανέμεται υπό την GNU FDL και την CC-BY-SA 3.0. (ιστορικό/συντάκτες).