Θεωρία τύπων
From Wikipedia, the free encyclopedia
Στα Μαθηματικά, στη Λογική και στη Επιστήμη των Υπολογιστών, η Θεωρία Τύπων είναι ένα από τα τυπικά συστήματα τα οποία χρησιμοποιούνται στην Απλοϊκή Θεωρία Συνόλων, ή στη μελέτη τέτοιων φορμαλισμών γενικότερα. Στη Θεωρία των Γλωσσών Προγραμματισμού, ενός κλάδου της Επιστήμης των Υπολογιστών, η Θεωρία Τύπων μπορεί να αναφέρεται στο σχεδιασμό, στην ανάλυση και στη μελέτη των Συστημάτων Τύπων, παρόλο που κάποιοι επιστήμονες της Πληροφορικής περιορίζουν τη σημασία του όρου στη μελέτη των αφηρημένων φορμαλισμών όπως ο λ-λογισμός με τύπους.
Ο Μπέρτραντ Ράσελ εφηύρε την πρώτη θεωρία τύπων μετά την ανακάλυψή του πως η εκδοχή της Απλοϊκής Θεωρίας Συνόλων του Γκότλομπ Φρέγκε υπόκειντο στο Παράδοξο του Ράσελ. Αυτή η θεωρία τύπων βρίσκεται σε περίοπτη θέση στο Principia Mathematica των Άλφρεντ Νορθ Γουάιτχεντ και Ράσελ. Αποφεύγει το Παράδοξο του Ράσελ με το να δημιουργεί πρώτα μία ιεραρχία τύπων, και κατόπιν να αναθέτει κάθε μαθηματική (και πιθανώς άλλη) οντότητα σε έναν τύπο. Τα αντικείμενα ενός δοσμένου τύπου δημιουργούνται αποκλειστικά από αντικείμενα προηγούμενων τύπων (αυτών που είναι χαμηλότερα στην ιεραρχία), αποφεύγοντας έτσι τις επαναλήψεις.
Ο Αλόνσο Τσερτς, εφευρέτης του λ-λογισμού, ανέπτυξε μια Λογική Υψηλής Τάξης γνωστότερη ως Θεωρία Τύπων του Τσερτς,[1] με σκοπό να αποφύγει το Παράδοξο Κλέινι-Ρόσερ που ταλαιπωρούσε τον αρχικό αμιγή λ-λογισμό. Η θεωρία τύπων του Τσερτς είναι μια παραλλαγή του λ-λογισμού στην οποία οι εκφράσεις (που επίσης καλούνται φόρμουλες ή λ-όροι) κατηγοριοποιούνται σε τύπους, και οι τύποι των εκφράσεων περιορίζουν τους τρόπους με τους οποίους μπορούν να συνδυαστούν. Με άλλα λόγια, είναι ένας λ-λογισμός με τύπους.
Το άρθρο Η Θεωρία Τύπων του Church στην Εγκυκλοπαίδεια την Φιλοσοφίας του Στάνφορντ είναι αφιερωμένο σε αυτό το θέμα.
Σήμερα χρησιμοποιούνται πολλοί άλλοι παρόμοιοι λογισμοί, συμπεριλαμβανομένης της Ιντουισιονιστικής θεωρίας τύπων του Περ Μάρτιν-Λέφ , του Συστήματος F του Ζαν-Ιβ Ζιράρ και του Λογισμoύ των κατασκευών. Στον λ-λογισμό με τύπους, οι τύποι παίζουν ένα ρόλο παρόμοιο με αυτό των συνόλων στη Θεωρία Συνόλων.