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

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