Semantică denotațională

În informatică, semantica denotațională care poate fi tradusă și ca semantica înțelesurilor (cunoscută anterior ca semantică matematică sau semantică Scott-Strachey) este o abordare privind formalizarea înțelesurilor ce țin de limbajele de programare prin construirea de obiecte matematice (numite denotații) ce descriu înțelesurile expresiilor din alte limbaje. Alte abordări privind elaborarea de semantici formalizate pentru limbajele de programare includ semantici axiomatice și semantici operaționale.

În sens larg, semanticile denotaționale se preocupă de găsirea unor obiecte matematice numite domenii care să reprezinte ceea ce fac programele. De exemplu, programele (sau frazele din programe) pot fi reprezentate prin funcții parțiale sau de interacțiunea dintre mediu și sistem.

Un punct important pentru semanticile denotaționale este acela că semanticile ar trebui să fie compoziționale: denotația unei fraze a unui program ar trebui să fie construită din denotațiile frazelor componente.

Evoluție istorică

Semanticile denotaționale își au originile în opera lui Christopher Strachey și Dana Scott publicată la începutul anilor 70.^[1] Semanticile denotaționale așa cum au fost concepute la începuturi de Strachey și Scott, au oferit denotația (înțelesul) unui program de computer ca fiind o funcție care transpune inputul în output.^[2] Petru a da înțeles unor programe definite recursiv, Scott a propus lucrul cu funcții care să ofere continuitatea între domenii, îndeosebi pentru comenzi parțiale complete. Așa cum este descris mai jos, lucrul a continuat prin investigarea semanticilor denotaționale corespunzătoare pentru aspectele limbajelor de programare ce țin de secvențialitate, concurență, non-determinism și stare locală.

Semanticile denotaționale au fost dezvoltate pentru a fi utilizate de limbajele moderne care implică concurența și excepțiile, de exemplu, Concurrent ML,^[3] CSP,^[4] și Haskell.^[5] Semanticile acestor limbaje este compozițională prin faptul că denotația unei fraze depinde de denotațiile subfrazelor. De exemplu, înțelesul pentru expresiile aplicate f(E1,E2) este definit în termenii de semantici ale subfrazelor f, E1, și E2. Într-un limbaj de programare, E1 și E2 pot fi evaluate concurent, iar execuția uneia dintre ele poate afecta pe cealaltă prin interacțiunea prin intermediul unor obiecte partajate, fiind cauza unor denotații care să fie definite ca termeni raportați unii la ceilalți. De asemenea, E1 și E2 ar putea să ridice o excepție care ar putea cauza încheierea execuției unuia sau al celuilalt. Secțiunile de mai jos descriu cazurile speciale ale semanticilor acestor limbaje de programare moderne.

Note

^ Dana S. Scott. Outline of a mathematical theory of computation. Technical Monograph PRG-2, Oxford University Computing Laboratory, Oxford, England, November 1970.
^ Dana Scott and Christopher Strachey. Toward a mathematical semantics for computer languages Oxford Programming Research Group Technical Monograph. PRG-6. 1971.
^ John Reppy "Concurrent ML: Design, Application and Semantics" in Springer-Verlag, Lecture Notes in Computer Science, Vol. 693. 1993
^ A. W. Roscoe. "The Theory and Practice of Concurrency" Prentice-Hall. Revised 2005.
^ 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.

Lectură suplimentară

Manuale

R. E. Milne and C. Strachey, A theory of programming language semantics. Chapman and Hall, London; Wiley, New York, 1976.
M. J. C. Gordon. The Denotational Description of Programming Languages. Springer-Verlag, Berlin, 1979.
Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977. (A classic if dated textbook.)
David A. Schmidt, Denotational semantics: a methodology for language development, Allyn and Bacon, 1986, ISBN: 0-205-10450-9 (out or print now; free electronic version available)
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
V. Stoltenberg-Hansen, I. Lindström, E. R. Griffor, Mathematical Theory of Domains. Cambridge University Press, 1994.

Note de curs

Glynn Winskel. Denotational Semantics. University of Cambridge.

Alte opere

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)
Michael Smyth. "Power domains" Journal of Computer and System Sciences. 1978.
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.
Will Clinger, Foundations of Actor Semantics. MIT Mathematics Doctoral Dissertation, June 1981.
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.

[1] Dana S. Scott. Outline of a mathematical theory of computation. Technical Monograph PRG-2, Oxford University Computing Laboratory, Oxford, England, November 1970.

[2] Dana Scott and Christopher Strachey. Toward a mathematical semantics for computer languages Oxford Programming Research Group Technical Monograph. PRG-6. 1971.

[3] John Reppy "Concurrent ML: Design, Application and Semantics" in Springer-Verlag, Lecture Notes in Computer Science, Vol. 693. 1993

[Roscoe-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.

[1]

[2]

[3]

[4]

[5]