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

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

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

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

## Υλοποιήσεις
Οι επόμενες είναι γλώσσες προγραμματισμού που έχουν αμιγή συστήματα τύπων:
* SAGE 
* Yarrow 
* Henk 2000

## Σημειώσεις


## Αναφορές
* Morten Heine Sørensen, Paweł Urzyczyn, *Lectures on the Curry&ndash;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"

## Εξωτερικοί Σύνδεσμοι
* Pure Type Systems overview by Roger Bishop Jones

Κατηγορία:Θεωρία αποδείξεων
Κατηγορία:Θεωρία τύπων
Κατηγορία:Λ-λογισμός