العربية
中国
Français
Deutsch
Ελληνική
हिन्दी
Italiano
日本語
Português
Русский
EspañolDENOTATIONAL SEMANTICS
In computer science, 'denotational semantics' is an approach to formalizing the semantics of computer systems by constructing mathematical objects (called ''denotations'' or ''meanings'') which express the semantics of these systems. Other approaches to providing a formal semantics of programming languages include axiomatic semantics and operational semantics. The denotational approach to semantics was originally developed to deal only with systems defined by a single computer program. Later the field broadened to include systems composed of more than one program, such as those found in networking and concurrent systems.
Denotational semantics originated in the work of Christopher Strachey and Dana Scott in the 1960s. As originally developed by Strachey and Scott, denotational semantics interpreted the denotation (meaning) of a computer program as a function that mapped input into output. Later, this proved to be too limiting to allow the definition of denotations (meanings) for programs that included elements such as recursively defined functions and data structures. Seeking to address these difficulties, Scott introduced a generalized approach to denotational semantics, based on domains . Later researchers introduced approaches based on power domains, in an effort to address difficulties with the semantics of concurrent systems .
Fixed point semantics
The denotational theory of computational system semantics is concerned with finding mathematical objects that represent what systems do. Collections of such objects are called domains. For example, systems might be represented by partial functions, or by Actor event diagram scenarios: these are two examples of domains.
A domain is typically a partial order, which can be understood as an order of definedness. For instance, given partial functions f and g, one might 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.
Various additional properties are often reasonable and helpful:
the article on domain theory has more details.
The mathematical denotation denoted by a system S is found by constructing increasingly better approximations from an initial empty denotation called ⊥S using some denotation approximating function 'progression'S to construct a denotation (meaning ) for S as follows:
::'Denote'S ≡ ⊔i∈ω 'progression'Si(⊥S).
It would be expected that 'progression'S would be ''monotone'', ''i.e.'', if x≤y then 'progression'S(x)≤'progression'S(y). More generally, we would expect that
::If ∀i∈ω xi≤xi+1, then 'progression'S(⊔i∈ω xi) = ∨i∈ω 'progression'S(xi)
This last stated property of 'progression'S is called ω-continuity.
A central question of denotational semantics is to characterize when it is possible to create denotations (meanings) according to the equation for 'Denote'S. A fundamental theorem of computational domain theory is that if 'progression'S is ω-continuous then 'Denote'S will exist.
It follows from the ω-continuity of 'progression'S that
:::'progression'S('Denote'S) = 'Denote'S
The above equation motivates the terminology that 'Denote'S is a ''fixed point'' of 'progression'S.
Furthermore this fixed point is least among all fixed points of 'progression'S.
The denotational semantics of functional programs provides an example of fixed point semantics as shown in the next section.
Example of factorial function
Consider the factorial function which is defined on all whole numbers as follows:
:factorial ≡ λ(n)if (n==0)then 1 else n
★ factorial(n-1)
The 'graph' of factorial is the set of all ordered pairs for which factorial is defined with the first element of an ordered pair being the argument and the second element being the value, ''e.g.'',
:'graph'(factorial) = {
The denotation (meaning) 'Denote'factorial for the factorial program is constructed as follows:
:'Denote'factorial = 'graph'(factorial) = ∪i∈ω 'progression'factoriali({})
where
:'progression'factorial(g) ≡ λ(n)if (n==0)then 1 else n
★ g(n-1)
Note: 'progression'factorial is a fix point operator (see definition in section above) whose least fixed point is 'Denote'factorial, i.e.,
:'Denote'factorial = 'progression'factorial('Denote'factorial)
Also 'progression'factorial is ω-continuous (see definition in section above).
Derivation of Scott Continuity from Computational Criteria
In order to be accepted as the foundation of denotational semantics, the criterion of continuity needs to be motivated on computational grounds. One way to do this is using the Actor model. If f is an Actor that behaves as a mathematical function then the graph of f can be derived as the least fixed point of 'progression'f as follows (see Carl Hewitt and Henry Baker [1977]):
:'graph'(f) = ∪i∈ω 'progression'fi({})
where
:'progression'f(G)≡{
::Roughly speaking 'immediate-descendants'f(
In the above manner, the criterion of continuity can be derived from the laws of Actors which are in turn based on physical laws.
Full abstraction
The concept of full abstraction is concerned with whether the denotational semantics for a program is an exact match for its operational semantics.
Key properties of full abstraction are:
#'Abstractness': The denotational semantics must be formalised using mathematical structures that are independent of the representation and operational semantics of the programming language;
#'Soundness': All observably distinct programs have distinct denotations;
#'Completeness': Any two programs with distinct denotations must be observably distinct.
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'S function for the semantics such that the denotation (meaning) of a system S is ∨i∈ω'progression'Si(⊥S) where ⊥S is the initial configuration of s.
#'Full completeness': Every morphism of the semantic model should be the denotation of a program.
A long-standing issue in denotational semantics was full abstraction in the presence of inductive datatypes, particularly the type of natural numbers, as a type admitting usage as a method of recursion. A traditional interpretation of this question was as semantics for the system PCF. The success achieved by game semantics in providing fully abstract models in the 1990s for PCF led to a fundamental change in the way that work on denotational semantics was done.
Compositionality in programming languages
Main articles: Principle of compositionality
An important aspect of denotational semantics of programming languages is compositionality, by which the denotation of a program is constructed from denotations of its parts. For example consider the expression "
For an example of compositionality in actor semantics,
see Compositionality in Actor Semantics.
Other programming constructs
The denotational compositional semantics presented above is very general and can be used for functional, imperative, concurrent, logic, ''etc.'' programs.
Challenges for denotational semantics
Delays and futures
Providing a denotational compositional semantics for delays and futures provides a challenge for denotational semantics.
Denotational semantics of concurrency
Extending denotational semantics to concurrency proved challenging (see unbounded nondeterminism).
Two principle approaches to denotational semantics of concurrency are those based on the process calculi and the Actor model (see denotational semantics of the Actor model).
Early history of denotational semantics
As mentioned earlier, the field was initially developed by Christopher Strachey and Dana Scott in the 1960s and then Joe Stoy in the 1970s at the Programming Research Group, part of the Oxford University Computing Laboratory.
Montague grammar is a form of denotational semantics for idealized fragments of English.
Connections to other areas of computer science
Some work in denotation semantics has interpreted types as domains in the sense of domain theory which can be seen as a branch of model theory, leading to connections with type theory and category theory. Within computer science, there are connections with abstract interpretation, program verification and functional programming, see for instance monads in functional programming. In particular, denotational semantics has used the concept of continuations to express control flow in sequential programming in terms of functional programming semantics.
References
★ 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 Professes'' MIT EECS Doctoral Dissertation. August 1975.
★ Joseph E. Stoy, ''Denotational Semantics: The Scott-Strachey Approach to Programming Language Semantics''. MIT Press, Cambridge, Massachusetts, 1977. (A classic if dated textbook.)
★ 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.
★ C.A.R. Hoare. ''Communicating Sequential Processes'' CACM. August, 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. ''A brief history of process algebra'' Theoretical Computer Science. 2005.
★ 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.
★ Bill Roscoe. ''The Theory and Practice of Concurrency'' Prentice-Hall. 2005.
★ Carl Sassenrath (1999) denotational semantics and the Rebol programming language
External links
★ ''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
Notes
1. The paper by Hewitt and Baker contained a small bug in the definition of 'immediate-descendants'f that was corrected in Will Clinger [1981].
This article provided by Wikipedia. To edit the contents of this article, click here for original source.
psst.. try this: add to faves
