Ένα πρόγραμμα για τον τελεστή ελαχιστοποίησης

Μιλούσα προχθές για τη χρήση του τελεστή ελαχιστοποίησης (βήτα τάξης) ως τυπικού αντιπαραδείγματος για τη σφαλερή διαίσθηση οτι «άν ένα συναρτησιακό είναι μέγιστο, θά 'πρεπε νά 'ναι και ολικό». Στο μεταξύ έπεσα πάνω σε μιά ερώτηση στο στάκ εξτσέιντζ της πληροφορικής, σχετικά με την αποτελεσματικότητα του ενλόγω τελεστή (ή, για ν' ακριβολογούμε, μίας εκδοχής του: για κάθε κατηγόρημα στους φυσικούς παίρνουμε και έναν ανάλογο τελεστή ελαχιστοποίησης).

Η ερώτηση στο στάκ εξτσέιντζ τίθεται στα πλαίσια του κλασικού φορμαλισμού σχετικά με την αποτελεσματικότητα (τον πιάσαμε αυτόν τον φορμαλισμό και εδώ, όταν μιλούσαμε για έν' απ' τα πέιπερ του Μπέργκερ), οπου χρειάζεσαι μία αρίθμηση των ισόπεδων φυσικών που νά 'χει κάποιες συγκεκριμένες ιδιότητες, και λές έναν τελεστή απ' το \(\mathbb{N}\) στο \(\mathbb{N}\) αποτελεσματικό όταν συνοδεύεται απο μία αναδρομική συνάρτηση (εννοούμενη πάνω στους δείκτες της αρίθμησης), έτσι ωστε να καθιστά ένα συγκεκριμένο διάγραμμα (τελεστή, αναδρομικής συνάρτησης και αρίθμησης) μεταθετικό --για λεπτομέρειες, δές εδώ. Όλ' αυτά καλά και ζόρικα, αλλα κάπου εκεί έρχεται πάλι ο Μπάουερ και απαντά στην ερώτηση με το γνωστό του τρόπο: «η υπολογισιμότητα αφορά τον υπολογισμό· έ, γιατί δε χρησιμοποιείς υπολογιστή;».

Ο τελεστής ελαχιστοποίησης δεύτερης τάξης είναι μέγιστος

Είναι κοινώς γνωστό στους κόλπους της ανώτερης υπολογισιμότητας, και συγκεκριμένα στη θεωρία πεδίων, οτι ο τελεστής ελαχιστοποίησης (δεύτερης τάξης), στα αγγλικά «minimization operator», είναι παράδειγμα συναρτησιακού που ενώ είναι μέγιστο δέν είναι ολικό, ωστόσο δύσκολα να βρεί κανείς απόδειξη γι' αυτό το πράγμα. Γιά να δούμε εδώ μια απόδειξη, που πατάει πάνω στα χνάρια του παραδείγματος 8.3.2 του [Stoltenberg-Hansen & al 1994].

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

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

Η βασική τυπολογία της πιθανοθεωρίας

Με μιά στοιχειώδη διαστατική ανάλυση των βασικών εννοιών της πιθανοθεωρίας, καταλήγει κανείς στο εξής διάγραμμα:\[
\begin{matrix}
\Omega & \stackrel{e}{\longrightarrow} & \mathcal{E} \\
X\downarrow & & \downarrow Pr_X\\
\mathbb{M} & \stackrel{p_X, f_X, F_X}{\longrightarrow} & [0,1]
\end{matrix}
\]

Στρατηγικές αποτίμησης

Στη λειτουργική σημασιολογία κάθε λαμδαλογισμού, θεμελιακό ρόλο παίζουν οι στρατηγικές αποτίμησης: με ποιά σειρά αποτιμούμε τα μέρη, δηλαδή τους υποόρους ενός δοσμένου όρου;

Ας περιοριστούμε στον άτυπο λογισμό λάμδα, οπου η αναγωγή βασίζεται απλά στον κανόνα της βήτα μετατροπής\[
(\lambda_x t) t' \leadsto t\mid_{x := t'},
\]και άς πάρουμε για παράδειγμα τον όρο\[t = (\lambda_x x) ((\lambda_x x)(\lambda_y (\lambda_x x) y)).\]Με σχολική ας πούμε νοοτροπία, θα λέγαμε οτι εντάξει, κάνε τις αναγωγές με όποια σειρά σου φαίνεται πιό εύκολη. Για παράδειγμα, άλλος μπορεί να σκεφτόταν\[
\begin{align*}
t &= (\lambda_x x) (\underline{(\lambda_x x)(\lambda_y (\lambda_x x) y)})\\
&\leadsto (\lambda_x x)(\lambda_y \underline{(\lambda_x x) y})\\
&\leadsto \underline{(\lambda_x x)(\lambda_y y)}\\
&\leadsto \lambda_y  y ,
\end{align*}
\]και άλλος\[
\begin{align*}
t &= (\lambda_x x) (\underline{(\lambda_x x)(\lambda_y (\lambda_x x) y)})\\
&\leadsto \underline{(\lambda_x x)(\lambda_y (\lambda_x x) y)}\\
&\leadsto \lambda_y \underline{(\lambda_x x) y}\\
&\leadsto \lambda_y  y .
\end{align*}
\]Πώς να υλοποιήσουμε όμως μια τέτοια αποτίμηση με έναν ομοιόμορφο τρόπο;

Συναρτησιακά υποψιασμένα με τις προσεγγίσεις

Καταρχήν, θυμήσου αυτό το ωραίο πόστ του Μπάουερ. \(\newcommand{\ite}{\mathrm{if}}\newcommand{\Con}{\mathrm{Con}}\newcommand{\Tok}{\mathrm{Tok}}\) 

Κουζίνα της μάγισσας 1971

Ξαναμφανίστηκε γιατι πέθαινε. Αυτό ηταν. Με την ευκαιρία όμως ξαναβρήκα το δαγκωνιάρικο κειμενάκι του μ' αφορμή το θεώρημα Ρίμαν-Ρόχ ---καθότι κλασικά, τον θάβουμε, και ξεθάβουμ' ότι δικό του.

Ότι και να πώ για τη μαρτυρία αυτή του λυσσαλέου αυτού τύπου, του κάργα «τό 'πε και τό 'κανε», θ' ακουστώ λουντέμης. Άρ' απλά 'α το μεταφράσω 'πως μπορώ.

Θεώρημα Ρίμαν-Ρόχ: η τελευταία κραυγή: το διάγραμμα είναι μεταθετικό! Προκειμένου να δώσω σ' αυτόν τον ισχυρισμό για την \(f:X \to Y\) ένα προσεγγιστικό  ν ό η μ α , έπρεπε πρώτα για δύο ώρες να καταχραστώ την υπομονή των ακροατών. Σ' ασπρόμαυρο (στα Lecture Notes του Springer) παίρνει άνετα 400, 500 σελίδες. Ένα συναρπαστικό παράδειγμα για το πώς ο πόθος μας για γνώσεις και ανακαλύψεις ξεθυμαίνει όλο και περισσότερο μές στο αποξενωμένο λογικό παραλήρημα, ενώ η ίδια η ζωή πάει με χιλιάδες τρόπους κατα διαόλου ---και απειλείται με τελειωτικό αφανισμό. Ώρα ν' αλλάξουμε πορεία!

(6/12/1971)                      Αλεξάντερ Γκρότεντικ

Aτομικότητα κατα Μπουκιαρέλι ϗ σία

Η έννοια της ατομικότητας της πληροφορίας είν' απ' τα πράγματα που μ' έχουν στοιχειώσει στο παρελθόν, κι' ακόμα με στοιχειώνουν. Λές οτι ένα σύνολο \(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)\), αλλα κανένα απο τα διανύσματα αριστερά δέν αρκεί για να παράξει απο μόνο του το διάνυσμα στα δεξιά.

Αφελής θεωρία αποδείξεων

Ακούγεται περίεργο, αλλα υπάρχουν άνθρωποι που κάνουν μαθηματικά στα σοβαρά, στα σχολεία και στα πανεπιστήμια, που για καιρό δέν συνειδητοποιούν οτι, απο λογική άποψη, σε όλα τα μαθηματικά υπάρχουν έξι (6) μορφές ισχυρισμών όλες κι όλες. (Σε όλα;... όχι, όχι σε όλα, αλλα άν κάποιος φτάσει να μελετάει τροπικές λογικές φερειπείν, τότε έχει ήδη πολύ καλά υπόψη του όλ' αυτά που γράφω παρακάτω.) Το αποτέλεσμα είναι να κολλάνε συχνά όταν πρωτοαντιμετωπίζουν έναν ισχυρισμό, ειδικά σε κλάδους στους οποίους δέν έχουν αναπτύξει ακόμη καλή διαίσθηση, και να μπερδεύονται, όχι γιατι ο ισχυρισμός είναι απαραίτητα βαθύς ή δύστροπος, αλλα γιατι η λογική του μορφή παραμένει γι' αυτούς ανεξιχνίαστη.

Μερίδιο της ευθύνης γι' αυτήν την έλλειψη οικειότητας με τη βασική λογική κουβαλάει η γνωστή καταδίκη του φορμαλισμού απο πολλούς ενεργούς μαθηματικούς, μία στάση που αναπόφευκτα έχει διαποτίσει και τα λογής-λογής προγράμματα σπουδών. Μα σκέψου έναν σκακιστή να σου λέει: «Σκάκι σημαίνει "τυφλό σκάκι". Ασφαλώς και μπορούμε να παίξουμε κάθε παρτίδα στη σκακιέρα, αλλα η παρτίδα υπάρχει ανεξάρτητα απ' τη σκακιέρα, άρα δέ χρειαζόμαστε κάν σκακιέρες... ΈΞΩ ΟΙ ΣΚΑΚΙΕΡΕΣ ΑΠ' ΤΟ ΣΚΑΚΙ!» Άντε πάνε να κάνεις ανάλυση μετά, για στρατηγικές των νί κινήσεων, χωρίς να στήσεις μπροστά σου τα πιόνια. Δέ λέω, η αντίποδη στάση είναι εξίσου για μπάτσες: «ναί, σε παίζω μιά παρτίδα, αλλα θα φέρω τη σκακιέρα μου, με πιόνια γαλάτες και ρωμαίους, με άλλες δέ ξέρω να παίζω...» Ο φορμαλισμός, σε πρώτη φάση, δέν είναι παρα η σκακιέρα των μαθηματικών· τίποτε παραπάνω, τίποτε λιγότερο. Και μιά και μιλάμε για διδασκαλία, μεταξύ άλλων, άς ρωτήσουμε δασκάλους του σκακιού αν ένα παιδί θα μάθει καλύτερο σκάκι αποφεύγοντας συστηματικά το παίξιμο πάνω στη σκακιέρα.

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

«Αποδείξεις και τύποι»

Ξεκινάμε με τον Ζιράρ. Όχι γιατί ο Ζιράρ κι εγώ δε ξέρω τί, απλά, έκατσε εδώ και δυό-τρεις μέρες και βρήκα καλή αφορμή (έχω να γράψω ένα σχετικό ριβιού) να πιάσω επιτέλους σοβαρά το [Girard et al 1989]. Τον τύπο τον έχω αποφύγει ολ' αυτά τα χρόνια, κυρίως απο τεμπελιά, αλλα και κάτι λόγω δυσανεξίας στη γνωστή και γραφική πλέον γαλλιά –ξές, αυτός ο γλωσσικός εθνάρεσκος αυτοαποκλεισμός που θυμίζει ελληναριό: ιστοσελίδες αποκλειστικά στα γαλλικά, κιτσάτοι γαλλισμοί σε αγγλικά κείμενα, και άλλες τέτοιες καγκουριές.

Ε λοιπόν, παρά τις γαλλιές το βιβλίο διαβάζεται νεράκι. Αφενός γιατί δέ χάνεται στις λεπτομέρειες, κι αφετέρου λόγω γαλλιάς καλώς εννοούμενης: ο Ζιράρ τό 'χει με το μπλαμπλά, και δέν εχει πέσει και στη λούμπα της πολιτικής ορθότητας που μαστίζει το σινάφι απ' άκρη σ' άκρη. Γουστάρεις να τον διαβάζεις κι ας μή συμφωνείς. Ο συνδυασμός αυτών των δύο πάντως είναι επικίνδυνος: μπορεί κανείς να το ξεφυλλίσει σε μεγάλο βαθμό, παραλείποντας κάθε απόδειξη, και στο τέλος, χωρίς να έχει σκοντάψει συχνά, να έχει την αίσθηση οτι κάτι έκανε· στην πραγματικότητα, είναι πολύ πιθανό να έχει απλά αποκομίσει καναδυό τρία συνθήματα, που δέ θα μπορέσει να υποστηρίξει αν χρειαστεί. Αλλα εντάξει, αυτή ειναι η γνωστή ιδιοτροπία του καλογραμμένου μαθηματικού κειμένου, οτι διαβάζεται και σάν εφημερίδ' απο παιδί: μόνο τις γελοιογραφίες.