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

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

Ας περιοριστούμε στον άτυπο λογισμό λάμδα, οπου η αναγωγή βασίζεται απλά στον κανόνα της βήτα μετατροπής\[
(\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*}
\]Πώς να υλοποιήσουμε όμως μια τέτοια αποτίμηση με έναν ομοιόμορφο τρόπο;