Δηλωτική σημασιολογία

Στην επιστήμη των υπολογιστών, η δηλωτική σημασιολογία (denotational semantics) είναι μια προσέγγιση για την τυποποίηση της σημασίας των γλωσσών προγραμματισμού μέσω της κατασκευής μαθηματικών αντικειμένων (που ονομάζονται δηλώσεις, denotations), τα οποία περιγράφουν τις σημασίες των εκφράσεων των γλωσσών. Άλλες προσεγγίσεις της τυπικής σημασιολογίας των γλωσσών προγραμματισμού είναι η αξιωματική σημασιολογία (axiomatic semantics) και η λειτουργική σημασιολογία (operational semantics).

Η δηλωτική σημασιολογία, γενικά, ασχολείται με την εύρεση μαθηματικών αντικειμένων που ονομάζονται πεδία (domains), που αναπαριστούν αυτό που κάνει ένα πρόγραμμα. Για παράδειγμα, κάποια προγράμματα (ή φράσεις από προγράμματα) μπορούν να αναπαρασταθούν από μερικές συναρτήσεις, από σενάρια διαγραμμάτων συμβάντων από Actors ή από παίγνια (games) μεταξύ του περιβάλλοντος και του συστήματος: όλα αυτά είναι γενικά παραδείγματα πεδίων.

Μια σημαντική αρχή της δηλωτικής σημασιολογίας είναι ότι η σημασιολογία πρέπει να είναι συνθετική: η σημασιολογία μιας φράσης του προγράμματος πρέπει να κατασκευάζεται από τις δηλώσεις των υποφράσεών της.

Ανάπτυξη της δηλωτικής σημασιολογίας

Η δηλωτική σημασιολογία προήλθε από το έργο του Christopher Strachey και του Dana Scott κατά τη δεκαετία του 1960. Όπως αρχικά αναπτύχθηκε από αυτούς, η δηλωτική σημασιολογία έδινε τη δήλωση (σημασία) ενός προγράμματος υπολογιστή ως μια συνάρτηση που αντιστοιχίζει είσοδο σε έξοδο.^[1] Για να δοθούν οι δηλώσεις των αναδρομικά ορισμένων προγραμμάτων, ο Scott πρότεινε την εργασία με συνεχείς συναρτήσεις μεταξύ πεδίων, και ειδικότερα πλήρεις σχέσεις μερικής διάταξης (complete partial orders). Όπως θα περιγραφεί στη συνέχεια, το έργο αυτό συνεχίστηκε προς την έρευνα πάνω στην κατάλληλη δηλωτική σημασιολογία που αφορά πλευρές των γλωσσών προγραμματισμού, όπως η αλληλουχίες εντολών (sequentiality), ο ταυτοχρονισμός, ο μη-ντετερμινισμός και η τοπική κατάσταση (local state).

Έχουν αναπτυχθεί δηλωτικές σημασιολογίες για σύγχρονες γλώσσες προγραμματισμού που χρησιμοποιούν capabilities όπως ο ταυτοχρονισμός και οι εξαιρέσεις, π.χ. η ActorScript,^[2] η Concurrent ML,^[3] οι CSP,^[4] και η Haskell.^[5] Οι σημασιολογίες αυτών των γλωσσών υπακούουν στον κανόνα της σύνθεσης γιατί η δήλωση μιας φράσης εξαρτάται από τις δηλώσεις των υποφράσεών της. Για παράδειγμα, η σημασία της έκφρασης f(E1,E2) ορίζεται με βάση τη σημασιολογία των υποφράσεών της f, E1 και E2. Σε μια σύγχρονη γλώσσα προγραμματισμού, οι E1 και E2 μπορούν να αποτιμώνται ταυτόχρονα και η εκτέλεσης της μιας από αυτές μπορεί να επηρεάζει την άλλη μέσω κοινών αντικειμένων, με αποτέλεσμα οι σημασιολογία τους να πρέπει να ορίζεται αμοιβαία. Επίσης η E1 ή η E2 μπορεί να προκαλέσουν μια εξαίρεση, η οποία προκαλεί τον τερματισμό της άλλης. Οι παρακάτω ενότητες περιγράφουν ειδικές περιπτώσεις της σημασιολογίας αυτών των σύγχρονων γλωσσών προγραμματισμού.

Σημασιολογία αναδρομικών προγραμμάτων

Η δηλωτική σημασιολογία αντιστοιχίζει σε κάθε φράση προγράμματος μια συνάρτηση από ένα περιβάλλον (που περιέχει τις τιμές των ελεύθερων μεταβλητών της) στη δήλωσή της. Για παράδειγμα, η φράση n*m παράγει μια δήλωση όταν της δοθεί ένα περιβάλλον που έχει δεσμεύσεις για τις δύο μεταβλητές της: τη n και τη m. Αν στο περιβάλλον η n έχει την τιμή 3 και η m έχει την τιμή 5, τότε η δήλωση είναι 15.

Μια συνάρτηση μπορεί να μοντελοποιηθεί ως ένα σύνολο από διατεταγμένα ζεύγη, με κάθε ζεύγος να αποτελείται από δύο μέρη: (1) ένα όρισμα για τη συνάρτηση και (2) την τιμή της συνάρτησης για αυτό το όρισμα. Για παράδειγμα, το σύνολο των διατεταγμένων ζευγών {[0 1] [4 3]} είναι η δήλωση μιας συνάρτησης με τιμή 1 για όρισμα 0, τιμή 3 για όρισμα 4, και μη ορισμένη σε κάθε άλλη περίπτωση.

Το πρόβλημα που πρέπει να λυθεί είναι η απόδοση δηλώσεων σε αναδρομικά προγράμματα που ορίζονται με βάση τον εαυτό τους, όπως ο ορισμός της συνάρτησης παραγοντικό (factorial):

factorial ≡ λ(n) if (n==0) then 1 else n*factorial(n-1).

Μια λύση είναι η κατασκευή της δήλωσης προσεγγιστικά, αρχίζοντας με το κενό σύνολο διατεταγμένων ζευγών (το οποίο στη θεωρία συνόλων θα μπορούσε να γραφεί ως {}). Αν το {} τοποθετηθεί στον παραπάνω ορισμό του παραγοντικού τότε η δήλωση είναι {[0 1]}, που είναι μια καλύτερη προσέγγιση του παραγοντικού. Επαναληπτικά: αν το {[0 1]} τοποθετηθεί στον ορισμό τότε η δήλωση είναι {[0 1] [1 1]}. Επομένως είναι βολικό μια προσέγγιση της factorial να θεωρείται ως μία είσοδος F ως εξής:

λ(F) λ(n) if (n==0) then 1 else n*F(n-1).

Είναι χρήσιμο να θεωρηθεί μια αλυσίδα από "επαναλήψεις" όπου η Fⁱ αντιστοιχεί σε i-φορές εφαρμογή της F.

• η F⁰({}) είναι η πλήρως μη ορισμένη μερική συνάρτηση {},
• η F¹({}) είναι η συνάρτηση {[0 1]} που είναι ορισμένη στο 0, με τιμή 1, και μη ορισμένη οπουδήποτε αλλού,
• η F⁵({}) είναι η συνάρτηση {[0 1] [1 1] [2 2] [3 6] [4 24]}

Το ελάχιστο άνω όριο (least upper bound) αυτής της αλυσίδας είναι η πλήρης συνάρτηση factorial, η οποία μπορεί να εκφραστεί ως εξής, με το σύμβολο "⊔" να σημαίνει "ελάχιστο άνω όριο":

⊔_i∈NFⁱ({})

Δηλωτική σημασιολογία μη ντετερμινιστικών προγραμμάτων

Η έννοια των power domains αναπτύχθηκε για δοθεί μια δηλωτική σημασιολογία των μη ντετερμινιστικών ακολουθιακών προγραμμάτων. Αν P είναι ένας κατασκευαστης power domain, το P(D) είναι το πεδίο των μη ντετερμινιστικών υπολογισμών με τύπο που δηλώνεται από το D.

Υπάρχουν κάποιες δυσκολίες όσον αφορά τη δικαιοσύνη (fairness) και τις μη φραγμένες συμπεριφορές σε πεδιο-θεωρητικά μοντέλα του μη ντετερμινισμού.^[6] Δείτε επίσης Power domains.

Δηλωτική σημασιολογία του ταυτοχρονισμού

Αρκετοί ερευνητές θεωρούν ότι τα πεδιο-θεωρητικά μοντέλα που δόθηκαν παραπάνω δεν αρκούν για τη γενική περίπτωση του ταυτόχρονου υπολογισμού. Για αυτόν το λόγο έχουν προταθεί διάφορα νέα μοντέλα. Στις αρχές του 1980, το στυλ της δηλωτικής σημασιολογίας άρχισε να χρησιμοποιείται για την απόδοση σημασιολογίας σε γλώσσες ταυτοχρονισμού. Παραδείγματα είναι η δουλειά του Will Clinger στο μοντέλο Actor, η δουλειά του Glynn Winskel σε δομές συμβάντων (event structures) και δίκτυα petri^[7], και η δουλειά των Francez, Hoare, Lehmann, και de Roever (1979) στα trace semantics για CSP.^[8] Αυτές οι κατευθύνσεις της έρευνας συνεχίζουν να προχωρούν.

Πρόσφατα, ο Winskel και άλλοι πρότειναν την κατηγορία των profunctors ως θεωρία πεδίων για τον ταυτοχρονισμό.^[9][10]

Δηλωτική σημασιολογία της κατάστασης

Η κατάσταση (όπως ο σωρός) και απλά χαρακτηριστικά των προστακτικών γλωσσών προγραμματισμού μπορούν να μοντελοποιηθούν με ευθύ τρόπο στη δηλωτική σημασιολογία που προαναφέρθηκε. Τα βιβλία περιέχουν περισσότερες πληροφορίες. Η βασική ιδέα είναι η θεώρηση μιας εντολής σαν μιας μερικής συνάρτησης σε κάποιο πεδίο από καταστάσεις. Τότε η δήλωση του "x:=3" είναι η συνάρτηση που από μια κατάσταση σε μια κατάσταση με την τιμή 3 να έχει ανατεθεί στην x. Ο τελεστής ακολουθιών εντολών ";" δηλώνεται με σύνθεση συναρτήσεων. Οι κατασκευές σταθερού σημείου χρησιμοποιούνται στη συνέχεια για να δώσουν σημασιολογία στους βρόχους, όπως στην εντολή "while".

Η μοντελοποίηση προγραμμάτων με τοπικές μεταβλητές είναι δυσκολότερη. Μια προσέγγιση είναι να μη χρησιμοποιούνται πια πεδία, αλλά να ερμηνεύονται οι τύποι ως functors από κάποια κατηγορία από κόσμους σε μια κατηγορία από πεδία. Οι δηλώσεις τότε των προγραμμάτων προκύπτουν από φυσικός μετασχηματισμός φυσικές συνεχείς συναρτήσεις ανάμεσα σε αυτούς τους functors.^[11][12]

Δηλώσεις τύπων δεδομένων

Πολλές γλώσσες προγραμματισμού επιτρέπουν στο χρήστη να ορίζει αναδρομικούς τύπους δεδομένων. Για παράδειγμα, ο τύπος των λιστών αριθμών μπορεί να οριστεί ως:

datatype list = Cons of (Nat, list) | Empty.

Αυτή η ενότητα ασχολείται μόνο με συναρτησιακές δομές δεδομένων που δεν αλλάζουν. Οι συμβατικές προστακτικές γλώσσες προγραμματισμού θα επέτρεπαν στα στοιχεία μιας τέτοιας αναδρομικής λίστας να αλλάζουν.

Ένα άλλο παράδειγμα: ο τύπος των δηλώσεων του λ-λογισμού χωρίς τύπους είναι:

datatype D = (D → D)

Το πρόβλημα της επίλυσης εξισώσεων πεδίων ασχολείται με την εύρεση πεδίων που μοντελοποιούν τέτοιους τύπους δεδομένων. Γενικά μιλώντας, μια προσέγγιση είναι να θεωρείται το σύνολο όλων των πεδίο ως πεδίο, και στη συνέχεια να επιλύεται εκεί ο αναδρομικός ορισμός. Τα βιβλία περιέχουν περισσότερες πληροφορίες.

Οι πολυμορφικοί τύποι δεδομένων είναι τύποι δεδομένων που ορίζονται με μια παράμετρο. Για παράδειγμα, ο τύπος των λιστών από α (α lists) ορίζεται ως εξής:

datatype α list = Cons of (α, list) | Empty.

Οι λίστες από αριθμούς είναι τότε τύπου Nat list, ενώ οι λίστες από συμβολοσειρές είναι String list.

Έχουν αναπτυχθεί κάποια πεδιο-θεωρητικά μοντέλα του πολυμορφισμού από κάποιους ερευνητές, ενώ κάποιοι άλλοι έχουν μοντελοποιήσει τον παραμετρικό πολυμορφισμό σε κατασκευαστικές θεωρίες συνόλων. Περισσότερες λεπτομέρειες μπορούν να βρεθούν στα βιβλία.

Πρόσφατα υπάρχει ένα πεδίο έρευνας για δηλωτική σημασιολογία για γλώσσες προγραμματισμού που βασίζονται σε κλάσεις ή αντικείμενα.^[13]

Δηλωτική σημασιολογία προγραμμάτων περιορισμένης πολυπλοκότητας

Λόγω της ανάπτυξης γλωσσών προγραμματισμού βασισμένων στη γραμμική λογική, έχει αποδοθεί δηλωτική σημασιολογία σε γλώσσες που περιλαμβάνουν γραμμική χρήση (π..χ proof nets, coherence spaces) και πολυπλοκότητα πολυωνυμικού χρόνου.^[14]

Δηλωτική σημασιολογία για ακολουθιακά προγράμματα

Το πρόβλημα της αφαίρεσης για την ακολουθιακή γλώσσα προγραμματισμού PCF αποτέλεσε για μεγάλο χρονικό διάστημα, ένα μεγάλο ανοιχτό ερώτημα της δηλωτικής σημασιολογίας. Το πρόβλημα της PCF είναι ότι είναι πολύ ακολουθιακή ως γλώσσα. Για παράδειγμα, δεν υπάρχει τρόπος να οριστεί η συνάρτηση παράλληλη-διάζευξη (parallel-or) στην PCF. Για αυτόν το λόγο, η παραπάνω τεχνική με τη χρήση πεδίων, έχει ως αποτέλεσμα δηλωτική σημασιολογία που δεν είναι πλήρως αφηρημένη.

Αυτό το ανοιχτό ερώτημα απαντήθηκε σε μεγάλο βαθμό κατά τη δεκαετία του 1990 με την ανάπτυξη των game semantics και με τεχνικές που περιλάμβαναν λογικές σχέσεις.^[15] Για περισσότερες λεπτομέρειες, βλ. PCF.

Η δηλωτική σημασιολογία ως μετάφραση από κώδικα σε κώδικα

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

Σε αυτά τα πλαίσια, οι ιδέες της δηλωτικής σημασιολογίας, όπως η πλήρης αφαίρεση, βοηθούν στην ικανοποίηση απαιτήσεων ασφαλείας.^[16][17]

Αφαίρεση

Συχνά θεωρείται σημαντικό να συνδέεται η δηλωτική σημασιολογία με τη λειτουργική σημασιολογία. Αυτό είναι ιδιαίτερα σημαντικό όταν η δηλωτική σημασιολογία είναι πολύ μαθηματική και αφηρημένη, και η λειτουργική σημασιολογία είναι πιο στέρεη ή πιο κοντά σε υπολογιστικές έννοιες. Οι παρακάτω ιδιότητες της δηλωτικής σημασιολογίες πολλές φορές θεωρούνται ενδιαφέρουσες.

1. Ανεξαρτησία από τη σύνταξη: Οι δηλώσεις των προγραμμάτων δε θα έπρεπε να περιλαμβάνουν τη σύνταξη της αρχικής γλώσσας.
2. Ορθότητα (Soundness): Όλα τα προγράμματα που μπορούν να παρατηρηθούν ως διαφορετικά έχουν διαφορετικές δηλώσεις.
3. Πλήρης αφαίρεση: Δύο προγράμματα έχουν την ίδια δήλωση ακριβώς όταν μπορεί να παρατηρηθεί ότι είναι ισοδύναμα. Όσον αφορά τη σημασιολογία στο κλασικό στυλ, η πλήρης αφαίρεση μπορεί να θεωρηθεί περίπου ως η απαίτηση ότι "η λειτουργική ισοδυναμία ταυτίζεται με τη δηλωτική ισότητα". Στη δηλωτική σημασιολογία σε πιο intensional μοντέλα, όπως το μοντέλο Actor και το process calculi, υπάρχουν πολλοί τρόποι ισοδυναμίας σε κάθε μοντέλο, και η έννοια της πλήρους αφαίρεσης αποτελεί θέμα συζήτησης και δυσκολότερη να οριστεί μονοσήμαντα. Η μαθηματική δομή της λειτουργικής σημασιολογίας και της δηλωτικής σημασιολογίας μπορούν επίσης να πλησιάσουν η μια την άλλη.

Επιπλέον επιθυμητές ιδιότητες ανάμεσα στη λειτουργική και τη δηλωτική σημασιολογία είναι:

1. Κατασκευή (Constructivism): ασχολείται με το αν στοιχεία ενός πεδίου μπορούν να αποδειχθούν ότι υπάρχουν με κατασκευαστικές μεθόδους.
2. Ανεξαρτησία της δηλωτικής και της λειτουργικής σημασιολογίας: Η δηλωτική σημασιολογία πρέπει να τυποποιείται με τη χρήση μαθηματικών δομών που είναι ανεξάρτητες από τη λειτουργική σημασιολογία μιας γλώσσας προγραμματισμού. Όμως, οι αρχές στις οποίες βασίζονται είναι στενά συνδεδεμένες. Βλ. την ενότητα Αρχή της σύνθεσης παρακάτω.
3. Πληρότητα (Full completeness) ή ικανότητα ορισμού (definability): Κάθε μορφισμός του σημασιολογικού μοντέλου θα πρέπει να είναι η δήλωση ενός προγράμματος.^[18]

Αρχή της σύνθεσης

Ένα σημαντικό χαρακτηριστικό της δηλωτικής σημασιολογίας είναι η Αρχή της σύνθεσης (compositionality), σύμφωνα με την οποία η δήλωση ενός προγράμματος κατασκευάζεται από τις δηλώσεις των τμημάτων του. Για παράδειγμα, έστω η έκφραση "7 + 4". Η αρχή της σύνθεσης σε αυτήν την περίπτωση είναι το να δοθεί σημασία στην "7 + 4" με όρους "7", "4" και "+".

Η βασική δηλωτική σημασιολογία της θεωρίας πεδίων είναι συνθετική γιατί δίνεται όπως περιγράφεται στη συνέχεια. Αρχίζουμε θεωρώντας αποσπάσματα προγράμματος, δηλαδή προγράμματα με ελεύθερες μεταβλητές. Ένα περιβάλλον τυποποίησης (typing context) δίνει κάποιον τύπο σε κάθε ελεύθερη μεταβλητή. Για παράδειγμα, η έκφραση (x + y) θα μπορούσε να θεωρηθεί σε ένα περιβάλλον τυποποίησης (x:nat,y:nat). Στη συνέχεια δίνουμε δηλωτική σημασιολογία στα αποσπάσματα του προγράμματος, ακολουθώντας το εξής σχέδιο.

1. Αρχίζουμε περιγράφοντας τη σημασία των τύπων της γλώσσας μας: η σημασία κάθε τύπου πρέπει να είναι ένα πεδίο. Γράφουμε〚τ〛για το πεδίο που δηλώνει τον τύπο τ. Για παράδειγμα, η σημασία του τύπου nat θα έπρεπε να είναι το πεδίο των φυσικών αριθμών: 〚nat〛=ℕ_⊥.
2. Από τη σημασία των τύπων παράγουμε σημασία για περιβάλλοντα τυποποίησης. Ορίζουμε〚 x₁:τ₁,..., x_n:τ_n〛 = 〚 τ₁〛× ... ×〚τ_n〛. Για παράδειγμα,〚x:nat,y:nat〛= ℕ_⊥×ℕ_⊥. Ως ειδική περίπτωση, η σημασία του κενού περιβάλλοντος τυποποίησης, χωρίς μεταβλητές, είναι το πεδίο με ένα μόνο στοιχείο, που δηλώνεται ως 1.
3. Τελικά, πρέπει να δώσουμε σημασία σε κάθε απόσπασμα-προγράμματος-σε-περιβάλλον-τυποποίησης. Υποθέστε ότι το P είναι ένα μέρος του προγράμματος με τύπο σ, στο περιβάλλον τυποποίησης Γ, και συχνά γράφουμε Γ⊢P:σ. Τότε η σημασία αυτού του προγράμματος-σε-περιβάλλον-τυποποίησης πρέπει να είναι μια συνεχής συνάρτηση〚Γ⊢P:σ〛:〚Γ〛→〚σ〛. Για παράδειγμα, το〚⊢7:nat〛:1→ℕ_⊥ είναι η συνάρτηση που είναι σταθερά "7", ενώ το 〚x:nat,y:nat⊢x+y:nat〛:ℕ_⊥×ℕ_⊥→ℕ_⊥ είναι η συνάρτηση που προσθέτει δύο αριθμούς.

Με αυτόν τον τρόπο, η σημασία της σύνθετης έκφρασης (7+4) ορίζεται από τη σύνθεση των τριών συναρτήσεων 〚⊢7:nat〛:1→ℕ_⊥, 〚⊢4:nat〛:1→ℕ_⊥, και 〚x:nat,y:nat⊢x+y:nat〛:ℕ_⊥×ℕ_⊥→ℕ_⊥.

Τα παραπάνω αποτελούν ένα γενικότερο σχήμα για τη συνθετική δηλωτική σημασιολογία. Δεν υπάρχει κάτι που να αφορά ιδιαίτερα τα πεδία και τις συνεχείς συναρτήσεις. Κάποιος θα μπορούσε να δουλέψει αντί αυτών, με μια διαφορετική κατηγορία. Για παράδειγμα, στα game semantics, η κατηγορία των παιγνίων έχει τα παίγνια ως αντικείμενα και τις στρατηγικές ως μορφισμούς: μπορούμε να ερμηνεύσουμε τους τύπους ως παίγνια και τα προγράμματα ως στρατηγικές. Σε μια απλή γλώσσα, χωρίς γενική αναδρομή, μπορούμε να χρησιμοποιήσουμε την κατηγορία των συνόλων. Σε μια γλώσσα με παρενέργειες, μπορούμε να εργαστούμε με την κατηγορία Kleisliγια μια μονάδα. Σε μια γλώσσα με κατάσταση, μπορούμε να εργαστούμε με μια κατηγορία functor. Ο Robin Milner έχει υποστηρίξει τη μοντελοποίηση της θέσης (location) και της αλληλεπίδρασης (interaction) με την εργασία σε μια κατηγορία με αντικείμενα interfaces και μορφισμούς bigraphs.^[19]

Σημασιολογία και υλοποίηση

Σύμφωνα με το Dana Scott [1980]:

Δε χρειάζεται η σημασιολογία να ορίζει την υλοποίηση, αλλά θα πρέπει να παρέχει κριτήρια που δείχνουν ότι μια υλοποίηση είναι σωστή.^[20]

Σύμφωνα με τον Clinger [1981]:

Συνήθως, όμως, η τυπική σημασιολογία μιας κλασικής ακολουθιακής γλώσσας προγραμματισμού μπορεί να διερμηνευτεί η ίδια ώστε να αποτελέσει μια (μη αποδοτική) υλοποίηση της γλώσσας. Όμως η τυπική σημασιολογία δε χρειάζεται πάντα να παρέχει μια τέτοια υλοποίηση, και η πίστη ότι η σημασιολογία πρέπει να δίνει μια υλοποίηση οδηγεί σε σύγχυση όσον αφορά την τυπική σημασιολογία των ταυτόχρονων γλωσσών. Αυτή η σύγχυση είναι δυστυχώς εμφανής όταν η εμφάνιση του μη ντετερμινισμού χωρίς φράγμα στη σημασιολογία μιας γλώσσας προγραμματισμού λέμε ότι υπονοεί ότι η γλώσσα προγραμματισμού δε μπορεί να υλοποιηθεί.^[21]

Συνδέσεις με άλλες περιοχές της επιστήμης υπολογιστών

Υπάρχει έργο στη δηλωτική σημασιολογία που ερμηνεύει τους τύπους ως πεδία όπως η θεωρία πεδίων (domain theory), η οποία μπορεί να θεωρηθεί παρακλάδι της θεωρίας μοντέλων (model theory), οδηγώντας στη θεωρία τύπων και στη θεωρία κατηγοριών. Μέσα στην επιστήμη των υπολογιστών, υπάρχουν σχέσεις με την αφηρημένη διερμηνεία, την τυπική επαλήθευση (formal verification) και τον έλεγχο μοντέλων.

Οι μονάδες (monads) εισήχθηκαν στη δηλωτική σημασιολογία για την οργάνωση της σημασιολογίας, και οι ιδέες αυτές έχουν προκαλέσει σημαντικό αντίκτυπο στο συναρτησιακό προγραμματισμό.

Παραπομπές

1. Dana Scott and Christopher Strachey. Toward a mathematical semantics for computer languages Oxford Programming Research Group Technical Monograph. PRG-6. 1971.
2. Carl Hewitt.ActorScript^TM: Industrial strength integration of local and nonlocal concurrency for Client-cloud Computing arXiv:0907.3330
3. John Reppy "Concurrent ML: Design, Application and Semantics" in Springer-Verlag Lecture Notes In Computer Science; Vol. 693. 1993
4. A. W. Roscoe. "The Theory and Practice of Concurrency" Prentice-Hall. Revised 2005.
5. Simon Peyton Jones, Alastair Reid, Fergus Henderson, Tony Hoare, and Simon Marlow. "A semantics for imprecise exceptions" Conference on Programming Language Design and Implementation. 1999.
6. Paul Blain Levy: Amb Breaks Well-Pointedness, Ground Amb Doesn't. Electr. Notes Theor. Comput. Sci. 173: 221-239 (2007)
7. Event Structure Semantics for CCS and Related Languages. DAIMI Research Report, University of Aarhus, 67 pp., April 1983.
8. Nissim Francez, C.A.R. Hoare, Daniel Lehmann, and Willem-Paul de Roever. Semantics of nondeterminism, concurrency, and communication Journal of Computer and System Sciences. December 1979.
9. Gian Luca Cattani, Glynn Winskel: Profunctors, open maps and bisimulation. Mathematical Structures in Computer Science 15(3): 553-614 (2005)
10. Mikkel Nygaard, Glynn Winskel: Domain theory for concurrency. Theor. Comput. Sci. 316(1): 153-190 (2004)
11. Peter W. O'Hearn, John Power, Robert D. Tennent, Makoto Takeyama: Syntactic control of interference revisited. Electr. Notes Theor. Comput. Sci. 1. 1995.
12. Frank J. Oles: A Category-Theoretic Approach to the Semantics of Programming. PhD thesis, Syracuse University. 1982.
13. Bernhard Reus, Thomas Streicher: Semantics and logic of object calculi. Theor. Comput. Sci. 316(1): 191-213 (2004)
14. P. Baillot. Stratified coherence spaces: a denotational semantics for Light Linear Logic (ps.gz) Theoretical Computer Science , 318 (1-2), pp. 29-55, 2004.
15. P. W. O'Hearn and J. G. Riecke, Kripke Logical Relations and PCF, Information and Computation, Volume 120, Issue 1, July 1995, pp. 107-116.
16. Martin Abadi. Protection in programming-language translations. Proc. of ICALP'98. LNCS 1443. 1998.
17. Andrew Kennedy. Securing the .NET programming model. Theoretical Computer Science, 364(3). 2006
18. Curien, Pierre-Louis (2007). «Definability and Full Abstraction». Electronic Notes in Theoretical Computer Science (Papers in honour of Gordon Plotkin: Elsevier) 172: 301–310. doi:10.1016/j.entcs.2007.02.011. 
19. The Space and Motion of Communicating Agents. Robin Milner. Cambridge University Press, 2009, ISBN 9780521738330, 2008 draft.
20. It is not necessary for the semantics to determine an implementation, but it should provide criteria for showing that an implementation is correct.
21. Usually, however, the formal semantics of a conventional sequential programming language may itself be interpreted to provide an (inefficient) implementation of the language. A formal semantics need not always provide such an implementation, though, and to believe that semantics must provide an implementation leads to confusion about the formal semantics of concurrent languages. Such confusion is painfully evident when the presence of unbounded nondeterminism in a programming language's semantics is said to imply that the programming language cannot be implemented.

Περαιτέρω διάβασμα

Βιβλία

• Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977.
• Carl Gunter, "Semantics of Programming Languages: Structures and Techniques". MIT Press, Cambridge, Massachusetts, 1992. (ISBN 978-0262071437)
• Glynn Winskel, Formal Semantics of Programming Languages. MIT Press, Cambridge, Massachusetts, 1993. (ISBN 978-0262731034)
• R. D. Tennent, Denotational semantics. Handbook of logic in computer science, vol. 3 pp 169—322. Oxford University Press, 1994. (ISBN 0-19-853762-X)
• S. Abramsky and A. Jung: Domain theory. In S. Abramsky, D. M. Gabbay, T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, vol. III. Oxford University Press, 1994. (ISBN 0-19-853762-X)
• David A. Schmidt, Denotational semantics: a methodology for language development, Allyn and Bacon, 1986, ISBN 0205104509 (εξαντλήθηκε - κυκλοφορεί δωρεάν ως ηλεκτρονική έκδοση στο http://www.cis.ksu.edu/~schmidt/text/densem.html)

Άλλες παραπομπές

• Irene Greif. Semantics of Communicating Parallel Processes MIT EECS Doctoral Dissertation. August 1975.
• Gordon Plotkin. A powerdomain construction SIAM Journal on Computing, September 1976.
• Edsger Dijkstra. A Discipline of Programming Prentice Hall. 1976.
• Krzysztof R. Apt, J. W. de Bakker. Exercises in Denotational Semantics MFCS 1976: 1-11
• J. W. de Bakker. Least Fixed Points Revisited, Theoretical Computer Science 2(2): 155-181 (1976)
• Carl Hewitt and Henry Baker Actors and Continuous Functionals Proceeding of IFIP Working Conference on Formal Description of Programming Concepts. August 1-5, 1977.
• Henry Baker. Actor Systems for Real-Time Computation MIT EECS Doctoral Dissertation. January 1978.
• Michael Smyth. Power domains, Journal of Computer and System Sciences. 1978.
• George Milne and Robin Milner. Concurrent processes and their syntax, JACM. April, 1979.
• Nissim Francez, C.A.R. Hoare, Daniel Lehmann, and Willem-Paul de Roever. Semantics of nondeterminism, concurrency, and communication, Journal of Computer and System Sciences. December 1979.
• Nancy Lynch and Michael J. Fischer. On describing the behavior of distributed systems in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Jerald Schwartz Denotational semantics of parallelism in Semantics of Concurrent Computation. Springer-Verlag. 1979.
• William Wadge. An extensional treatment of dataflow deadlock Semantics of Concurrent Computation. Springer-Verlag. 1979.
• Ralph-Johan Back. Semantics of Unbounded Nondeterminism, ICALP 1980.
• David Park. On the semantics of fair parallelism Proceedings of the Winter School on Formal Software Specification. Springer-Verlag. 1980.
• Lloyd Allison, A Practical Introduction to Denotational Semantics, Cambridge University Press. 1987.
• P. America, J. de Bakker, J. N. Kok and J. Rutten. Denotational semantics of a parallel object-oriented language, Information and Computation, 83(2): 152 - 205 (1989)
• David A. Schmidt, The Structure of Typed Programming Languages. MIT Press, Cambridge, Massachusetts, 1994. ISBN 0-262-69171-X.
• M. Korff True concurrency semantics for single pushout graph transformations with applications to actor systems, Working papers of the Int. Workshop on Information Systems - Correctness and Reusability. World Scientific. 1995.
• M. Korff and L. Ribeiro Concurrent derivations as single pushout graph grammar processes, Proceedings of the Joint COMPUGRAPH/SEMAGRAPH Workshop on Graph Rewriting and Computation. ENTCS Vol 2, Elsevier. 1995.
• Thati, Prasanna, Carolyn Talcott, and Gul Agha. Techniques for Executing and Reasoning About Specification Diagrams, International Conference on Algebraic Methodology and Software Technology (AMAST), 2004.
• J.C.M. Baeten, T. Basten, and M.A. Reniers. Algebra of Communicating Processes, Cambridge University Press. 2005.
• He Jifeng and C.A.R. Hoare. Linking Theories of Concurrency United Nations University International Institute for Software Technology UNU-IIST Report No. 328. July, 2005.
• Luca Aceto and Andrew D. Gordon (editors). Algebraic Process Calculi: The First Twenty Five Years and Beyond Process Algebra. Bertinoro, Forlì, Italy, August 1–5, 2005.
• A. W. Roscoe: The Theory and Practice of Concurrency, Prentice Hall, ISBN 0-13-674409-5. Revised 2005.

Εξωτερικοί σύνδεσμοι

• Denotational Semantics (Αγγλικά)
• Structure of Programming Languages I: Denotational Semantics. Σημειώσεις από μαθήματα του 1995 από τον Wolfgang Schreiner (Αγγλικά)