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

Από τη Βικιπαίδεια, την ελεύθερη εγκυκλοπαίδεια
Μετάβαση σε: πλοήγηση, αναζήτηση

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

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

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

Η πρώτη χρήση του όρου "λειτουργική σημασιολογία" αποδίδεται στο Dana Scott (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], με αποτέλεσμα να είναι μια από τις πιο συχνές παραπομπές σε τεχνική αναφορά στην επιστήμη υπολογιστών.

Δείτε επίσης[Επεξεργασία | επεξεργασία κώδικα]

Παραπομπές[Επεξεργασία | επεξεργασία κώδικα]

  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». http://www-formal.stanford.edu/jmc/recursive.html. Ανακτήθηκε στις 2006-10-13. 

Αναφορές[Επεξεργασία | επεξεργασία κώδικα]

  • 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. (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. διαθέσιμο ηλεκτρονικά.
Στο λήμμα αυτό έχει ενσωματωθεί κείμενο από το λήμμα Operational semantics της Αγγλόγλωσσης Βικιπαίδειας, η οποία διανέμεται υπό την GNU FDL και την CC-BY-SA 3.0. (ιστορικό/συντάκτες).