Denotational semantics

Broadly speaking, denotational semantics is concerned with finding mathematical objects called domains that represent what programs do.

Denotational semantics originated in the work of Christopher Strachey and Dana Scott published in the early 1970s.

[1][2] As originally developed by Strachey and Scott, denotational semantics provided the meaning of a computer program as a function that mapped input into output.

[2] To give meanings to recursively defined programs, Scott proposed working with continuous functions between domains, specifically complete partial orders.

As described below, work has continued in investigating appropriate denotational semantics for aspects of programming languages such as sequentiality, concurrency, non-determinism and local state.

For example, the meaning of the applicative expression f(E1,E2) is defined in terms of semantics of its subphrases f, E1 and E2.

In a modern programming language, E1 and E2 can be evaluated concurrently and the execution of one of them might affect the other by interacting through shared objects causing their meanings to be defined in terms of each other.

The sections below describe special cases of the semantics of these modern programming languages.

[2] A function can be represented as a set of ordered pairs of argument and corresponding result values.

Consider for example the factorial function, which might be defined recursively as: To provide a meaning for this recursive definition, the denotation is built up as the limit of approximations, where each approximation limits the number of calls to factorial.

In the next approximation, we can add the ordered pair (0,1), because this doesn't require calling factorial again.

Similarly we can add (1,1), (2,2), etc., adding one pair each successive approximation because computing factorial(n) requires n+1 calls.

Furthermore, this iterative process of better approximations of the factorial function forms an expansive (also called progressive) mapping because each

The concept of power domains has been developed to give a denotational semantics to non-deterministic sequential programs.

[7] Many researchers have argued that the domain-theoretic models given above do not suffice for the more general case of concurrent computation.

[10][11] State (such as a heap) and simple imperative features can be straightforwardly modeled in the denotational semantics described above.

For example, the type of lists of numbers can be specified by This section deals only with functional data structures that cannot change.

Conventional imperative programming languages would typically allow the elements of such a recursive list to be changed.

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

[15] The problem of full abstraction for the sequential programming language PCF was, for a long time, a big open question in denotational semantics.

It is for this reason that the approach using domains, as introduced above, yields a denotational semantics that is not fully abstract.

This open question was mostly resolved in the 1990s with the development of game semantics and also with techniques involving logical relations.

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

For semantics in the traditional style, adequacy and full abstraction may be understood roughly as the requirement that "operational equivalence coincides with denotational equality".

Milner has advocated modelling location and interaction by working in a category with interfaces as objects and bigraphs as morphisms.

Within computer science, there are connections with abstract interpretation, program verification, and model checking.