Η έννοια της ατομικότητας της πληροφορίας είν' απ' τα πράγματα που μ' έχουν στοιχειώσει στο παρελθόν, κι' ακόμα με στοιχειώνουν. Λές οτι ένα σύνολο \(U\) απο ατομικές πληροφορίες είναι το ίδιο ατομικό, στην περίπτωση που για κάθε ατομική πληροφορία \(b\), όταν \(U \vdash b\), τότε υπάρχει μία \(a \in U\) με \(\{a\} \vdash b\): οποιαδήποτε ατομική πληροφορία ενέχεται στην \(U\), θα ενέχεται και σε κάποιο ατομικό της κομμάτι.
Αυτό ενγένει είναι χοντρή απαίτηση, καθώς η ατομικότητα κατα κάποιο τρόπο πάει κόντρα σε μία εγγενή στο χώρο έννοια ανεξαρτησίας. Σκέψου το \(U\) ως (περατό) σύνολο διανυσμάτων σε κάποιον διανυσματικό χώρο και το \(b\) ως διάνυσμα, και ερμήνευσε τον ισχυρισμό «το \(U\) ενέχει την πληροφορία \(b\)» ώς «το διάνυσμα \(b\) γράφεται ως γραμμικός συνδυασμός κάποιων διανυσμάτων του \(U\)». Να πείς οτι το \(U\) είναι ατομικό, είναι να πείς οτι κάθε φορά που ένα διάνυσμα \(b\) γράφεται ως γραμμικός συνδυασμός διανυσμάτων \(\{a_1, \ldots, a_m\} \subseteq U\), στην πραγματικότητα μπορεί να γραφτεί ως γραμμικός συνδυασμός, δηλαδή πολλαπλάσιο, ενός μόνο διανύσματος \(a \in U\). Αυτό ισχύει πιχί στην πραγματική ευθεία, οπου μάλιστα για κάθε μή μηδενικό διάνυσμα \(a \in U\) (με \(U\) μή κενο) έχουμε \(b = \kappa a\), για \(\kappa = b/a\), αλλα δέν ισχύει σε ανώτερες διαστάσεις: στο επίπεδο πιχί έχουμε \(\{(1, 0), (0,1)\} \vdash (1,1)\), αλλα κανένα απο τα διανύσματα αριστερά δέν αρκεί για να παράξει απο μόνο του το διάνυσμα στα δεξιά.
Σχετικά με την ατομικότητα προκύπτουν κάποιες εύκολες παρατηρήσεις (πιχί κάθε μονοσύνολο είναι ατομικό) και κάποιες εύλογες, ωραίες απορίες. Μία τέτοια απορία που μ' απασχόλησε πολύ στο παρελθόν, είναι η εξής: εντάξει, δέν έχουμε ατομικότητα για κάθε \(U\), αλλα μήπως μπορούμε να βρούμε κάποιο \(U'\) πληροφοριακά ισοδύναμο με το \(U\), που να ενέχει δηλαδή ακριβώς τις ίδιες πληροφορίες, το οποίο να είναι ατομικό; Στο παράδειγμα του ευκλείδειου επιπέδου βλέπουμε οτι αυτό δέν γίνεται. Πηγαίνοντάς το αυθόρμητα και προσθέτοντας στη βάση \(\{(1, 0), (0,1)\}\), αν όχι κάθε διάνυσμα που αυτή αποτυχαίνει να ενέχει ατομικά, έστω ένα για κάθε ευθεία που μας λείπει, θα χάναμε προφανώς την περατότητα του \(U\): οι ευθείες που έχουμε να καλύψουμε μεταξύ των δύο αξόνων είναι άπειρες το πλήθος. Απ' την άλλη, απο βασικές γνώσεις γραμμικής άλγεβρας, ξέρουμε οτι άμα θές να διατηρήσεις την πληροφορία της βάσης (στην προκείμενη περίπτωση, κάθε διάνυσμα στον επαγόμενο υποχώρο), δέν μπορείς ν' αφαιρέσεις διανύσματα απ' αυτήν, και επίσης οτι κάθε άλλη βάση είναι ατομικά(!) ισοδύναμη μ' αυτήν· ατομικότητα εδώ σημαίνει περιορισμό της επιχειρηματολογίας σε ευθείες (σημαίνει ήδη «γραμμικότητα»). Άρα πάπαλα.
Ωστόσο, υπάρχουν ενδιαφέροντες χώροι στη θεωρητική πληροφορική οπου αυτό είναι εφικτό σε κάθε ανώτερη διάσταση, πιό σωστά, σε κάθε ανώτερο τύπο. Το παράδειγμά μου είναι η ιεραρχία των συναφών πληροφοριοσυστημάτων Σκότ (coherent Scott information systems), που ερμηνεύουν την ιεραρχία τύπων \(\rho ::= \iota | \rho \to \rho\), για κάθε βασικό τύπο \(\iota\) που δίνεται επαγωγικά απο δομητές, όπως οι φυσικοί \(\mathbb{N}\) (δίνεται απ' τους δομητές «μηδέν» και «επόμενος»), οι μπουλιανοί \(\mathbb{B}\) (δίνεται απ' τους δομητές «αλήθεια» και «ψεύδος») και λοιπά.
Ατομικότητα ίσον γραμμικότητα
Εδώ δέ θα επεκταθώ σε ζητήματα δηλωτικής, αλλα θα γράψω για έναν χαρακτηρισμό της ατομικότητας που βρήκα στο [Bucciarelli et al 2010]. Οι Μπουκιαρέλι και σία δέ μιλάν γι' «ατομικότητα», αλλα χρησιμοποιούν μία εκδοχή πληροφοριοσυστήματων που τα καλούν γραμμικά πληροφοριοσυστήματα (linear information systems) για να στήσουν ένα μοντέλο της ιντουισιονιστικής γραμμικής λογικής. Δείχνουν μάλιστα οτι τα πεδία που επάγονται απ' τα γραμμικά πληροφοριοσυστήματα είναι τα πρώτα αλγεβρικά πεδία Σκότ (prime algebraic Scott domains), και έτσι η δουλειά τους συνδέεται και με τη δουλειά του Γκουό-Κιάν Ζάνγκ (πιχί [Zhang 1992] ή και [Zhang 1996]). Εμένα εδώ μ' ενδιαφέρει, πολύ στενά, ο ορισμός που δίνουν για το γραμμικό πληροφοριοσύστημα. Οι συγγραφείς δέν το κάνουνε λιανά, αλλα ο ορισμός τους αντιστοιχεί όντως στην έννοια ενός πληροφοριοσυστήματος οπου κάθε γειτονιά είναι ατομική, και αυτό θέλω να δείξω εδωπέρα.
Ένα πληροφοριοσύστημα Σκότ είναι μία τριάδα \(\newcommand{\Tok}{\mathrm{Tok}}\newcommand{\Con}{\mathrm{Con}}(\Tok, \Con, \vdash)\). Τα στοιχεία του \(\Tok\) τα σκεφτόμαστε ώς ατομικές πληροφορίες ή άτομα, τα στοιχεία του \(\Con\) είναι περατοσύνολα ατόμων που σκεφτόμαστε ώς συνεπή σύνολα (consistent sets) ή, για τοπολογικούς λόγους που δέ θα πιάσω, ως (τυπικές) γειτονιές (formal neighborhoods), και \(\vdash\) είναι μία σχέση τύπου \(\Con \times \Tok\), που εκφράζει την ενοχή ή μετάδοση της πληροφορίας: άν \(U \vdash b\), τότε λέμε οτι η πληροφορία που εκφράζει το \(U\) ενέχει (δόκιμος όρος) την ατομική πληροφορία που εκφράζει το \(b\). Τα άτομα, η συνέπεια και η ενοχή, οφείλουν να ικανοποιούν τα εξής αξιώματα:\[\begin{align} (1)\quad & \{a\} \in \Con \ ,\\ (2)\quad & U \in \Con \land V \subseteq U \to V \in \Con \ ,\\ (3)\quad & U \in \Con \land a \in U \to U \vdash a \ , \\ (4)\quad & U, V \in \Con \land U \vdash V \land V\vdash c \to U \vdash c \ ,\\ (5)\quad & U \in \Con \land U \vdash b \to U \cup \{b\} \in \Con \ ,\end{align}\] οπου \(U, V \subseteq^{f}\Tok\) και \(a, b, c \in \Tok\) και οπου γράφουμε \(U \vdash V\) αντί για \(\forall_{b \in V}U \vdash b\). Επιπλέον, λέμε οτι έχουμε ένα ατομικό πληροφοριοσύστημα άν η ενοχή είναι ατομική:\[\begin{align}(6)\quad & U \in \Con \land U \vdash b \to \exists_{a \in U}\{a\} \vdash b \ .\end{align}\]Σε ένα πληροφοριοσύστημα, η ατομική ενοχή συνεπάγεται και την ενοχή, ωστε ισχύει και το αντίστροφο του (6). Άς το κάνουμε λημματάκι αυτό.
Λήμμα. Άν \(U \in \Con\) και \(\{a\} \vdash b\), για κάποιο \(a \in U\), τότε \(U \vdash b\).
Απόδειξη. Απ' το (3) έχουμε οτι \(U \vdash a\), οπότε το (4) μας δίνει το ζητούμενο. Τέλος.
Οι ισχυρισμοί (1) έως (5) είναι η στάνταρ αξιωματικοποίηση των πληροφοριοσυστημάτων Σκότ απ' το [Larsen, Winskel 1991] και μετά (που διαφέρει κατά τι απ' το ορίτζιναλ [Scott 1982]). Ο ισχυρισμός (6) είναι θά 'λεγα η αυθόρμητη αξιωματική επιλογή αν θές να μιλήσεις για ατομικότητα πατώντας στα (1) έως (5). Αυτός όμως δέν είναι ο μόνος τρόπος να πιάσεις την ατομικότητα. Πατώντας στην διαίσθηση του λήμματος και παίρνοντας στα σοβαρά οτι «η ατομική ενοχή πρόκειται στην τελική για μιά διμελή σχέση ατόμων», μπορείς ν' αλλάξεις τη λογική δομή του πληροφοριοσυστήματος: αντί για \(\vdash \subseteq \Con \times \Tok\) πάρε \(\vdash \subseteq \Tok \times \Tok\), και προσάρμοσε τα αξιώματα αναλόγως. Αυτό ακριβώς κάνανε οι Μπουκιαρέλι ϗ σία. Παρεμπιπτόντως, αυτό ακριβώς έκανα και γώ όταν εξέταζα πληροφοριοσυστήματα που είναι μαζί καί ατομικά καί συναφή (οπου «συνάφεια» σημαίνει οτι και το κατηγόρημα \(\Con\) ξεπέφτει σε μία διμελή σχέση, βλέπε σχόλια παρακάτω), αλλ' αυτό θα μας πάει αλλού.
Ορίζουμε λοιπόν ένα γραμμικό πληροφοριοσύστημα να είναι μία τριάδα \((\Tok, \Con, \geq)\), οπου η σχέση \(\geq\) τώρα είναι μία διμελής σχέση στο \(\Tok\) (δέ γράφω πάλι \(\vdash\) για να μή μπερδέψουμε τα μπούτια μας στα επόμενα), και που υπόκειται στα εξής αξιώματα:\[\begin{align} (1')\quad & \{a\} \in \Con \ ,\\ (2')\quad & U \in \Con \land \forall_{b \in V} \exists_{a \in U} a \geq b \to V \in \Con \ ,\\ (3')\quad & a \geq a \ ,\\ (4')\quad & a \geq b \land b \geq c \to a \geq c \ .\end{align}\]Η διαισθητική βάση της όλης ανάπτυξης των Μπουκιαρέλι ϗ σία είναι οτι η γραμμικότητα πράγματι χαρακτηρίζει την ατομικότητα σε παραδοσιακά πληροφοριοσυστήματα. Αυτό ας το κάνουμε ένα θεωρηματάκι.
Θεώρημα. Άν \((\Tok, \Con, \geq)\) είναι γραμμικό πληροφοριοσύστημα, τότε η τριάδα \((\Tok, \Con, \vdash)\), οπου\[U \vdash b := U \in \Con \land \exists_{a \in U} a \geq b \ ,\]είναι ατομικό πληροφοριοσύστημα. Αντίστροφα, άν \((\Tok, \Con, \vdash)\) είναι ατομικό πληροφοριοσύστημα, τότε η τριάδα \((\Tok, \Con, \geq)\), με\[a \geq b := \{a\} \vdash b \ ,\]είναι γραμμικό πληροφοριοσύστημα.
Απόδειξη. Ας είναι \((\Tok, \Con, \geq)\) ένα γραμμικό πληροφοριοσύστημα. Το (1) το παίρνουμε απο το (1'). Για το (2), ας είναι \(U \in \Con\) και \(V \subseteq U\)· απ' το (3') έχεις οτι \(b \geq b\) για κάθε \(b \in V\), και αφού \(V \subseteq U\), το (2') σου δίνει οτι \(V \in \Con\). Για το (3), ας είναι \(U \in \Con\) και \(a \in U\)· τότε παίρνεις \(U \vdash a\) απ' την (3') και τον ορισμό της \(\vdash\). Για το (4), ας είναι \(U, V \in \Con\) με \(U \vdash V\) και \(V \vdash c\)· απ' τον ορισμό της \(\vdash\), αυτό σημαίνει οτι υπάρχει \(b_c \in V\) με \(b_c \geq c\) και τότε υπάρχει και \(a_{b_c} \in U\) με \(a_{b_c} \geq b_c\)· η (4') και ο ορισμός της \(\vdash\) μας δίνουν οτι \(U \vdash c\). Για το (5), ας είναι \(U \in \Con\) και \(U \vdash b\)· απ' το (3) έχουμε ήδη οτι \(U \vdash a\) για κάθε \(a \in U\), και ο ορισμός της
\(\vdash\) μας λέει τελικά πως για κάθε \(c \in U\cup\{b\}\), υπάρχει \(a_c \in U\) με \(a_c \geq c\)· το (2') τότε μας δίνει \(V \in \Con\). Τέλος, για το (6), ας είναι \(U \in \Con\) και \(U \vdash b\)· απ' τον ορισμό της \(\vdash\) (έ, κι απ' το (1) επίσης), παίρνεις οτι υπάρχει \(a \in U\) με \(\{a\} \vdash b\). Το \((\Tok, \Con, \vdash)\) είναι λοιπόν ατομικό πληροφοριοσύστημα.
Αντίστροφα, ας είναι \((\Tok, \Con, \vdash)\) ατομικό πληροφοριοσύστημα.Το (1') το έχουμε πάλι απευθείας απ' το (1). Για το (2'), ας είναι \(U \in \Con\) και υπόθεσε οτι για κάθε \(b \in V\) υπάρχει κάποιο \(a \in U\) ωστε νά 'ναι \(a \geq b\)· ο ορισμός της \(\geq\) σου λέει οτι για τέτοια \(b\) και \(a\) είναι \(\{a\} \vdash b\)· απ' το (6) και το Λήμμα, παίρνουμε οτι για κάθε \(b \in V\) είναι \(U \vdash b\)· το (5) τότε μας λέει πως \(U \cup V \in \Con\) και έτσι το (2) μας δίνει οτι \(V \in \Con\). Για το (3'), για οποιοδήποτε \(a\) έχουμε βέβαια οτι \(\{a\} \in \Con\) απ' το (1') ήδη, και τότε το (3) και ο ορισμός της \(\geq\) σου δίνουν οτι \(a \geq a\). Τέλος, για την (4'), ας είναι \(a \geq b\) και \(b \geq c\)· απ' τον ορισμό της \(\geq\) και το (4) παίρνουμε οτι \(a \geq c\). Άρα όντως, το \((\Tok, \Con, \geq)\) είναι γραμμικό πληροφοριοσύστημα. Τέλος.
Σχόλια
Το ωραίο με το χαρακτηρισμό της ατομικότητας κατα Μπουκιαρέλι ϗ σία είναι βέβαια οτι έχουμε οικονομικότερη περιγραφή (τέσσερα ψωροαξιώματα έναντι των αρχικών έξι). Για περαιτέρω χώνεμα της ισοδυναμίας ατομικών και γραμμικών πληροφοριοσυστημάτων, μπορεί κανείς να παίξει πεδιοθεωρητικά, και να δείξει οτι τα αντίστοιχα επαγόμενα πεδία είναι ισόμορφα (τί «ισόμορφα»; τα ίδια...), καθώς και κατηγοριοθεωρητικά, και να δείξει οτι οι αντίστοιχες κατηγορίες (με κατάλληλα ορισμένες προσεγγίσιμες απεικονίσεις για μορφισμούς κάθε φορά) είναι ισόμορφες.
Ένα άλλο πόιντ είναι ο συσχετισμός των γραμμικών πληροφοριοσυστημάτων του [Bucciarelli et al 2010] με τα πρώτα πληροφοριοσυστήματα του [Zhang 1992] (που πρωτύτερα τα έλεγε ευσταθή πληροφοριοσυστήματα [Zhang 1989]). Τα δέ, είναι ατομικά πληροφοριοσυστήματα που επιπλέον ικανοποιούν την εξής ιδιότητα:\[\begin{align}(7)\quad & U \in \Con \to \exists_{m \in \mathbb{N}}\exists^{m}_{b \in \Tok}U \vdash b \ ,\end{align}\]παναπεί, ο απαγωγικός κλεισμός κάθε γειτονιάς είναι περατός. Ακόμη πιό χοντρή ιδιότητα αυτή για ένα πληροφοριοσύστημα, αναγκαία ωστόσο, μας λέει ο Ζάνγκ, αν θέλουμε να αναπαραστήσουμε τα dI-πεδία με πληροφοριοσυστήματα. Καθώς τα dI-πεδία είναι ειδική περίπτωση πρώτων αλγεβρικών πεδίων, έπεται οτι όπως έχουμε πρώτα αλγεβρικά πεδία ανάμεσα στα ενγένει πεδία και στα dI-πεδία, έτσι οφείλουμε νά 'χουμε ατομικά (ή «γραμμικά») πληροφοριοσυστήματα ανάμεσα στα ενγένει πληροφοριοσυστήματα και στα πρώτα πληροφοριοσυστήματα του Ζάνγκ. Ενδιαφέρον είναι να βρούμε επιπλέον τη θέση της συνάφειας μέσα σ' όλ' αυτά, που μιά και τό 'φερ' η κουβέντα θα την γράφαμε\[\begin{align}(8)\quad & \forall_{a,a' \in U}\{a, a'\} \in \Con \to U \in \Con \ ,\end{align}\]καθώς, βέβαια, και ν' αφηγηθούμε την όλη ιστορία απ' την οπτική της έννοιας της σειραϊκότητας, που θά 'δινε την (ιστορικά) σωστή διαίσθηση. Μα νόν αντέσο.
Ένα τελευταίο νότα μπένε: στην τρέχουσα βερσιόν του πέιπερ στο άρκιβ [Mon, 29 Mar 2010 12:13:18 GMT (22kb)], ο ορισμός του (γενικού, μή γραμμικού) πληροφοριοσυστήματος που δίνουν οι συγγραφείς στην ενότητα 3 είναι ελλιπής, αφού δέν αρκεί για να παράξει το αξίωμα (5). Η βαρύτητα της συγκεκριμένης εργασίας πάντως πέφτει στη γραμμική περίπτωση, οπου όπως είδαμε το (5) μπορεί να συναχθεί απο τα άλλα αξιώματα, και η παράλειψη της ενότητας 3 δέ θα πρέπει να επηρεάζει τα κύρια θεωρήματά τους. Άλλωστε, η ενότητα αποσκοπεί ακριβώς στο να συσχετίσει το γραμμικό μοντέλο με τη μή γραμμικό, άρα η παράλειψη το πολύ ν' αφορά το συσχετισμό αυτό και μόνον.
