Λογική με πολλούς τύπους

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

Η λογική με πολλούς τύπους (many-sorted logic) μπορεί να αναπαριστά τυπικά την πρόθεση να μη χειριζόμαστε το σύμπαν σαν μια ομογενή συλλογή από αντικείμενα, αλλά να χωρίζεται αυτό με τρόπο παρόμοιο με αυτόν των τύπων του προγραμματισμού με τύπους. Τα συναρτησιακά και τα βεβαιωτικά (assertive) "μέρη του λόγου" της γλώσσας της λογικής ανακλούν αυτόν τον χωρισμό του σύμπαντος με τύπους, ακόμα και στο συντακτικό επίπεδο: η αντικατάσταση και το πέρασμα παραμέτρων μπορούν να γίνουν μόνο με αυτόν τον τρόπο, σεβόμενοι τους "τύπους".

Υπάρχουν πολλοί τρόποι για την τυποποίηση της παραπάνω πρόθεσης: μια λογική με πολλούς τύπους είναι κάθε "πακέτο" πληροφοριών που την ικανοποιεί. Στις περισσότερες περιπτώσεις δίνονται τα εξής:

  • ένα σύνολο από τύπους (sorts), S
  • μια κατάλληλη γενίκευση της έννοιας της υπογραφήςοπλισμού, αγγλ. signature) για να μπορεί να γίνει χειρισμός της επιπλέον πληροφορίας που έρχεται με τους τύπους.

Το πεδίο τότε κάθε δομής αυτής της υπογραφής χωρίζεται σε διακριτά υποσύνολα, ένα για κάθε τύπο.

Αλγεβροποίηση[Επεξεργασία | επεξεργασία κώδικα]

Η αλγεβροποίηση της λογικής με πολλούς τύπους εξηγείται στο On the Algebraization of Many-sorted Logics από τους Carlos Caleiro και Ricardo Gonçalves. Το βιβλίο γενικεύει την αφηρημένη αλγεβρική λογική στην περίπωση των πολλών τύπων, αλλά μπορεί να χρησιμοποιηθεί και σαν εισαγωγικό υλικό.

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

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