Denotational semantics

From Wikipedia, the free encyclopedia

Wikibooks has a book on the topic of

Haskell/Denotational 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 (Abramsky and Jung 1994). Later researchers introduced approaches based on power domains, in an effort to address difficulties with the semantics of concurrent systems (Clinger 1981).

1 Fixed point semantics
- 1.1 Example of factorial function
- 1.2 Derivation of Scott Continuity from Actor Semantics
2 Full abstraction
3 Compositionality in programming languages
4 Denotational semantics of concurrency
5 Early history of denotational semantics
6 Connections to other areas of computer science
7 References
8 External links

[edit] Fixed point semantics

The denotational theory of computational system semantics is concerned with finding mathematical objects that represent what systems do. The theory makes use of computational mathematical domains. Examples of such computational domains are partial functions and Actor event diagram scenarios.

The relationship x≤y means that x can computationally evolve to y. If the denotations are partial functions, for example, f≤g may mean that f agrees with g on all values for which f is defined. If the denotations are Actor event diagram scenarios, x≤y means that a system which satisfies x can evolve into a system which satisfies y.

Computational domains have the following properties:

Bottom exists. The domain has a least element denoted by ⊥ such that for every element x in the domain ⊥≤x.
Limits exist. As computation continues, the denotations should become better and have a limit so if we have $\forall i \in \omega$ $x_i \le x_{i+1}$ then the least upper bound $\vee_{i \in \omega} x_i$ should exist. The property just stated is called $ω$ -completeness.
Finite elements are countable. An element x is finite (also called isolated in the domain literature) if and only if whenever A is directed, ∨A exists and $x \le \vee A$ , there exists $a \in A$ with $x \le a$ . In other words, x is finite if one must go through x in order to get up to or above x via the limit process.
Every element is the least upper bound of a countable increasing sequence of finite elements. Intuitively this means that every element can be reached by a computational process in which each progression is finite.
The domain is downward closed.

The mathematical denotation denoted by a system S is found by solving 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 [Hewitt 2006b]:

Denote_S ≡ ∨_i∈ω progression_Sⁱ(⊥_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∈ω x_{i_{≤x_i+1_{, then progression_S(∨_i∈ω x_i) = ∨_i∈ω progression_S(x_i)}}}

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

[edit] 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) = {<n, factorial(n)>|n∈ω} = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}

The denotation (meaning) Denote_factorial for the factorial program is constructed as follows:

Denote_factorial = graph(factorial) = ∪_i∈ω progression_factorialⁱ({})

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

[edit] Derivation of Scott Continuity from Actor Semantics

The Actor model provides a foundation for deriving Dana Scott's denotational semantics of functions (as illustrated in the previous section above for factorial) as demonstrated first by a theorem of Carl Hewitt and Henry Baker [1977]:

If an Actor f behaves like a mathematical function, then progression_f is a Scott continuous functional whose least fixed point is

graph(f) = ∪_i∈ω progression_fⁱ({})

where

progression_f(G)≡{<x, y>|<x, y>∈graph(f) and immediate-descendants_f(<x, y>)⊆G}

The paper by Hewitt and Baker contained a small bug in the definition of immediate-descendants_f that was corrected in Will Clinger [1981].

[edit] 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_Sⁱ(⊥_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.}

_{[edit] Compositionality in programming languages}

_{See main article 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 "<expression₁> + <expression₂>". Compositionality in this case is to provide a meaning for "<expression₁> + <expression₂>" in terms of the meanings of <expression₁> and <expression₂>.}

[edit] Environments

The Actor model provides a modern and very general way the compositionality of programs can be analyzed. In this analysis, programs are Actors that are sent Eval messages with the address of an environment Actor so that programs inherit their denotational semantics from the denotational semantics of the Actor model (an idea published in Hewitt [2006a]). The environment holds the bindings of identifiers. When an environment is sent a Lookup message with the address of an identifier x, it returns the latest (lexical) binding of x.

As an example of how this works consider the lambda expression <L> below which implements a tree data structure when supplied with parameters for a leftSubTree and rightSubTree. When such a tree is given a parameter message "getLeft", it return leftSubTree and likewise when given the message "getRight" it returns rightSubTree.

 λ(leftSubTree, rightSubTree)
   λ(message)
     if (message == "getLeft") then leftSubTree
     else if (message == "getRight") then rightSubTree

Consider what happens when an expression of the form "(<L> 1 2)" is sent an Eval message with environment E. One semantics for application expressions such as this one is the following: <L>, 1 and 2 are all sent Eval messages with environment E. The integers 1 and 2 immediately reply to the Eval message with themselves.

However <L> responds to the Eval message by creating a closure Actor (process) C that has an address (called body) for <L> an address (called environment) for E. The Actor "(<L> 1 2)" then sends C the message [1 2].

When C receives the message [1 2], it creates a new environment Actor F which behaves as follows:

When it receives a Lookup message for the identifier leftSubTree it responds with 1
When it receives a Lookup message for the identifier rightSubTree it responds with 2
When it receives a Lookup message for any other identifier, it forwards the Lookup message to E.

The Actor (process) C then sends an Eval message with environment F to the following actor (process):

   λ(message)
     if (message == "getLeft") then leftSubTree
     else if (message == "getRight") then rightSubTree

[edit] Arithmetic expressions

For another example consider the Actor for the expression "<expression₁> + <expression₂>" which has addresses for two other actors (processes) <expression₁> and <expression₂>). When the composite expression Actor (process) receives an Eval message with addresses for an environment Actor E and a customer C, it sends Eval messages to expression₁ and <expression₂ with environment E and customer a new Actor (process) C₀. When C₀ has received back two values N₁ and N₂, it sends C the value N₁ + N₂. In this way, the denotational semantics for process calculi and the Actor model provide a denotational semantics for "<expression₁> + <expression₂>" in terms of the semantics for <expression₁> and <expression₂>.

[edit] Delays and Futures

Providing a denotational compositional semantics for delays and futures provides a challenge for denotational semantics.

[edit] Other programming constructs

The denotational compositional semantics presented above is very general and can be used for functional, imperative, concurrent, logic, etc. programs

[edit] Denotational semantics of concurrency

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). Extending denotational semantics to concurrency proved challenging (see unbounded nondeterminism).

[edit] 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.

According to Clinger [1981],

Plotkin's original power domain construction was simplified in [Smyth 1978] which remains the standard introduction to the subject. A number of nondeterministic programming languages have now been given power domain semantics. Of these the semantics of [Francez, Hoare, Lehmann, and de Roever 1979] had the most influence over the development of the denotational model in Clinger's dissertation.

The denotational semantics in Clinger's dissertation is probably the first power domain semantics for languages with true concurrency, but it is not the first power domain semantics for a language with unbounded nondeterminism. [Back 1980] has given a power domain semantics for a language with unboundedly nondeterministic assignment as a primitive operation. Three differences between Back's work and the Actor denotation semantics in Clinger's dissertation stand out:

The source of nondeterminism in Back's paper is basic assignment statements whereas in the Actor model it is message latency.
Back's paper treats nondeterministic sequential programming languages whereas the Actor model is concerned with concurrent programming languages.
The power domain in Back's paper apparently is constructed from a complete underlying domain. This third difference is not entirely clear because Back's power domain construction appears to be nonstandard.

A similarity between Back's work the Actor denotational semantics in Clinger's dissertation is that Back found it necessary to build the power domain out of execution sequences instead of single states: the Actor power domain is built out of Actor event diagrams, which are generalizations of execution sequences.

[edit] 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.

[edit] 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, 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.
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 Hewitt (2006a). The repeated demise of logic programming and why it will be reincarnated What Went Wrong and Why: Lessons from AI Research and Applications. Technical Report SS-06-08. AAAI Press. March 2006.
Carl Hewitt (2006b) What is Commitment? Physical, Organizational, and Social COIN@AAMAS. 2006.

[edit] External links

Denotation Semantics by Lloyd Allison
Structure of Programming Languages I: Denotational Semantics by Wolfgang Schreiner
Denotational Semantics: A Methodology for Language Development by David Schmidt
Presentation by Josh Cogliati
HQL by H. Hernan Moraldo – complete denotational semantics of a small language

Retrieved from "http://en.wikipedia.org../../../d/e/n/Denotational_semantics.html"

Categories: Logic in computer science | Computational models | Formal specification languages | Semantics