MathJax

Παρασκευή 22 Ιουλίου 2016

«Αποτελεσματικότητα και ολικότητα»

Στο πολύ ωραίο (και αρκετά λάιτ) αρθράκι [Berger 1999], πρόδρομο του --πάνω-κάτω ίδιου-- [Berger 2002], ο Ούλριχ Μπέργκερ γράφει μιά πολύ συνοπτική, αλλα αρκετά ζουμερή ρετροσπεκτίβα της ανώτερης υπολογισιμότητας μέσω πεδίων Σκότ, και συγκεκριμένα όσον αφορά τα δύο κομβικά θέματα της αποτελεσματικότητας (effectivity/effectiveness) και της ολικότητας (totality).



1

Στην εισαγωγή παραθέτει τα βασικά της θεωρίας πεδίων, και δή, ορίζει την έννοια του πεδίου (Σκότ) ως διάταξης με ελάχιστο στοιχείο, η οποία έχει αριθμήσιμη βάση, είναι αλγεβρική, και είναι κατευθυνόμενα και συνεπώς πλήρης --ελλείψει ελάχιστου στοιχείου μιλάει για οιονεί πεδία (quasi-domains)--, ενώ επίσης περιορίζει την ανάπτυξή του στα συναφή πεδία. Εισάγει την ιεραρχία των μερικών συνεχών συναρτησιακών \( \{D_\rho\}_\rho \), για \( \rho \) περατούς τύπους, και επικεντρώνεται στην περίπτωση της ιεραρχίας πάνω στους ισόπεδους, (flat) φυσικούς \( \mathbb{N}^\bot = \mathbb{N} \cup \{\bot\} \) και στους πραγματικούς \( \mathbb{R} \) που παίρνονται ως ιδεωδική πλήρωση της διάταξης των (επεκταμένων) διαστημάτων \( [a, b] \) με \( a, b \in \mathbb{Q} \cup \{-\infty, \infty\} \) και \( a \leq b \) (\( \mathbb{Q} \) οι ρητοί).

2

Στη δεύτερη ενότητα ξεκινάει με την αποτελεσματικότητα. Ένα αποτελεσματικό πεδίο είναι ένα πεδίο \( (D, \sqsubseteq) \) εφοδιασμένο με μία αρίθμηση (numbering, Nummerierung) \( \nu_0 : \mathbb{N} \to D \), η οποία ικανοποιεί τα εξής: (i) τα σύνολα \[ \{ (m, n) \in \mathbb{N} \times \mathbb{N} \mid \nu_0(m) \sqsubseteq \nu_0(n)\}, \  \{ (m, n) \in \mathbb{N} \times \mathbb{N} \mid \nu_0(m) \uparrow \nu_0(n)\} \] είναι αποφασίσιμα, και (ii) υπάρχει αναδρομική συνάρτηση \( f : \mathbb{N} \times \mathbb{N} \to^{rec} \mathbb{N} \) τέτοια ωστε\[ m \uparrow n \to \nu_0(f(m, n)) = \nu_0(m) \sqcup \nu_0(n) \]για κάθε \( m, n \in \mathbb{N} \). Ένα στοιχείο \( x \in D \) λέγεται τότε (πεδιοθεωρητικά) υπολογίσιμο, γράφε \( x \in D^{comp} \), άν το σύνολο \( \{ m \mid \nu_0(m) \sqsubseteq x \} \) των δεικτών των προσεγγίσεών του είναι αναδρομικά απαριθμήσιμο. Με στάνταρ εργαλεία, λέει, της στοιχειώδους θεωρίας υπολογισιμόητας, η αριθμησιμότητα περνάει και σε σύνθετα πεδία αφενός, και αφετέρου (πιχί, με χρήση αγκυλών Κλέινι) μπορείς να ορίσεις αρίθμηση \( \nu : \mathbb{N} \to D^{comp} \) τέτοια ωστε (i) το σύνολο\[ \{ (m, n) \in \mathbb{N} \times \mathbb{N} \mid \nu_0(m) \sqsubseteq \nu(n) \} \]νά 'ναι αποφασίσιμο, (ii) να υπάρχει αναδρομική συνάρτηση \( g : \mathbb{N} \to^{rec} \mathbb{N} \) τέτοια ωστε\[ \nu_0(m) = \nu \circ g(m) \] για κάθε \( m \in \mathbb{N} \) και (iii) για κάθε άλλη αρίθμηση \( \nu' : \mathbb{N} \to D^{comp} \) που ικανοποιεί τα (i) και (ii) να υπάρχει αναδρομική συνάρτηση \( h : \mathbb{N} \to^{rec} \mathbb{N} \) τέτοια ωστε\[ \nu'(m) = \nu \circ h (m) \]για κάθε \( m \in \mathbb{N} \). Τέλος, μία αποτελεσματική διαδικασία \( f : D \to^{eff} E\) είναι ένα ζεύγος απο απεικονίσεις \( f : D^{comp} \to E^{comp} \) και \( \hat{f} : \mathbb{N} \to^{rec} \mathbb{N} \) τέτοιες ωστε να ισχύει\[ f \circ \nu_D (m) = \nu_E \circ \hat{f} (m) \]για κάθε \( m \in \mathbb{N} \).

Κατόπιν επικεντρώνεται στα μερικά υπολογίσιμα συναρτησιακά πάνω στους ισόπεδους φυσικούς, και εφιστά γι' αυτά την προσοχή στη διάκριση μεταξύ πεδιοθεωρητικής υπολογισιμότητας, PCF-υπολογισιμότητας και S1-S9-υπολογισιμότητας, και παραθέτει βασικά αποτελέσματα:
  1. Πλάτεκ: Ένα μερικό συνεχές συναρτησιακό είναι PCF-υπολογίσιμο άν και μόνο άν είναι S1-S9-υπολογίσιμο.
  2. Ορισιμότητα Πλότκιν: Υπάρχει μερικό συνεχές συναρτησιακό που είναι πεδιοθεωρητικά υπολογίσιμο αλλα όχι PCF-υπολογίσιμο (το γνωστό ζήτημα με τα παράλληλα συναρτησιακά).  Περαιτέρω, ένα μερικό συνεχές συναρτησιακό είναι πεδιοθεωρητικά υπολογίσιμο άν και μόνο άν είναι (PCF+POR+PE)-υπολογίσιμο (οπου POR είναι η παράλληλη διάζευξη και PE η παράλληλη υπαρξιακή ποσόδειξη).
  3. Γενίκευση Ράις-Σαπίρο: Ας είναι \( \mathcal{U} \subseteq D^{comp} \) σύνολο υπολογίσιμων συναρτησιακών. Άν το σύνολο \( \{ m \mid \nu(m) \in \mathcal{U} \} \) είναι ημιαποφασίσιμο τότε το σύνολο \( \mathcal{U} \) είναι ανοιχτό κατα Σκότ στο \( D^{comp} \).
  4. Γενίκευση Μάιχιλ-Σέπερντσον: Κάθε αποτελεσματική διαδικασία μεταξύ αποτελεσματικών πεδίων είναι συνεχής κατα Σκότ, απ' όπου: υπάρχει αποτελεσματική ισομορφία μεταξύ υπολογίσιμων μερικών συνεχών συναρτησιακών και μερικών αποτελεσματικών διαδικασιών.

3

Στην επόμενη ενότητα περνάει στην ολικότητα, την οποία αναλύει πολύ όμορφα και επεξηγηματικά με τοπολογικο-πεδιοθεωρητικούς όρους --άλλωστε, τέτοια ακριβώς ήταν και η βάση στην οποία είχε ήδη στηρίξει τη διατριβή του. Δανείζεται απ' τον Νόρμαν την έννοια του πεδίου με ολικότητα, που δίνεται ως ένα πεδίο \( D \) μαζί με ένα υποσύνολο \( \overline{D} \subseteq D \) που ονομάζει ολικότητα του \( D \), και είναι τέτοιο ωστε (i) το \( \overline{D} \) να είναι κλειστό προς τα πάνω, δηλαδή\[ x \in \overline{D} \land x \sqsubseteq y \to y \in \overline{D} \]για κάθε \( x, y \in D \) (αυτό που είναι γνωστό και ώς «λήμμα επέκτασης»), και (ii) η συνέπεια να είναι μεταβατική, άρα και ισοδυναμία στο \( \overline{D} \), δηλαδή να έχεις\[ x \uparrow y \land y \uparrow z \to x \uparrow z\]για κάθε \( x, y, z \in \overline{D} \). Τη συνθήκη (ii) την δικαιολογεί ήδη με τοπολογικούς όρους: δύο ολικά είναι συνεπή άν και μόνο άν δέν είναι διαχωρίσιμα, αρχή η οποία συνάδει με την εδραιωμένη τοπολογική ερμηνεία αλα Σμίθ (Smyth) των ανοιχτοσυνόλων ως παρατηρήσιμων ιδιοτήτων.

Γράφει τις κλάσεις και τα πηλίκα με παχιά, άρα \( \mathbf{x} \in \mathbf{D} \) δηλώνει \( \{ x' \in \overline{D} \mid x' \uparrow x \} \in \overline{D} / \uparrow\), για δοσμένο \( x \in \overline{D} \). Σε περίπτωση που το \( D \) είναι αποτελεσματικό τότε επάγεται μία έννοια υπολογισιμότητας απ' το \( D \) στο \( \mathbf{D} \): λέμε οτι η κλάση \( \mathbf{x} \in \mathbf{D} \) είναι πεδιοθεωρητικά ή PCF υπολογίσιμη όταν περιέχει ένα αντίστοιχα υπολογίσιμο στοιχείο.

Το ζήτημα τώρα είναι ποιά η επαγωγική συμπεριφορά της ολικότητας, μ' άλλα λόγια, άν αυτή διατηρείται κατα την εκθετοποίηση, κατα την κατασκευή δηλαδή των χώρων συναρτήσεων: άν \( D \) και \( E \) είναι δύο πεδία με ολικότητα, τότε τί γίνεται με την ολικότητα του χώρου συναρτήσεων \( D \to E \); Η προφανής και φυσιολογική απάντηση είναι να πείς οτι\[ \overline{D \to E} := \{ f \in D \to E \mid \forall_{x \in \overline{D}} f(x) \in \overline{E} \} \](το οποίο μπορούμε να συμβολίσουμε και με \( \overline{D} \to \overline{E} \)), οτι δηλαδή η ολικότητα του χώρου συναρτήσεων θ' απαρτίζεται απο εκείνες τις συναρτήσεις που διατηρούν την ολικότητα. Ο ορισμός όμως παρουσιάζει ενγένει προβλήματα, καθώς δέν εγγυάται οτι η συνέπεια θα είναι μεταβατική ή οτι θα έχεις την ιδιότητα της εκτατικότητας\[ \forall_{x \in \overline{D}} f(x) \uparrow g(x) \leftrightarrow f \uparrow g \]για κάθε \( f, g \in \overline{D \to E} \). Ώς αντιπαράδειγμα δίνει ο Μπέργκερ την περίπτωση της ιεραρχίας πάνω στους ισόπεδους φυσικούς, οπου ώς ολικότητα του πεδίου \( \mathbb{N}^\bot \) έχει επιλεχθεί απλώς το μονοσύνολο \( \{ 0 \} \): στο σύνολο \( \overline{\mathbb{N}^\bot \to \mathbb{N}^\bot} \) θα συνυπάρχουν εξορισμού συναρτήσεις όπως η \(\lambda_x \mathsf{if}(x=0,0,52)\) και η \( \mathsf{id_{\mathbb{N}^\bot}} \), οι οποίες καί τη μεταβατικότητα βλάπτουν, αλλα καί την επάνω επιθυμητή ιδιότητα.

Έτσι φτάνει στην αναγκαιότητα της πυκνότητας: ένα σύνολο \( M \subseteq D \) θα είναι πυκνό στο \( D \) όταν\[ \forall_{x \in D} \exists_{x_m \in M} x \sqsubseteq x_m .\]Μ' αυτήν την έξτρα υπόθεση ικανοποιούνται καί η διατήρηση της ολικότητας κατα την επαγωγή, καί η ιδιότητα της εκτατικότητας των ολικών. Και γιατί μιλάμε για «εκτατικότητα»; γιατι απ' το παραπάνω, θεωρώντας δύο ολικά αντικείμενα ισοδύναμα εάν είναι συνεπή, παίρνεις\[ \mathbf{f} = \mathbf{g} \leftrightarrow \forall_{\mathbf{x} \in \overline{D}} \mathbf{f}(\mathbf{x}) = \mathbf{g}(\mathbf{x})\]για κάθε \( f, g \in \overline{D \to E} \), οπου με \( \mathbf{f} (\mathbf{x}) \) εννοείται η κλάση ισοδυναμίας της τιμής \( f(x) \). Το μόνο πρόβλημα που παραμένει είναι να εξασφαλιστεί οτι και η ιδιότητα της πυκνότητας θα διατηρείται κατα την επαγωγή. Το αντιπαράδειγμα που φέρνει εδωπέρα είναι η περίπτωση να έχεις πάλι την ιεραρχία πάνω στους ισόπεδους φυσικούς, και να θεωρήσεις τα πεδία \( D, E = \mathbb{N}^\bot \) με αντίστοιχες ολικότητες \( \overline{D} = \mathbb{N}^\bot \) και \( \overline{E} = \mathbb{N} \): τότε το σύνολο \( \overline{D \to E} \) θα περιέχει αναγκαστικά μόνο σταθερές συναρτήσεις, άρα δέν υπάρχει ελπίδα να ειναι πυκνό στον \( D \to E \). Σημειώνει οτι το πρόβλημα σ' αυτό το αντιπαράδειγμα είναι οτι επιλέξαμε να βρίσκεται ανάμεσα στα ολικά και το αντικείμενο \( \bot \).

Και έτσι φτάνει και στην αναγκαιότητα της διαχωριστικότητας, ή, όπως το λέει εδωπέρα, της συμπυκνότητας: ένα σύνολο \( N \subseteq D \) θα είναι σύμπυκνο στο \( D \) όταν\[ \forall_{x,y \in D^c} ( x \not\uparrow x \to \exists_{t : D \to \mathbb{B}^\bot} t(x) \not = t(y)) ,\]οπου \( D^c \) είναι το σύνολο των συμπαγών αντικειμένων του πεδίου \( D \) και \( \mathbb{B} \) είναι οι μπουλιανοί. Προσέχουμε εδωπέρα οτι η συμπυκνότητα αφορά τα συμπαγή. Πράγματι, αργότερα θα χρησιμοποιήσει τον όρο διαχωριστικότητα για την ιδιότητα μίας συνάρτησης· συγκεκριμένα, λέει μία συνάρτηση \( f : D \to E \) διαχωριστική όταν\[ x \not \uparrow y \to f(x) \not \uparrow f(y) \] για κάθε \( x, y \in D \), όταν δηλαδή διατηρεί ασυνέπειες (θυμήσου εδώ τις συνεποανακλαστικές γειτονοαπεικονίσεις που προκύπτουν κατα τη μελέτη κανονικών μορφών), ενώ την λέει πυκνή όταν το σύνολο \( f[D] \) των τιμών της είναι πυκνό στο \( E \).

Μ' αυτά και μ' αυτά, παραθέτει τα εξής αποτελέσματα.
  1. Αφηρημένη πυκνότητα (Μπέργκερ): Ας είναι \( D \) και \( E \) πεδία με ολικότητα. Άν το \( \overline{D} \) είναι σύμπυκνο και το \( \overline{E} \) πυκνό, τότε το \( \overline{D \to E} \) είναι πυκνό, ενώ άν το \( \overline{D} \) είναι πυκνό και το \( \overline{E} \) σύμπυκνο, τότε το \( \overline{D \to E} \) είναι σύμπυκνο. Απ' όπου: σε κάθε ιεραρχία \( D_\rho \) μερικών συνεχών συναρτησιακών πάνω απο ένα πεδίο με πυκνή και σύμπυκνη ολικότητα, το σύνολο \( \overline{D_\rho} \) είναι πυκνή και σύμπυκνη ολικότητα σε κάθε περατό τύπο \( \rho \).
  2. Πυκνότητα στους ισόπεδους φυσικούς: Απ' το προηγούμενο: Στην ιεραρχία \( D_\rho \), οπου \( D = \mathbb{N}^\bot \) και \( \overline{D} = \mathbb{N} \), το σύνολο \( \overline{D_\rho} \) είναι πυκνό και σύμπυκνο στο \( D_\rho \) για κάθε περατό τύπο \( \rho \).
  3. Ιεραρχία Κλέινι--Κράιζελ (Έρσοφ): Η ιεραρχία των πηλίκων \( \mathbf{D}_\rho \) του προηγούμενου είναι ισόμορφη με την ιεραρχία των συναρτησιακών Κλέινι--Κράιζελ.
  4. Πυκνότητα στους πραγματικούς (Νόρμαν): Τα ολικά συναρτησιακά \( \overline{\mathbb{R}_\rho} \) είναι πυκνά στο \( \mathbb{R}_\rho \) για κάθε περατό τύπο \( \rho \).
  5. Αποτελεσματική επιλογή (Κράιζελ): Ας είναι \( D_\rho \) η ιεραρχία των μερικών συνεχών συναρτησιακών πάνω στους ισόπεδους φυσικούς και μπουλιανούς, και \( \rho \) και \( \sigma \) οποιοιδήποτε περατοί τύποι. Υπάρχει PCF+POR-υπολογίσιμο συναρτησιακό επιλογής\[ \Gamma : (\rho \times \sigma \to \mathbb{B}) \to \rho \to \sigma \]τέτοιο ωστε για κάθε ολικό συναρτησιακό \( f : \rho \times \sigma \to \mathbb{B} \) με\[ \forall_{x \in \overline{D_\rho}} \exists_{y \in \overline{D_\sigma}} f(x, y) = \mathsf{tt} ,\]να ισχύει\[ \forall_{x \in \overline{D_\rho}} f(x, \Gamma (f, x)) = \mathsf{tt} .\]
Το θεώρημα 4 του Νόρμαν, να σημειώσουμε, δέν προκύπτει άμεσα απο το 1, και μάλιστα κύριο μέλημα του Μπέργκερ σ' αυτήν την ενότητα είναι να φτάσει σε μιά κατάλληλη γενίκευση του 4 στα πλαίσια της πεδιοθεωρίας, πράγμα που αποτελεί και το μόνο νέο αποτέλεσμα του πέιπερ --δέν μπαίνουμε εδώ σ' αυτήν τη συζήτηση.

4

Στην τέταρτη ενότητα επιστρέφει στην έννοια της αποτελεσματικότητας για να εξετάσει αυτήν τη φορά τα ολικά συναρτησιακά. Ας είναι \( D \) ένα πεδίο. Ένα σύνολο \( M \subseteq D \) θα λέγεται αποτελεσματικά πυκνό στο \( D \), όταν υπάρχει υπολογίσιμη πυκνή ακολουθία \( g : \mathbb{N} \to M \). Ένα στοιχείο \( x \in D \) λέγεται σχεδόν μέγιστο όταν\[ x \sqsubseteq y \land x \sqsubseteq y' \to y \uparrow y' \]για κάθε \( y, y' \in D \) (ώς παράδειγμα φέρνει τα στοιχεία ενός σύμπυκνου συνόλου).

Παραθέτει εδώ τα εξής αποτελέσματα.
  1. Νόρμαν: Κάθε ολικό συνεχές συναρτησιακό πάνω στους ισόπεδους φυσικούς είναι PCF-υπολογίσιμο. Επιπλέον, αν \( \rho \) είναι περατός τύπος, υπάρχει PCF-υπολογίσιμο συναρτησιακό \( \Delta : (\mathbb{N} \to \mathbb{N}) \to \rho \) τέτοιο ωστε για κάθε ολικό συνεχές συναρτησιακό \( f : \rho \) και απαρίθμηση \( f_0 : \mathbb{N} \to \mathbb{N} \) των συμπαγών προσεγγίσεων του \( f \), το \( \Delta(f_0) \) να είναι ολικό και \( \Delta(f_0) \sqsubseteq f \).
  2. Επέκταση (Μπέργκερ): Ας είναι \( D \) και \( E \) αποτελεσματικά πεδία με ολικότητα. Άν το \( \overline{D} \) είναι αποτελεσματικά πυκνό και τα στοιχεία του \( \overline{E} \) είναι σχεδόν μέγιστα, τότε κάθε ολική αποτελεσματική διαδικασία \( f \in \overline{D \to E} \) επεκτείνεται σε μία αποτελεσματική διαδικασία \( \hat{f} \in D \to E \), δηλαδή τέτοια ωστε \( f(x) \sqsubseteq \hat{f}(x) \) για κάθε \( x \in \overline{D} \). Απο τη γενίκευση του Μάιχιλ--Σέπερντσον, η \( \hat{f} \) θα είναι συνεχής.
  3. Ιεραρχία HEO: Η ιεραρχία των κληρονομικά αποτελεσματικών διαδικασιών περατού τύπου είναι αποτελεσματικά ισομορφική με την ιεραρχία των κληρονομικά υπολογίσιμων ολικών συναρτησιακών πάνω στους ισόπεδους φυσικούς.
Τα θεωρήματα 2 και 3 αποτελούν καί τα δύο γενικεύσεις του θεωρήματος Κράιζελ--Λακόμπ-Σένφιλντ (το δέ 3, συγκεκριμένα, προκύπτει απο το θεώρημα παραγοντοποίησης του Μπέργκερ, που δέν το πιάνει εδωπέρα).

5

Στην πέμπτη και τελευταία ενότητα αναφέρεται απλά στη βιβλιογραφία που επεκτείνει αποτελέσματα απο πάνω σε γενικότερα συστήματα τύπων που οδεύουν μάλιστα προς τη θεωρία τύπων του Μάρτιν-Λέβ, συγκεκριμένα σε δεσμευμένα γινόμενα και αθροίσματα καθώς και σε τελεστές οικουμενικών τύπων. Αυτά πατάνε σε δουλειά των Πάλμγκρεν και Στόλτεμπεργκ-Χάνσεν, Κρίστιανσεν και Νόρμαν, Βάγκμπε, και του ιδίου, αλλα δέν επεκτείνεται.