Καταρχήν, θυμήσου αυτό το ωραίο πόστ του Μπάουερ. \(\newcommand{\ite}{\mathrm{if}}\newcommand{\Con}{\mathrm{Con}}\newcommand{\Tok}{\mathrm{Tok}}\)
Στην περίπτωση που δουλεύουμε στα πλαίσια γλωσσολογισμού που στηρίζει το σύνολο της θεωρίας πεδίων, με την έννοια οτι πιάνει όχι μόνο τα αντικείμενα των πεδίων αλλα και τις προσεγγίσεις των αντικειμένων, ανοίγει, δυνητικά, πεδίο δόξης λαμπρό για τη μελέτη μικτών συναρτησιακών: συναρτησιακών τυπωμένων κατα τη γραμματική\[\tilde\rho ::= \rho \mid \Tok_\rho \mid \Con_\rho,\]οπου \(\rho\) είναι ένας συνήθης τύπος. Μία τέτοια μελέτη ασφαλώς θα επιτρέψει επιτέλους να γίνει λόγος, στο επίπεδο της γλώσσας ήδη, για το μοντέλο μαζί με τις προσεγγίσεις, άρα να ψηλαφιστούνε μοτίβα εντός μοντέλου που έως τώρα ενδεχομένως θεματοποιούνταν μόνο με διαισθητικό και υπαινικτικό τρόπο.
Για παράδειγμα, μπορείς να σκεφτείς μία διαδικασία πρώτης τάξης \(\Gamma : \iota \to \mathbb{N}\) που μετράει τις γειτονιές ενός ιδεώδους σε οποιαδήποτε περατική άλγεβρα \(\iota\). Σε κάθε περατική άλγεβρα έχεις καταρχήν την εύκολη απεικόνιση \(\sup : \Con_\iota \to \Tok_\iota\), που σου δίνει το σουπρέμουμ \(\sup(U)\) μιάς γειτονιάς \(U\). Απ' το σουπρέμουμ παίρνεις με στάνταρ (άν και ίσως τρομακτική) συνδυαστική το πλήθος των ατόμων απο κάτω του, πές με μιά απεικόνιση \(f : \Tok_\iota \to G_\mathbb{N}\). Ε τότε το πλήθος των υποσυνόλων θα δίνεται απ' την \(g := \lambda m.\ 2^m\). Θέτουμε άρα\[\Gamma := \lambda x.\ \ite(\sup (x) \neq \infty_\iota, \mathsf{S}^{g(f(\sup(x)))}\bot, \infty_{\mathbb{N}}),\]οπου με \(\infty_\iota\) εννοώ εδώ οποιαδήποτε απο τις απειρίες στην άλγεβρα \(\iota\) (στην \(\mathbb{N}\) έχουμε μία μόνο, στις \(\mathbb{U}\), \(\mathbb{B}\) καμία, αλλα στην \(\mathbb{D}\), όπως και σε κάθε άλγεβρα με υπερμονομελείς δομητές, ήδη άπειρες, και είναι βέβαια θέμα να τις συμβολίσεις συστηματικά -όχι της ώρας). Εδώ θέλει επίσης προσοχή το πώς θα ορίσεις το σούπ για ιδεώδες, οπου, ακριβώς, μπορεί να σου δίνει απειρία.
Σε κάθε περίπτωση, άν αυτή η διαδικασία \(\Gamma\) είναι εντέλει ορίσιμη με κάποιον αποδεκτό τρόπο (δέν τό βλέπω καθαρά εκεί με τον έλεγχο του σουπρέμουμ για ιδεώδη), τότε, και παρά την κραυγαλέα ασυνέχεια της \(f\), η \(\Gamma\) είναι φανερά συνεχής, άρα νά, τσάκα-τσάκα ένα συναρτησιακό υποψιασμένο με τις προσεγγίσεις. Γιατί; γιατι στήνεται με τη βοήθεια μικτών συναρτησιακών.
Έχουμε φυσιολογικά παραδείγματα σε ανώτερους τύπους; Ειδικότερα, σε τύπους τάξης \(4\) και πάνω, δίνοντας έτσι μή τετριμμένα παραδείγματα «ενδιαφέροντων συναρτησιακών» αλα Μπάουερ; Η πρώτη, αυθόρμητη ιδέα, είναι να μιλήσεις για τη δομή ενός αντικειμένου ανώτερου τύπου υπολογίζοντας συνδυαστικά μεγέθη στις προσεγγίσεις του, και φαίνεται υποσχόμενη. Μένει να εφαρμοστεί, αφενός, και αφετέρου να βρεθούν και άλλες ιδέες του πώς να μιλήσεις για τη δομή του.
Στην περίπτωση που δουλεύουμε στα πλαίσια γλωσσολογισμού που στηρίζει το σύνολο της θεωρίας πεδίων, με την έννοια οτι πιάνει όχι μόνο τα αντικείμενα των πεδίων αλλα και τις προσεγγίσεις των αντικειμένων, ανοίγει, δυνητικά, πεδίο δόξης λαμπρό για τη μελέτη μικτών συναρτησιακών: συναρτησιακών τυπωμένων κατα τη γραμματική\[\tilde\rho ::= \rho \mid \Tok_\rho \mid \Con_\rho,\]οπου \(\rho\) είναι ένας συνήθης τύπος. Μία τέτοια μελέτη ασφαλώς θα επιτρέψει επιτέλους να γίνει λόγος, στο επίπεδο της γλώσσας ήδη, για το μοντέλο μαζί με τις προσεγγίσεις, άρα να ψηλαφιστούνε μοτίβα εντός μοντέλου που έως τώρα ενδεχομένως θεματοποιούνταν μόνο με διαισθητικό και υπαινικτικό τρόπο.
Για παράδειγμα, μπορείς να σκεφτείς μία διαδικασία πρώτης τάξης \(\Gamma : \iota \to \mathbb{N}\) που μετράει τις γειτονιές ενός ιδεώδους σε οποιαδήποτε περατική άλγεβρα \(\iota\). Σε κάθε περατική άλγεβρα έχεις καταρχήν την εύκολη απεικόνιση \(\sup : \Con_\iota \to \Tok_\iota\), που σου δίνει το σουπρέμουμ \(\sup(U)\) μιάς γειτονιάς \(U\). Απ' το σουπρέμουμ παίρνεις με στάνταρ (άν και ίσως τρομακτική) συνδυαστική το πλήθος των ατόμων απο κάτω του, πές με μιά απεικόνιση \(f : \Tok_\iota \to G_\mathbb{N}\). Ε τότε το πλήθος των υποσυνόλων θα δίνεται απ' την \(g := \lambda m.\ 2^m\). Θέτουμε άρα\[\Gamma := \lambda x.\ \ite(\sup (x) \neq \infty_\iota, \mathsf{S}^{g(f(\sup(x)))}\bot, \infty_{\mathbb{N}}),\]οπου με \(\infty_\iota\) εννοώ εδώ οποιαδήποτε απο τις απειρίες στην άλγεβρα \(\iota\) (στην \(\mathbb{N}\) έχουμε μία μόνο, στις \(\mathbb{U}\), \(\mathbb{B}\) καμία, αλλα στην \(\mathbb{D}\), όπως και σε κάθε άλγεβρα με υπερμονομελείς δομητές, ήδη άπειρες, και είναι βέβαια θέμα να τις συμβολίσεις συστηματικά -όχι της ώρας). Εδώ θέλει επίσης προσοχή το πώς θα ορίσεις το σούπ για ιδεώδες, οπου, ακριβώς, μπορεί να σου δίνει απειρία.
Σε κάθε περίπτωση, άν αυτή η διαδικασία \(\Gamma\) είναι εντέλει ορίσιμη με κάποιον αποδεκτό τρόπο (δέν τό βλέπω καθαρά εκεί με τον έλεγχο του σουπρέμουμ για ιδεώδη), τότε, και παρά την κραυγαλέα ασυνέχεια της \(f\), η \(\Gamma\) είναι φανερά συνεχής, άρα νά, τσάκα-τσάκα ένα συναρτησιακό υποψιασμένο με τις προσεγγίσεις. Γιατί; γιατι στήνεται με τη βοήθεια μικτών συναρτησιακών.
Έχουμε φυσιολογικά παραδείγματα σε ανώτερους τύπους; Ειδικότερα, σε τύπους τάξης \(4\) και πάνω, δίνοντας έτσι μή τετριμμένα παραδείγματα «ενδιαφέροντων συναρτησιακών» αλα Μπάουερ; Η πρώτη, αυθόρμητη ιδέα, είναι να μιλήσεις για τη δομή ενός αντικειμένου ανώτερου τύπου υπολογίζοντας συνδυαστικά μεγέθη στις προσεγγίσεις του, και φαίνεται υποσχόμενη. Μένει να εφαρμοστεί, αφενός, και αφετέρου να βρεθούν και άλλες ιδέες του πώς να μιλήσεις για τη δομή του.
