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

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

Στους κλάδους της μαθηματικής λογικής γνωστούς ως θεωρία αποδείξεων και θεωρία τύπων, ένα αμιγές σύστημα τύπων (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 (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"

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