Αμιγές σύστημα τύπων

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

Στους κλάδους της μαθηματικής λογικής γνωστούς ως θεωρία αποδείξεων και θεωρία τύπων, ένα αμιγές σύστημα τύπων (pure type system), παλαιότερα γνωστό ως γενικευμένο σύστημα τύπων, είναι μια μορφή του λ-λογισμού με τύπους που επιτρέπει έναν αυθαίρετο αριθμό από είδη και εξαρτήσεις ανάμεσα σε αυτά. Το πλαίσιο μπορεί να θεωρηθεί σαν μία γενίκευση του λ-κύβου του Barendregt, με την έννοια ότι όλες οι γωνίες του κύβου μπορούν να αναπαρασταθούν σαν στιγμιότυπα του αμιγούς συστήματος τύπων με μόνο δύο είδη.[1][2] Πράγματι ο Barendregt (1991) σχημάτισε τον κύβο του με αυτήν την ρύθμιση.[3] Τα αμιγή συστήματα τύπων μπορεί να κάνουν δυσδιάκριτη την διαφορά ανάμεσα στου τύπους και στους όρους, η ιεραρχία τύπων καταρρέει, όπως και στην περίπτωση του λογισμού κατασκευών, αλλά αυτό δεν είναι η γενική περίπτωση, όπως ο λ-λογισμός με απλούς τύπους που επιτρέπει μόνο στους όρους να εξαρτώνται από τύπους.

Τα αμιγή συστήματα τύπων εισήχθησαν ανεξάρτητα από τους Stefano Berardi (1988) και Jan Terlouw (1989).[1][2] Η ιντουισιονιστικες λογικές περιγράφηκαν για πρώτη φορά ως αμιγή συστήματα τύπων από τον Barendregt.[4]Πρότυπο:Clarify Στην διδακτορική του διατριβή,[5] ο Berardi όρισε ένα κλασικό λογικό κύβο που περιέχει Ιντουισιονιστικές λογικές] παρόμοιες με τον λάμδα κύβο (αυτές οι προδιαγραφές είναι μη-ανεξαρτώμενες). Μία τροποποίηση αυτού του κύβου ονομάστηκε αργότερα Λ-κύβος από τον Geuvers, o οποίος στην διδακτορική του διατριβή επέκτεινε την αντιστοιχία Curry-Howard σε αυτόν τον σχεδιασμό.[6] Βασισμένος σε αυτές της ιδέες, ο Barthe και άλλοι όρισαν τα κλασικά αμιγή συστήματα τύπων προσθέτοντας έναν τελεστή διπλής άρνησης.[7] Παρόμοια, το 1998, ο Tijn Borghuis εισήγαγε τα τροπικά αμιγή συστήματα τύπων.[8] Ο Roorda συζήτησε την εφαρμογή των αμιγών συστημάτων τύπων στον συναρτησιακό προγραμματισμό; και οι Roorda και Jeuring πρότειναν μία γλώσσα προγραμματισμού βασισμένη στα αμιγή συστήματα τύπων.[9]

Τα συστήματα που στηρίζονται στον λ-κύβο είναι ισχυρά κανονικοποιήσιμα. Τα αμιγή συστήματα τύπων σε γενικές γραμμές δεν χρειάζεται να είναι, όπως για παράδειγμα το U από το παράδοξο του Girard δεν είναι. Επιπλέον, όλα τα αμιγή συστήματα τύπων που δεν είναι ισχυρά κανονικοποιήσιμα δεν είναι ούτε (ασθενώς) κανονικοποιήσιμα: περιέχουν εκφράσεις οι οποίες δεν έχουν κανονικές μορφές, ακριβώς όπως ο λαμδα λογισμός χωρίς τύπους. Το αν αυτό είναι πάντα η περίπτωση είναι ένα σημαντικό ανοικτό πρόβλημα στον τομέα αυτό, δηλαδή το αν ένα (ασθενώς) κανονικοποιήσιμο αμιγες σύστημα τύπων είναι πάντα ισχυρά κανονικοποιήσιμο. Αυτό είναι γνωστό ως η εικασία των Barendregt–Geuvers–Klop[10] (από τους Henk Barendregt, Herman Geuvers και Jan Willem Klop).

Υλοποιήσεις[Επεξεργασία | επεξεργασία κώδικα]

Οι επόμενες είναι γλώσσες προγραμματισμού που έχουν αμιγή συστήματα τύπων:

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

  1. 1,0 1,1 Pierce, Benjamin (2002). Types and Programming Languages. MIT Press, σελ. 466. ISBN 0-262-16209-1. 
  2. 2,0 2,1 Fairouz D. Kamareddine, Twan Laan, Rob P. Nederpelt, A modern perspective on type theory: from its origins until today, Springer, 2004, ISBN 1402023340, section 4c, "Pure type systems", p. 116
  3. Barendregt, H. P. (1991). «Introduction to generalized type systems». Journal of Functional Programming 1 (2): 125–154. http://dare.ubn.kun.nl/dspace/bitstream/2066/17240/1/13256.pdf. 
  4. H. Barendregt (1992). «Lambda calculi with types». Στο: S. Abramsky, D. Gabbay and T. Maibaum. Handbook of Logic in Computer Science. Oxford Science Publications. ftp://ftp.cs.ru.nl/pub/CompMath.Found/HBK.ps. 
  5. S. Berardi. Type dependence and Constructive Mathematics. PhD thesis, University of Torino, 1990.
  6. H. Geuvers. Logics and Type Systems, PhD thesis, University of Nijmegen, 1993.
  7. G. Barthe; J. Hatcliff; M. H. Sørensen (1997). «A Notion of Classical Pure Type System». Electronic Notes in Theoretical Computer Science 6: 4–59. doi:10.1016/S1571-0661(05)80170-7. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.32.1371. 
  8. Borghuis, Tijn (1998). «Modal Pure Type Systems». Journal of Logic, Language and Information 7 (3): 265–296. doi:10.1023/A:1008254612284. 
  9. Jan-Willem Roorda. «Pure Type Systems for Functional Programming». http://people.cs.uu.nl/johanj/MSc/jwroorda/.  Roorda's masters' thesis (linked from the cited page) also contains a general introduction to pure type systems.
  10. Sørensen, Morten Heine; Urzyczyn, Paweł (2006). «Pure type systems and the lambda cube». Lectures on the Curry–Howard isomorphism. Elsevier, σελ. 358. ISBN 0444520775. 

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

  • Morten Heine Sørensen, Paweł Urzyczyn, Lectures on the Curry–Howard isomorphism, Elsevier, 2006, ISBN 0444520775, chapter 14, "Pure type systems and the lambda cube."
  • Berardi, Stefano. Towards a mathematical analysis of the Coquand–Huet calculus of constructions and the other systems in Barendregt's cube. Technical report, Department of Computer Science, CMU, and Dipartimento Matematica, Universita di Torino, 1988.
  • Terlouw, J. (in Dutch) Een nadere bewijstheoretische analyse van GSTTs. Manuscript, University of Nijmegen, Netherlands, 1989.

Πρόσθετη ανάγνωση[Επεξεργασία | επεξεργασία κώδικα]

  • David A. Schmidt, The structure of typed programming languages, MIT Press, 1994, ISBN 0262193493, section 8.3, "Generalized Type Systems"

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