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

Με μιά στοιχειώδη διαστατική ανάλυση των βασικών εννοιών της πιθανοθεωρίας, καταλήγει κανείς στο εξής διάγραμμα:\[
\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)                      Αλεξάντερ Γκρότεντικ