Denotational semantics

In computer science, denotational semantics is one of the approaches to formalize the semantics of computer systems by constructing mathematical objects (called denotations or meanings) which express the semantics of these systems. Originally the field was developed more narrowly to deal only with a system that is defined by a computer program. Later the field broadened to include systems not defined by a single program as found in networking and concurrent systems. The field originated in work by Christopher Strachey and Dana Scott in the 1960s. Other approaches include axiomatic semantics and operational semantics. (See formal semantics of programming languages.)

Denotational semantics as originally developed by Strachey and Scott interpreted the denotation (meaning) of a computer program as a function that mapped input into output. Functions later this proved to be too limiting for the denotations (meanings) of networked and concurrent systems.

Fixed point semantics

The denotational theory of programming language semantics is concerned with finding mathematical objects that represent what programs do. Examples of such objects are partial functions, sequences of states, and Actor event diagrams. Usually there is a partial ordering ≤ on these objects with x≤y meaning that x is compatible with but possibly less defined than y. In other words, x approximates y. If the objects are partial functions, for example, f≤g may mean that f agrees with g on all values for which f is defined. If the objects are Actor event diagram denotations, x≤y means that x is a possible initial history of y.

As computation continues, the approximations should become better so if we have ∀i∈ω x_{i≤xi+1 then the least upper bound ∨i∈ω xi should exist. The property just stated is called ω-completeness.}

The object representing a program S is found by solving by constructing increasingly better approximations from an initial begining approximation called ⊥ using some approximation building function progression_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≤xi+1 then}

progression_S(∨_i∈ω x_i) = ∨_i∈ω progression_S(x_i)

This just stated property of progression_s is called ω-continuity.

Now it is desired to constuct a denotation (meaning ) for S as follows: Denote_S ≡ ∨_i∈ωprogression_Sⁱ(⊥).

A central question of denotational semantics is to characterize when it is possible to create denotations (meanings) in according to the above construct. Obviously if the the denotations (meanings) that we are using is ω-complete and 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.

Denotational semantics of functional programs

The denotational semantics of functions provides an example of fixed point semantics.

Example of factorial function

Consider the factorial function which is defined on all non-negative 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) = {<0,1>,<1,1>,<2,2>,<3,6>,<4,24>…}

The denotation (meaning) Denote_factorial for a program factorial 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 Denote_factorial is a ω-continuous (see definition in section above).

Derivation from Actor Semantics

The Actor model provides a foundation for deriving the denotational semantics of functions as demonstrated first by a theorem of Carl Hewitt and Henry Baker [1977]:

If an Actor f behaves like a mathematical function, then D_f is a continuous functional and graph(f) is the limit of D_f beginning with the empty graph. Also graph(f) is the minimal fixed point of D_f where

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

Compositionality

An important aspect of denotational semantics 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₂>.

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

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

The Actor C then sends an Eval message with enviornment F to the following actor:

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

Arithmetic expressions

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

Delayed evaluation

Providing a compositional semantics for delayed evaluation provides a challenge for denotational semantics. The problem with classical approaches for compositional denotatonal sementics in dealing with expressions of form "delay <Expression>" has been how to formaize the semantics of the evaluation of <Expression>.

The Actor model provides a perfectly reasonable account:

The delay expression responds to an <Eval> message with environment E by creating a closure Actor C that has an address (called body) for <Expression> an address (called environment) for E.

When C receives a message M with Customer₀, it creates a new Actor Customer₁ and sends <Expression> an Eval message with environment E and the address of Customer₁.

When Customer₁ receives a value V, it sends V the message M with Customer₀.

Other programming language constructs can be provided compositional semantics in similar ways.

The Actor model compositional semantics is very general and can be used for functional, imperative, concurrent, logic, etc. programs

Denotational semantics of concurrency

Extending denotational semantics to concurrency proved challenging. See unbounded nondeterminism.

The domain of Actor computations

Clinger [1981] explained the domain of Actor computations as follows:

The augmented Actor event diagrams [see Actor model theory] form a partially ordered set < Diagrams,  ≤ > from which to construct the power domain P[Diagrams] (see the section on [[Denotational semantics#Denotations|Denotations) below). The augmented diagrams are partial computation histories representing "snapshots" [relative to some frame of reference] of a computation on its way to being completed. For x,y∈Diagrams, x≤y means x is a stage the computation could go through on its way to y. The completed elements of Diagrams represent computations that have terminated and nonterminating computations that have become infinite. The completed elements may be characterized abstractly as the maximal elements of Diagrams [see William Wadge 1979]. Concretely, the completed elements are those having non pending events. Intuitively, Diagrams is not ω-complete because there exist increasing sequences of finite partial computations

x₀ ≤ x₁ ≤ x₂ ≤ x₃ ≤ ...

in which some pending event remains pending forever while the number of realized events grows without bound, contrary to the requirement of finite [arrival] delay. Such a sequence cannot have a limit, because any limit would represent a completed nonterminating computation in which an event is still pending.

To repeat, the actor event diagram domain Diagrams is incomplete because of the requirement of finite arrival delay, which allows any finite delay between an event and an event it activates but rules out infinite delay.

Denotations

In his doctoral dissertation, Will Clinger explained how power domains are obtained from incomplete domains as follows:

From the article on Power domains: P[D] is the collection of downward-closed subsets of domain D that are also closed under existing least upper bounds of directed sets in D. Note that while the ordering on P[D] is given by the subset relation, least upper bounds do not in general coincide with unions.

For the actor event diagram domain Diagrams, an element of P[Diagrams] represents a list of possible initial histories of a computation. Since for elements x and y of Diagrams, x≤y means that x is an initial segment of the initial history y, the requirement that elements of P[Diagrams] be downward-closed has a clear basis in intuition.

...

Usually the partial order from which the power domain is constructed is required to be ω-complete. There are two reasons for this. The first reason is that most power domains are simply generalizations of domains that have been used as semantic domains for conventional sequential programs, and such domains are all complete because of the need to compute fixed points in the sequential case. The second reason is that ω-completeness permits the solution of recursive domain equations involving the power domain such as

R ≈ S → P[S + (S $\times$ R)]

which defines a domain of resumptions [Gordon Plotkin 1976]. However, power domains can be defined for any domain whatsoever. Furthermore the power domain of a domain is essentially the power domain of its ω-completion, so recursive equations involving the power domain of an incomplete domain can still be solved, provide the domains to which the usual constructors (+, $\times$,  → , and *) are applied are ω-complete. It happens that defining Actor semantics as in Clinger [1981] does not require solving any recursive equations involving the power domain.

In short, there is no technical impediment to building power domains from incomplete domains. But why should one want to do so?

In behavioral semantics, developed by Irene Greif, the meaning of program is a specification of the computations that may be performed by the program. The computations are represented formally by Actor event diagrams. Greif specified the event diagrams by means of causal axioms governing the behaviors of individual Actors [Greif 1975].

Henry Baker has presented a nondeterministic interpreter generating instantaneous schedules which then map onto event diagrams. He suggested that a corresponding deterministic interpreter operating on sets of instantaneous schedules could be defined using power domain semantics [Baker 1978].

The semantics presented in [Clinger 1981] is a version of behavioral semantics. A program denotes a set of Actor event diagrams. The set is defined extensionally using power domain semantics rather than intensionally using causal axioms. The behaviors of individual Actors is defined functionally. It is shown, however, that the resulting set of Actor event diagrams consists of exactly those diagrams that satisfy causal axioms expressing the functional behaviors of Actors. Thus Greif's behavioral semantics is compatible with a denotational power domain semantics.

Baker's instantaneous schedules introduced the notion of pending events, which represent messages on the way to their targets. Each pending event must become an actual (realized) arrival event sooner or later, a requirement referred to as finite delay. Augmenting Actor event diagrams with sets of pending events helps to express the finite delay property, which is characteristic of true concurrency [Schwartz 1979].

Sequential computations form an ω-complete subdomain of the domain of Actor computations

In his 1981 dissertation, Clinger showed how sequential computations form a subdomain of concurrent computations:

Instead of beginning with a semantics for sequential programs and then trying to extend it for concurrency, Actor semantics views concurrency as primary and obtains the semantics of sequential programs as a special case.

...

The fact that there exist increasing sequences without least upper bounds may seem strange to those accustomed to thinking about the semantics of sequential programs. It may help to point out that the increasing sequences produced by sequential programs all have least upper bounds. Indeed, the partial computations that can be produced by sequential computation form an ω-complete subdomain of the domain of Actor computations Diagrams. An informal proof follows.

From the Actor point of view, sequential computations are a special case of concurrent computations, distinguishable by their event diagrams. The event diagram of a sequential computation has an initial event, and no event activates more than one event. In other words, the activation ordering of an sequential computation is linear; the event diagram is essentially a conventional execution sequence. This means that the finite elements of Diagrams

x₀ ≤ x₁ ≤ x₂ ≤ x₃ ≤ ...

corresponding to the finite initial segments of a sequential execution sequence all have exactly one pending event, excepting the largest, completed element if the computation terminates. One property of the augmented event diagrams domain < Diagrams,  ≤ > is that if x≤y and x≠y, then some pending event of x is realized in y. Since in this case each x_i has at most one pending event, every pending event in the sequence becomes realized. Hence the sequence

x₀ ≤ x₁ ≤ x₂ ≤ x₃ ≤ ...

has a least upper bound in Diagrams in accord with intuition.

The above proof applies to all sequential programs, even those with choice points such as guarded commands. Thus Actor semantics includes sequential programs as a special case, and agrees with conventional semantics of such programs.

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:

1. The source of nondeterminism in Back's paper is basic assignment statements whereas in the Actor model it is message latency.
2. Back's paper treats nondeterministic sequential programming languages whereas the Actor model is concerned with concurrent programming languages.
3. 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.

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 a branch of model theory. and has many 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

• 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. (Quoted by permission of author.)
• 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 026269171X.
• 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.

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