Γλωσσάρι Θεωρίας Τύπων και Θεωρίας Κατηγοριών
Όταν, τον Μάρτιο του 2018, ξεκίνησα να επιβλέπω τη διπλωματική του Μάνου Πλίτση, τότε φοιτητή του ΣΕΜΦΕ, η οποία αφορούσε την κατηγορική σημασιολογία των εξαρτημένων τύπων, συνειδητοποίησα με τρόμο ότι δεν μπορούσα ούτε να αρθρώσω τον όρο εξαρτημένος τύπος. Μα πώς να λέγονται τα dependent types στα Ελληνικά;
Η θεωρία κατηγορίων, καθώς και τα συμπαρομαρτούντα αντικείμενα, ανήκουν στα ύστερα μαθηματικά του δευτερού μισού του 20ου αιώνα, δηλαδή την εποχή της παγκοσμιοποίσης, του εξαμερικανισμού, και της Αγγλικής ως εκ των πραγμάτων lingua franca. Εαν προσθέσουμε σε αυτό το γεγονός ότι ελάχιστοι ερευνητές εντός Ελλάδος ασχολούνται με το αντικείμενο (τα μεγάλα κέντρα ανάπτυξής του είναι η Αγγλία και η Γαλλία), τότε δεν είναι καθόλου παράδοξο το γεγονός ότι οι όροι της δεν έχουν ακόμα μεταφραστεί συστηματικά.
Ευτυχώς, για καλό ή για κακό, οι κανόνες του ΣΕΜΦΕ επιβάλλουν οι διπλωματικές εργασίες να γράφονται στα Ελληνικά. Για αυτό ασχοληθήκαμε με την συστηματική καταγραφή και μετάφραση των όρων που χρειάστηκε στη διπλωματική του. Σε μεγάλο βαθμό βασιστήκαμε στην διπλωματική της Κοάρ Μαρντιροσιάν που παρουσιάστηκε το 2014, και την οποία επέβλεψε ο Νίκος Τζεβελέκος.
Άλλες φορές καταφύγαμε στο Αγγλοελληνικόν Λεξικόν των Θεωρητικών και Εφηρμοσμένων Μαθηματικών του Μέμα Κολαΐτη. Τα αντίστοιχα λήμματα σημειώνονται με (ΜΚ). Παρά την παλαιότητα του (εκδόθηκε το 1975), το λεξικό του Κολαΐτη περιλαμβάνει πολλούς σχετικούς όρους, πιθανά λόγω της ήδη από τότε μεγάλης επιρροής της αλγεβρικής τοπολογίας και αλγεβρικής γεωμετρίας. Aς μην ξεχνάμε ότι ο Γκρόθεντικ έγραψε το μεγαλύτερο μέρος του έργου του στα Γαλλικά, και οι περισσότεροι Έλληνες μαθηματικοί της εποχής ήταν μάλλον γαλλοσπουδαγμένοι. Πώς, άλλωστε, κατέληξε το λεξικό του Κολαΐτη να περιλαμβάνει όρους-διαμάντια, όπως π.χ. γροθενδικιανή συνομολογικότης (Grothendieck cohomology);
Τέλος, αναγκαστήκαμε πολλές φορές να καταφύγουμε σε αυτοσχεδιασμό, τον οποίον σημειώνουμε με (Ν). Μπορεί η αλγεβρική τοπολογία να είναι προπολεμική, αλλά τα κατηγορικά μοντέλα της θεωρίας τύπων ανήκουν αδιαμφισβήτητα στην μετά-την-disco εποχή. Προσπαθήσαμε όσο γίνεται να μείνουμε πιστοί στις Ελληνικές ρίζες, και το λεξικό του Τριανταφυλλίδη αποτέλεσε ένα στοιχειώδες καταφύγιο. Αναμένουμε σχόλια, προτάσεις και παρατηρήσεις.
Γλωσσάρι Θεωρίας Κατηγοριών
| Αγγλικός όρος | Ελληνικός όρος | Σημειώσεις |
|---|---|---|
| category | κατηγορία | |
| categorical | κατηγορικός | |
| morphism | μορφισμός | MK |
| composition | σύνθεση | |
| commuting/commutative diagram | αντιμεταθετικό διάγραμμα | δείτε υπόμνημα |
| identity morphism | ταυτοτικός μορφισμός | |
| functor | συναρτητής | |
| natural transformation | φυσικός μετασχηματισμός | |
| (cartesian) product | (καρτεσιανό) γινόμενο | |
| homomorphism | ομομορφισμός | MK |
| isomorphism | ισομορφιμός | MK |
| monomorphism | μονομορφισμός | |
| epimorphism | επιμορφισμός | MK |
| universal property | καθολική ιδιότητα | |
| initial object | αρχικό αντικείμενο | |
| terminal/final object | τερματικό/τελικό αντικείμενο | |
| initial object | αρχικό αντικείμενο | |
| opposite (functor/category) | αντίθετος, -η, -ο | |
| full | πλήρης | |
| faithful | πιστός | |
| covariant | συναλλοιωτός, -η, -ο | |
| contravariant | ανταλλοιωτός, -η, -ο |
Γλωσσάρι Λογικής και Θεωρίας Τύπων
| Αγγλικός όρος | Ελληνικός όρος | Σημειώσεις |
|---|---|---|
| type theory | θεωρία τύπων | |
| (typing) context | περιβάλλον (τυποποίησης) | |
| term | όρος | |
| type | τύπος | |
| substitution | αντικατάσταση | |
| natural deduction | φυσική επαγωγή | |
| sequent calculus | ????? | |
| structural rules | δομικοί κανόνες | |
| substructural (logic) | υποδομική (λογική) | |
| weakening | εξασθένηση | |
| exchange | ανταλλαγή | N |
| contraction | συναίρεση | N |
| definitional equality | ισότητα καθ’ορισμόν | N |
| admissible rule | επιτρεπτός κανόνας | N |
| contraction | συναίρεση | N |
| formation rule | κανόνας διαμόρφωσης | N |
| introduction rule | κανόνας εισαγωγής | N |
| elimination rule | κανόνας απαλοιφής | N |
| computation rule | κανόνας υπολογισμού | N |
| uniqueness rule | κανόνας μοναδικότητας | N |
| (β-/η-)reduction | αναγωγή (τύπου β, τύπου η) | |
| (β-/η-)conversion | μετατροπή (τύπου β, τύπου η) | |
| dependent product | εξαρτημένο γινόμενο | N |
| dependent sum | εξαρτημένο άθροισμα | N |
| disjoint union | αποσυνδετή ένωση | |
| canonical form | θεσμική μορφή | NK |
Υπόμνημα: “Commutative”
Υπάρχει μια σχετική σύγχυση γύρω από τον όρο “commutative” και την Ελληνική του απόδοση.
Όσον αφορά την σχετική ιδιότητα των αλγεβρικών πράξεων, π.χ. της πρόσθεσης και του πολλαπλασιασμού φυσικών αριθμών, έχει επικρατήσει αδιαμφισβήτητα ο όρος αντιμεταθετική ιδιότητα. Κάποιοι μαθηματικοί, ιδιαίτερα όταν ασχολούνται με την ομολογιακή άλγεβρα ή την θεωρία κατηγοριών, χρησιμοποιούν τον όρο μεταθετική ιδιότητα για να αποδώσουν το commutative property/commutativity, και μεταθετικό διάγραμμα για να αποδώσουν το commuting/commutative diagram.
Το λεξικό του Κολαΐτη προτιμά συστηματικά τον όρο με το πρόθημα “αντι-.” Επίσης, το λεξικό του Τριανταφυλλίδη δικαιώνει ετυμολογικά αυτή την προτίμηση:
αντιμετάθεση η [andimetáθesi] Ο33 : (λόγ.) αμοιβαία αλλαγή θέσεως. α. (μαθημ.) η ιδιότητα της πρόσθεσης και του πολλαπλασιασμού να μην αλλοιώνεται το αποτέλεσμα, όταν αλλάξει η σειρά των όρων. β. (γλωσσ.) φαινόμενο κατά το οποίο δύο φθόγγοι ή δύο συλλαβές αλλάζουν αμοιβαία θέση μέσα στην ίδια λέξη, π.χ. πλατσουκωτός > πλακουτσωτός. || (γραμμ.) η αντιμεταχώρηση. [λόγ.: β: ελνστ. ἀντιμετάθε(σις) -ση· α: σημδ. γαλλ. permutation]
Η λόγια χρήση της λέξης αναφέρεται στην αμοιβαία αλλαγή θέσεως. Θα προτιμήσουμε λοιπόν τη χρήση του προθήματος, καθώς πιστεύουμε ότι η αμοιβαιότητα είναι κεντρικό στοιχείο του commutativity. Για παράδειγμα, στην κυκλική γραμμική λογική (cyclic linear logic), έχουμε κυκλικές μεταθέσεις, δηλαδή μπορούμε να πάμε από το Α, Β, Γ, Δ, Ε στο Δ, Ε, Α, Β, Γ, αλλά όχι “ελεύθερες” αντιμεταθέσεις.
Για αυτούς τους λόγους, επιμένουμε στη χρήση του αντιμεταθετικού διαγραμμάτος ως απόδοση του commutative diagram.
Τελευταία Ανανέωση: 30/6/18