Στη λειτουργική σημασιολογία κάθε λαμδαλογισμού, θεμελιακό ρόλο παίζουν οι στρατηγικές αποτίμησης: με ποιά σειρά αποτιμούμε τα μέρη, δηλαδή τους υποόρους ενός δοσμένου όρου;
Ας περιοριστούμε στον άτυπο λογισμό λάμδα, οπου η αναγωγή βασίζεται απλά στον κανόνα της βήτα μετατροπής\[
(\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*}
\]Πώς να υλοποιήσουμε όμως μια τέτοια αποτίμηση με έναν ομοιόμορφο τρόπο;
Ντετερμινιστικές στρατηγικές
Η παραπάνω σχολική στρατηγική - μή στρατηγική, αναφέρεται στη βιβλιογραφία ως πλήρης αναγωγή, και μπορούμε προφανώς να την κατανοήσουμε μόνο ως μή ντετερμινιστική στρατηγική. Άμα θέλουμε κάτι ντετερμινιστικό, δύο είναι οι φυσιολογικές προσεγγίσεις που έχουνε εδραιωθεί για τα καλά στην πιάτσα. Καί οι δύο πατάν στην κοινή σύμβαση οτι η αναγωγή προχωράει, καταρχήν, απο αριστερά προς τα δεξιά.
Περαιτέρω, η αναγωγή κατα κανονική σειρά (normal order) προχωράει απο έξω προς τα μέσα:\[
\begin{align*}
t &= \underline{(\lambda_x x) ((\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*}
\](οπου σε κάθε βήμα της αναγωγής παίρνεται υπόψη η προηγούμενη υπογράμμιση) και αντίθετα, η αναγωγή κατα σειρά εφαρμογής (applicative order) απο μέσα προς τα έξω:\[
\begin{align*}
t &= (\lambda_x x) ((\lambda_x x)(\lambda_y \underline{(\lambda_x x) y}))\\
&\leadsto (\lambda_x x) (\underline{(\lambda_x x)(\lambda_y y)})\\
&\leadsto \underline{(\lambda_x x) (\lambda_y y)}\\
&\leadsto \lambda_y y .
\end{align*}
\]Αυτές είναι οι δύο εύλογες και απλούστερες επιλογές ανάμεσα στις πολλαπλές επιλογές της σχολικής πλήρους αναγωγής.
Τώρα, δύο βαριάντες των επάνω παίρνουμε άν θεωρήσουμε οτι κάθε λαμδαφαίρεση είναι ήδη σε κανονική μορφή, είναι ήδη τιμή, και λειτουργεί άρα ως μαύρο κουτί, εμποδίζοντας την αναγωγή να προχωρήσει στα ενδότερα. Εδώ να κρατήσουμε ήδη ένα ερώτημα: Γιατί να το κάνουμε αυτό; γιατί η λαμδαφαίρεση να θεωρείται ανάγωγη; γιατί να θεωρείται «τιμή»;... (κρατούμενο ένα)
Η αναγωγή κατ' όνομα (call by name) προχωράει απο έξω προς τα μέσα κατα προσέγγιση λαμδαφαίρεσης:\[
\begin{align*}
t &= \underline{(\lambda_x x) ((\lambda_x x)(\boxed{\lambda_y (\lambda_x x) y}))}\\
&\leadsto \underline{(\lambda_x x)(\boxed{\lambda_y (\lambda_x x) y})}\\
&\leadsto \boxed{\lambda_y (\lambda_x x) y}
\end{align*}
\]και η αναγωγή κατα τιμή (call by value) προχωράει απο μέσα προς τα έξω κατα προσέγγιση λαμδαφαίρεσης:\[
\begin{align*}
t &= (\lambda_x x) (\underline{(\lambda_x x)(\boxed{\lambda_y (\lambda_x x) y})})\\
&\leadsto \underline{(\lambda_x x)(\boxed{\lambda_y (\lambda_x x) y})}\\
&\leadsto \boxed{\lambda_y (\lambda_x x) y} .
\end{align*}
\]
Παρσάρισμα
Στα παραπάνω, κάθε έκφραση τύπου «απο ... προς τα ...» προϋποθέτει ήδη οτι έχουμε παρσάρει τον όρο με κάποιον συμφωνημένο τρόπο. Αυτό το υπονοήσαμε ήδη μιλώντας για «μαύρα κουτιά»: πρώτα παρσάρουμε τον όρο και μετά ξεκινάμε να αποτιμούμε, και φυσικά, η διαδικασία της αποτίμησης, η αναγωγή δηλαδή, θα νοείται έτσι ωστε ν' απαγορεύεται να εισχωρεί στα μαύρα κουτιά, όποια κι αν είν' αυτά καθε φορά. Έτσι, στις περιπτώσεις των αναγωγών κατα κανονική σειρά και κατα σειρά εφαρμογής, το παρσάρισμα εισχωρεί στις λαμδαφαιρέσεις, ενώ στις περιπτώσεις των αναγωγών κατ' όνομα και κατα τιμή, όχι.
Παραστατικότερα, πλαισιώνοντας τους υποόρους που κατα περίπτωση θεωρούνται μαύρα κουτιά, βλέπουμε στις μέν περιπτώσεις τον όρο \(t\) ώς\[
(\lambda_x \boxed{x}) ((\lambda_x \boxed{x})(\lambda_y (\lambda_x \boxed{x}) \boxed{y}))
\]ενώ στις δέ τον βλέπουμε ώς\[
(\boxed{\lambda_x x}) ((\boxed{\lambda_x x})(\boxed{\lambda_y (\lambda_x x) y})).
\]Απ' όλα τα κουτάκια που μας δίνει το παρσάρισμα σε κάθε περίπτωση, σημειώσαμε εδώ μόνο αυτά που είπαμε «μαύρα κουτιά», δηλαδή μόνο τα μέσα-μέσα, και όχι κάθε υπερκουτάκι τους.
Να τελειώσουμε όμως κρατώντας άλλο ένα ερώτημα: με φιξαρισμένο παρσάρισμα, παίρνουμε με κάθε στρατηγική τον ίδιον όρο ως τελική τιμή· σύμπτωση, ή ισχύει πάντα αυτό; (κρατούμενο δύο)
Ας περιοριστούμε στον άτυπο λογισμό λάμδα, οπου η αναγωγή βασίζεται απλά στον κανόνα της βήτα μετατροπής\[
(\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*}
\]Πώς να υλοποιήσουμε όμως μια τέτοια αποτίμηση με έναν ομοιόμορφο τρόπο;
Ντετερμινιστικές στρατηγικές
Η παραπάνω σχολική στρατηγική - μή στρατηγική, αναφέρεται στη βιβλιογραφία ως πλήρης αναγωγή, και μπορούμε προφανώς να την κατανοήσουμε μόνο ως μή ντετερμινιστική στρατηγική. Άμα θέλουμε κάτι ντετερμινιστικό, δύο είναι οι φυσιολογικές προσεγγίσεις που έχουνε εδραιωθεί για τα καλά στην πιάτσα. Καί οι δύο πατάν στην κοινή σύμβαση οτι η αναγωγή προχωράει, καταρχήν, απο αριστερά προς τα δεξιά.
Περαιτέρω, η αναγωγή κατα κανονική σειρά (normal order) προχωράει απο έξω προς τα μέσα:\[
\begin{align*}
t &= \underline{(\lambda_x x) ((\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*}
\](οπου σε κάθε βήμα της αναγωγής παίρνεται υπόψη η προηγούμενη υπογράμμιση) και αντίθετα, η αναγωγή κατα σειρά εφαρμογής (applicative order) απο μέσα προς τα έξω:\[
\begin{align*}
t &= (\lambda_x x) ((\lambda_x x)(\lambda_y \underline{(\lambda_x x) y}))\\
&\leadsto (\lambda_x x) (\underline{(\lambda_x x)(\lambda_y y)})\\
&\leadsto \underline{(\lambda_x x) (\lambda_y y)}\\
&\leadsto \lambda_y y .
\end{align*}
\]Αυτές είναι οι δύο εύλογες και απλούστερες επιλογές ανάμεσα στις πολλαπλές επιλογές της σχολικής πλήρους αναγωγής.
Τώρα, δύο βαριάντες των επάνω παίρνουμε άν θεωρήσουμε οτι κάθε λαμδαφαίρεση είναι ήδη σε κανονική μορφή, είναι ήδη τιμή, και λειτουργεί άρα ως μαύρο κουτί, εμποδίζοντας την αναγωγή να προχωρήσει στα ενδότερα. Εδώ να κρατήσουμε ήδη ένα ερώτημα: Γιατί να το κάνουμε αυτό; γιατί η λαμδαφαίρεση να θεωρείται ανάγωγη; γιατί να θεωρείται «τιμή»;... (κρατούμενο ένα)
Η αναγωγή κατ' όνομα (call by name) προχωράει απο έξω προς τα μέσα κατα προσέγγιση λαμδαφαίρεσης:\[
\begin{align*}
t &= \underline{(\lambda_x x) ((\lambda_x x)(\boxed{\lambda_y (\lambda_x x) y}))}\\
&\leadsto \underline{(\lambda_x x)(\boxed{\lambda_y (\lambda_x x) y})}\\
&\leadsto \boxed{\lambda_y (\lambda_x x) y}
\end{align*}
\]και η αναγωγή κατα τιμή (call by value) προχωράει απο μέσα προς τα έξω κατα προσέγγιση λαμδαφαίρεσης:\[
\begin{align*}
t &= (\lambda_x x) (\underline{(\lambda_x x)(\boxed{\lambda_y (\lambda_x x) y})})\\
&\leadsto \underline{(\lambda_x x)(\boxed{\lambda_y (\lambda_x x) y})}\\
&\leadsto \boxed{\lambda_y (\lambda_x x) y} .
\end{align*}
\]
Παρσάρισμα
Στα παραπάνω, κάθε έκφραση τύπου «απο ... προς τα ...» προϋποθέτει ήδη οτι έχουμε παρσάρει τον όρο με κάποιον συμφωνημένο τρόπο. Αυτό το υπονοήσαμε ήδη μιλώντας για «μαύρα κουτιά»: πρώτα παρσάρουμε τον όρο και μετά ξεκινάμε να αποτιμούμε, και φυσικά, η διαδικασία της αποτίμησης, η αναγωγή δηλαδή, θα νοείται έτσι ωστε ν' απαγορεύεται να εισχωρεί στα μαύρα κουτιά, όποια κι αν είν' αυτά καθε φορά. Έτσι, στις περιπτώσεις των αναγωγών κατα κανονική σειρά και κατα σειρά εφαρμογής, το παρσάρισμα εισχωρεί στις λαμδαφαιρέσεις, ενώ στις περιπτώσεις των αναγωγών κατ' όνομα και κατα τιμή, όχι.
Παραστατικότερα, πλαισιώνοντας τους υποόρους που κατα περίπτωση θεωρούνται μαύρα κουτιά, βλέπουμε στις μέν περιπτώσεις τον όρο \(t\) ώς\[
(\lambda_x \boxed{x}) ((\lambda_x \boxed{x})(\lambda_y (\lambda_x \boxed{x}) \boxed{y}))
\]ενώ στις δέ τον βλέπουμε ώς\[
(\boxed{\lambda_x x}) ((\boxed{\lambda_x x})(\boxed{\lambda_y (\lambda_x x) y})).
\]Απ' όλα τα κουτάκια που μας δίνει το παρσάρισμα σε κάθε περίπτωση, σημειώσαμε εδώ μόνο αυτά που είπαμε «μαύρα κουτιά», δηλαδή μόνο τα μέσα-μέσα, και όχι κάθε υπερκουτάκι τους.
Να τελειώσουμε όμως κρατώντας άλλο ένα ερώτημα: με φιξαρισμένο παρσάρισμα, παίρνουμε με κάθε στρατηγική τον ίδιον όρο ως τελική τιμή· σύμπτωση, ή ισχύει πάντα αυτό; (κρατούμενο δύο)
