Added to Favorites

Related Searches

Definitions

Nearby Words

In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects (called denotations) which describe the meanings of expressions from the languages. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and operational semantics.

Denotational semantics originated in the work of Christopher Strachey and Dana Scott in the 1960s. As originally developed by Strachey and Scott, denotational semantics provided the denotation (meaning) of a computer program as a function that mapped input into output. To give denotations to recursively defined programs, Scott proposed working with continuous functions between domains, specifically complete partial orders. Work continues in the present day in investigating appropriate denotational semantics for aspects of programming languages such as sequentiality, concurrency, non-determinism and local state.

Broadly speaking, denotational semantics is concerned with finding mathematical objects that represent what programs do. Collections of such objects are called domains. For example, programs (or program phrases) might be represented by partial functions, or by Actor event diagram scenarios, or by games between the environment and the system: these are all general examples of domains.

An important tenet of denotational semantics is that semantics should be compositional: the denotation of a program phrase should be built out of the denotations of its subphrases. A simple example: the meaning of "3 + 4" is determined by the meanings of "3", "4", and "+".

Denotational semantics was first developed as a framework for functional and sequential programs modeled as mathematical functions mapping input to output. The first section of this article describes denotational semantics developed within this framework. Later sections deal with issues of polymorphism, concurrency, etc.

`function factorial(n:Nat):Nat ≡ if (n==0)then 1 else n*factorial(n-1)`.

In the semantics of recursion, a domain is typically a partial order, which can be understood as an order of definedness. For instance, the set of partial functions on the natural numbers can be given an order as follows:

- given partial functions f and g, let "f≤g" mean that "f agrees with g on all values for which f is defined".

It is usual to assume some properties of the domain, such as the existence of limits of chains (see cpo) and a bottom element. The partial order of partial functions has a bottom element, the totally undefined function. It also has least upper bounds of chains. Various additional properties are often reasonable and helpful: the article on domain theory has more details. One particularly important property is that of Scott continuity: one is interested in the continuous functions between domains (in the Scott topology). These are functions that preserve the order structure, and that preserve least upper bounds.

In this setting, types are denoted by domains, and the elements of the domains roughly capturing the elements of the types. A denotational semantics is given to a program phrase with free variables in terms of a continuous function from the denotation of its environment type to the denotation of its type. For example, the phrase `n*g(n-1)` has type `Nat`, and it has two free variables: `n`, of type `Nat`, and `g` of type `Nat -> Nat`. Thus its denotation will be a continuous function

- $mathbb\; N\; times\; (mathbb\; N\; rightharpoonup\; mathbb\; N)\; to\; mathbb\; N$.

Under this order on the partial functions, the denotation of the factorial program can be given as follows. First, we must develop denotations (as Scott-continuous functions) for the basic constructions such as `if-then-else`, `==`, and multiplication. One must also develop a denotational semantics for function abstraction and application. The program phrase

`λ n:N. if (n==0)then 1 else n*g(n-1)`

- $F:(mathbb\; Nrightharpoonupmathbb\; N)\; to\; (mathbb\; Nrightharpoonupmathbb\; N)$.

One way of proving the fixed point theorem gives an intuition as to why it is appropriate to give a semantics for recursion in this way. Every continuous function F:D→D on a domain D with bottom element ⊥ has a fixed point given by

- ⊔
_{i∈N}F^{i}(⊥).

It is instructive to think of the components of the chain as "iterates". In the case of the factorial program above, we had a function F on the domain of partial functions.

- F
^{0}(⊥) is the totally undefined partial function N→N; - F
^{1}(⊥) is the function that is defined at 0, to be 1, and undefined elsewhere; - F
^{5}(⊥) is the factorial function defined up to 4: F^{5}(⊥)(4) = 24. It is undefined for arguments greater than 4.

Thus the least upper bound of this chain, then, is the full factorial function (which happens to be a total function).

Things become more difficult in modelling programs with local variables. One approach is to no longer work with domains, but instead to interpret types as functors from some category of worlds to a category of domains. Programs are then denoted by natural continuous functions between these functors.

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

For another example: the type of denotations of the untyped lambda-calculus is

`datatype D = (D → D)`

Polymorphic data types are data types that are defined with a parameter. For example, the type of α `list`s is defined by

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

Some researchers have developed domain theoretic models of polymorphism. Other researchers have also modeled parametric polymorphism within constructive set theories. Details are found in the textbooks listed below.

A recent research area has involved denotational semantics for object and class based programming languages.

There are difficulties with fairness and unboundedness in domain-theoretic models of non-determinism. See Power domains for nondeterminism.

Recently, Winskel and others have proposed the category of profunctors as a domain theory for concurrency.

This open question was mostly resolved in the 1990s with the development of game semantics and also with techniques involving logical relations. For more details, see the page on PCF.

In this context, notions from denotational semantics, such as full abstraction, help to satisfy security concerns.

- Independence of denotational and operational semantics: The denotational semantics should be formalized using mathematical structures that are independent of the operational semantics of a programming language;
- Soundness: All observably distinct programs have distinct denotations;
- Full abstraction: Two programs have the same denotations precisely when they are observationally equivalent.

Additional desirable properties we may wish to hold between operational and denotational semantics are:

- Constructivity: The semantic model should be constructive in the sense that it should only include elements that can be intuitively constructed. One way of formalizing this is that every element must be the limit of a directed set of finite elements.
- Progressivity: For each system
`S`, there is a`progression`function for the semantics such that the denotation (meaning) of a system_{S}`S`is`⊔`where_{i∈ω}progression_{S}^{i}(⊥_{S})`⊥`is the initial configuration of_{S}`S`. - Full completeness or definability: Every morphism of the semantic model should be the denotation of a program.

For semantics in the traditional style, full abstraction may be understood roughly as the requirement that "operational equivalence coincides with denotational equality". For denotational semantics in more intensional models, such as the Actor model and process calculi, there are different notions of equivalence within each model, and so the concept of full abstraction is a matter of debate, and harder to pin down. Also the mathematical structure of operational semantics and denotational semantics can become very close.

- It is not necessary for the semantics to determine an implementation, but it should provide criteria for showing that an implementation is correct.

According to Clinger [1981]:

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

Monads were introduced to denotational semantics as a way of organising semantics, and these ideas have had a big impact in functional programming (see monads in functional programming).

- Joseph E. Stoy, Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics. MIT Press, Cambridge, Massachusetts, 1977. (A classic if dated textbook.)
- 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)
- Irene Greif. Semantics of Communicating Parallel Processes MIT EECS Doctoral Dissertation. August 1975.
- Gordon Plotkin. A powerdomain construction SIAM Journal of 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 Theor. Comput. Sci. 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 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, 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.
- 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.
- Carl Sassenrath (1999) denotational semantics and the REBOL programming language
- A. W. Roscoe: The Theory and Practice of Concurrency, Prentice Hall, ISBN 0-13-674409-5. Revised 2005.

- Denotational Semantics Overview of book by Lloyd Allison
- Structure of Programming Languages I: Denotational Semantics Course notes from 1995 by Wolfgang Schreiner
- Denotational Semantics: A Methodology for Language Development by David Schmidt

Wikipedia, the free encyclopedia © 2001-2006 Wikipedia contributors (Disclaimer)

This article is licensed under the GNU Free Documentation License.

Last updated on Friday October 10, 2008 at 05:25:05 PDT (GMT -0700)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

This article is licensed under the GNU Free Documentation License.

Last updated on Friday October 10, 2008 at 05:25:05 PDT (GMT -0700)

View this article at Wikipedia.org - Edit this article at Wikipedia.org - Donate to the Wikimedia Foundation

Copyright © 2014 Dictionary.com, LLC. All rights reserved.