|
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. 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: 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 progressionS to construct a denotation (meaning ) for S as follows Hewitt 2006b: DenoteS ≡ ∨i∈ω progressionSi(⊥S). It would be expected that progressionS would be monotone, i.e., if x≤y then progressionS(x)≤progressionS(y). More generally, we would expect that If ∀i∈ω xi≤xi+1, then progressionS(∨i∈ω xi) = ∨i∈ω progressionS(xi) This last stated property of progressionS 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 DenoteS. A fundamental theorem of computational domain theory is that if progressionS is ω-continuous then DenoteS will exist. It follows from the ω-continuity of progressionS that progressionS(DenoteS) = DenoteS The above equation motivates the terminology that DenoteS is a fixed point of progressionS. Furthermore this fixed point is least among all fixed points of progressionS. 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 nThe 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) Denotefactorial for the factorial program is constructed as follows: Denotefactorial = graph(factorial) = ∪i∈ω progressionfactoriali() where progressionfactorial(g) ≡ λ(n)if (n==0)then 1 else n Note: progressionfactorial is a fix point operator (see definition in section above) whose least fixed point is Denotefactorial, i.e., Denotefactorial = progressionfactorial(Denotefactorial) Also progressionfactorial is ω-continuous (see definition in section above). 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 progressionf is a Scott continuous functional whose least fixed point is graph(f) = ∪i∈ω progressionfi() where progressionf(G)≡ The paper by Hewitt and Baker contained a small bug in the definition of immediate-descendantsf that was corrected in Will Clinger 1981. 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: 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 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 " 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 λ(leftSubTree, rightSubTree) λ(message) if (message == "getLeft") then leftSubTree else if (message == "getRight") then rightSubTree Consider what happens when an expression of the form "( However When C receives the message 1 2, it creates a new environment Actor F which behaves as follows: 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 Arithmetic expressions For another example consider the Actor for the expression " Delayed evaluation Providing a denotational compositional semantics for delayed evaluation provides a challenge for denotational semantics. The problem with classical approaches for compositional denotational semantics in dealing with expressions of form "delay The denotational semantics of process calculi and the Actor model provides a perfectly reasonable account: The delay expression responds to an When C receives a message M with Customer0, it creates a new Actor (process) Customer1 and sends When Customer1 receives a value V, it sends V the message M with Customer0. Other programming language constructs can be provided compositional semantics in similar ways. The denotational compositional semantics presented above is very general and can be used for functional, imperative, concurrent, logic, etc. programs 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). 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:
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. 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. See also | |||||||
|
| ||||||||
 |
|
| |