Λειτουργική σημασιολογία

Στην επιστήμη υπολογιστών, η λειτουργική σημασιολογία (operational semantics) είναι ένας τρόπος να δίνεται νόημα σε προγράμματα υπολογιστών με μαθηματικά αυστηρό τρόπο. Η λειτουργική σημασιολογία περιλαμβάνει δύο κατηγορίες: η δομική λειτουργική σημασιολογία (structural operatational semantics) ή σημασιολογία μικρού βήματος (small-step semantics) περιγράφει τυπικά πώς συμβαίνουν τα ξεχωριστά βήματα ενός υπολογισμού σε ένα σύστημα, ενώ η φυσική σημασιολογία (natural semantics) ή σημασιολογία μεγάλου βήματος (big-step semantics) περιγράφει πώς προκύπτουν τα τελικά αποτελέσματα των υπολογισμών. Άλλες προσεγγίσεις της τυπικής σημασιολογίας των γλωσσών προγραμματισμού είναι η αξιωματική σημασιολογία και η δηλωτική σημασιολογία.

Η λειτουργική σημασιολογία μιας γλώσσας προγραμματισμού περιγράφει πώς ερμηνεύεται ένα έγκυρο πρόγραμμα σαν ακολουθία από υπολογιστικά βήματα. Οι ακολουθίες αυτές είναι η σημασία του προγράμματος. Στα συναρτησιακά προγράμματα, το τελικό βήμα μιας ακολουθίας που τερματίζει είναι αυτό που επιστρέφει την τιμή του προγράμματος. (Γενικά ένα πρόγραμμα μπορεί να επιστρέφει πολλές τιμές, αν είναι μη-ντετερμινιστικό, ή αν είναι ντετερμινιστικό και υπάρχουν πολλές ακολουθίες υπολογισμού με διαφορετικές τιμές που να είναι αποδεκτές από τη σημασιολογία.)

Η έννοια της λειτουργικής σημασιολογίας χρησιμοποιήθηκε για πρώτη φορά στον ορισμό της σημασιολογίας της Algol 68.^[1]

Η πρώτη χρήση του όρου "λειτουργική σημασιολογία" αποδίδεται στον Ντέινα Σκοτ (Plotkin04). Ακολουθεί ένα απόσπασμα από την ιστορική δημοσίευση του Scott πάνω στην τυπική σημασιολογία, στην οποία αναφέρει τη "λειτουργική" πλευρά της σημασιολογίας.

Γενικά είναι καλό να στοχεύουμε σε μια πιο 'αφηρημένη' και 'καθαρή' προσέγγιση στη σημασιολογία, αλλά για να πετύχει το σχέδιο, η λειτουργική σημασιολογία δε μπορεί να αγνοηθεί.^[2]

Μιά από τις πρώτες τυπικές χρήσεις της λειτουργικής σημασιολογίας ήταν η χρήση του λ-λογισμού για τον ορισμό της σημασιολογίας της LISP από τον Τζον Μακάρθι^[3]. Οι αφηρημένες μηχανές όπως η μηχανή SECD, έχουν επίσης στενή σχέση με τη λειτουργική σημασιολογία.

Προσεγγίσεις

Ο Gordon Plotkin εισήγαγε τη δομική λειτουργική σημασιολογία, ενώ ο Gilles Kahn τη φυσική σημασιολογία.

Δομική λειτουργική σημασιολογία

Η δομική λειτουργική σημασιολογία, δομημένη λειτουργική σημασιολογία (structured operational semantics, SOS) ή σημασιολογία μικρού βήματος εμφανίστηκε στο Plotkin81 από τον Gordon Plotkin σαν ένας λογικός τρόπος να ορίζεται η λειτουργική σημασιολογία. Η βασική ιδέα είναι να ορίζεται η συμπεριφορά ενός προγράμματος με βάση τη συμπεριφορά των επιμέρους τμημάτων του, παρέχοντας δηλαδή μια δομική (με βάση τη σύνταξη και την επαγωγή) θεώρηση της λειτουργικής σημασιολογίας. Η συμπεριφορά ενός προγράμματος περιγράφεται τότε με βάση ένα σύνολο από σχέσεις μετάβασης (transition relations). Οι ορισμοί με βάση αυτήν τη σημασιολογία έχουν τη μορφή κανόνων συνεπαγωγής (inference rules) που ορίζουν τις έγκυρες μεταβάσεις ενός σύνθετου συντακτικού μέρους με βάση τις μεταβάσεις των μερών που το αποτελούν.

Σαν ένα απλό παράδειγμα, θεωρούμε ένα μέρος της σημασιολογίας μιας απλής γλώσσας προγραμματισμού (περισσότερες λεπτομέρειες μπορούν να βρεθούν στο Plotkin81, το Hennessy90, και άλλα βιβλία). Έστω ότι οι $C_{1}$ και $C_{2}$ είναι κάποια προγράμματα της γλώσσας και η $s$ είναι κάποια κατάσταση (για παράδειγμα μια συνάρτηση από θέσεις στη μνήμη σε τιμές). Αν έχουμε εκφράσεις ( $E$ ), τιμές ( $V$ ) και θέσεις ( $L$ ), τότε μια εντολή ενημέρωσης της μνήμης θα είχε σημασιολογία:

${\frac {\langle E,s\rangle \Rightarrow V}{\langle L:=E\,,\,s\rangle \longrightarrow (s\uplus (L\mapsto V))}}$

Ο κανόνας λέει δηλαδή ότι "αν η έκφραση $E$ στην κατάσταση $s$ γίνεται τελικά η τιμή $V$ , τότε το πρόγραμμα $L:=E$ θα ενημερώσει την κατάσταση $s$ με την ανάθεση $L=V$ ".

Η σημασιολογία των ακολουθιών δίνεται από τους εξής τρεις κανόνες:

${\frac {\langle C_{1},s\rangle \longrightarrow s'}{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{2},s'\rangle }}\quad \quad {\frac {\langle C_{1},s\rangle \longrightarrow \langle C_{1}',s'\rangle }{\langle C_{1};C_{2}\,,s\rangle \longrightarrow \langle C_{1}';C_{2}\,,s'\rangle }}\quad \quad {\frac {}{\langle \mathbf {skip} ,s\rangle \longrightarrow s}}$

Ο πρώτος κανόνας λέει ότι, αν το πρόγραμμα $C_{1}$ στην κατάσταση $s$ τερματίζει στην κατάσταση $s'$ , τότε το πρόγραμμα $C_{1};C_{2}$ στην κατάσταση $s$ ανάγεται στο πρόγραμμα $C_{2}$ στην κατάσταση $s'$ . (Με απλούστερα λόγια: "Μπορούμε να εκτελέσουμε το $C_{1}$ και μετά να εκτελέσουμε το $C_{2}$ χρησιμοποιώντας την κατάσταση μνήμης που προέκυψε.) Ο δεύτερος κανόνας λέει ότι αν το πρόγραμμα $C_{1}$ στην κατάσταση $s$ μπορεί να αναχθεί στο πρόγραμμα $C_{1}'$ στην κατάσταση $s'$ , τότε το πρόγραμμα $C_{1};C_{2}$ στην κατάσταση $s$ ανάγεται στο πρόγραμμα $C_{1}';C_{2}$ στην κατάσταση $s'$ . (Η αρχή ενός μεταγλωττιστή που κάνει βελτιστοποιήσεις: "Μπορούμε να μετατρέψουμε το $C_{1}$ σαν να ήταν μόνο του, ακόμα και αν είναι απλά το πρώτο μέρος ενός προγράμματος.") Η σημασιολογία είναι δομική, επειδή η σημασία του ακολουθιακού προγράμματος $C_{1};C_{2}$ ορίζεται από τη σημασία του $C_{1}$ και τη σημασία του $C_{2}$ .

Αν έχουμε εκφράσεις αλήθειας πάνω στις καταστάσεις ( $B$ ), μπορούμε να ορίσουμε τη σημασιολογία της εντολής while: ${\frac {\langle B,s\rangle \Rightarrow \mathbf {true} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow \langle C;\mathbf {while} \ B\ \mathbf {do} \ C,s\rangle }}\quad {\frac {\langle B,s\rangle \Rightarrow \mathbf {false} }{\langle \mathbf {while} \ B\ \mathbf {do} \ C,s\rangle \longrightarrow s}}$

Ένας τέτοιος ορισμός επιτρέπει την τυπική ανάλυση της συμπεριφοράς των προγραμμάτων, επιτρέποντας τη μελέτη των σχέσεων μεταξύ προγραμμάτων, όπως οι σχέσεις προδιάταξης προσομοίωσης (simulation preorders) και η σχέση "bisimulation". Οι τελευταίες είναι ιδιαίτερα χρήσιμες στη θεωρία ταυτοχρονισμού.

Επειδή είναι ευανάγνωστη, τόσο όσον αφορά την εμφάνιση, όσο και όσον αφορά τη δομή, η δομική λειτουργική σημασιολογία έχει γίνει δημοφιλής και αποτελεί τον ντε φάκτο τρόπο ορισμού λειτουργικής σημασιολογίας. Σημείο αυτής της επιτυχία, η αρχική αναφορά ("Aarhus report") σχετικά με τη λειτουργική σημασιολογία (Plotkin81) έχει περισσότερες από 1000 παραπομπές να δείχνουν προς αυτήν σύμφωνα με τη σελίδα CiteSeer [1] Αρχειοθετήθηκε 2007-03-14 στο Wayback Machine., με αποτέλεσμα να είναι μια από τις πιο συχνές παραπομπές σε τεχνική αναφορά στην επιστήμη υπολογιστών.

Δείτε επίσης

Παραπομπές

↑ "The meaning of a program in the strict language is explained in terms of a hypothetical computer which performs the set of actions which constitute the elaboration of that program." (Algol68, Section 2)
↑ "It is all very well to aim for a more ‘abstract’ and a ‘cleaner’ approach to semantics, but if the plan is to be any good, the operational aspects cannot be completely ignored." (Scott70)
↑ John McCarthy. «Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I». Αρχειοθετήθηκε από το πρωτότυπο στις 4 Οκτωβρίου 2013. Ανακτήθηκε στις 13 Οκτωβρίου 2006.

Αναφορές

Gilles Kahn. "Natural Semantics". Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science. Springer-Verlag. London. 1987.
Gordon D. Plotkin. A Structural Approach to Operational Semantics Αρχειοθετήθηκε 2007-03-14 στο Wayback Machine.. (1981) Tech. Rep. DAIMI FN-19, Computer Science Department, Aarhus University, Aarhus, Denmark. (Reprinted with corrections in J. Log. Algebr. Program. 60-61: 17-139 (2004), preprint).
Gordon D. Plotkin. The Origins of Structural Operational Semantics. J. Log. Algebr. Program. 60-61:3-15, 2004. (preprint).
Dana S. Scott. Outline of a Mathematical Theory of Computation, Programming Research Group, Technical Monograph PRG–2, Oxford University, 1970.
Adriaan van Wijngaarden et al. Revised Report on the Algorithmic Language ALGOL 68. IFIP. 1968. ([2]^{[νεκρός σύνδεσμος]})
Matthew Hennessy. Semantics of Programming Languages. Wiley, 1990. διαθέσιμο ηλεκτρονικά.

[1] "The meaning of a program in the strict language is explained in terms of a hypothetical computer which performs the set of actions which constitute the elaboration of that program." (Algol68, Section 2)

[2] "It is all very well to aim for a more ‘abstract’ and a ‘cleaner’ approach to semantics, but if the plan is to be any good, the operational aspects cannot be completely ignored." (Scott70)

[3] John McCarthy. «Recursive Functions of Symbolic Expressions and Their Computation by Machine, Part I». Αρχειοθετήθηκε από το πρωτότυπο στις 4 Οκτωβρίου 2013. Ανακτήθηκε στις 13 Οκτωβρίου 2006.

[1]

[2]

[3]