In computer science, denotational semantics (initially known as mathematical semantics or Scott–Strachey semantics) is an approach of formalizing the meanings of programming languages by constructing mathematical objects (called denotations) that describe the meanings of expressions from the languages. Other approaches providing formal semantics of programming languages include axiomatic semantics and operational semantics.
Broadly speaking, denotational semantics is concerned with finding mathematical objects called domains that represent what programs do. For example, programs (or program phrases) might be represented by partial functions or by games between the environment and the system.
An important tenet of denotational semantics is that semantics should be compositional: the denotation of a program phrase should be built out of the denotations of its subphrases.
Historical development
Denotational semantics originated in the work of Christopher Strachey and Dana Scott published in the early 1970s. As originally developed by Strachey and Scott, denotational semantics provided the meaning of a computer program as a function that mapped input into output. 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.
Denotational semantics has been developed for modern programming languages that use capabilities like concurrency and exceptions, e.g., Concurrent ML, CSP, and Haskell. The semantics of these languages is compositional in that the meaning of a phrase depends on the meanings of its subphrases. 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. Also, E1 or E2 might throw an exception which could terminate the execution of the other one. The sections below describe special cases of the semantics of these modern programming languages.
Meanings of recursive programs
Denotational semantics is ascribed to a program phrase as a function from an environment (holding current values of its free variables) to its denotation. For example, the phrase produces a denotation when provided with an environment that has binding for its two free variables: and . If in the environment has the value 3 and has the value 5, then the denotation is 15.
A function can be represented as a set of ordered pairs of argument and corresponding result values. For example, the set { (0,1), (4,3)} denotes a function with result 1 for argument 0, result 3 for the argument 4, and undefined otherwise.
Consider for example the factorial function, which might be defined recursively as: int factorial(int n) { if (n == 0) then return 1; else return n * factorial(n-1); }
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. At the beginning, we start with no calls - hence nothing is defined. 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. In the limit we get a total function from to defined everywhere in its domain.
Formally we model each approximation as a partial function . Our approximation is then repeatedly applying a function implementing "make a more defined partial factorial function", i.e. , starting with the empty function (empty set). F could be defined in code as follows (using Map<int,int> for ): int factorial_nonrecursive(Map<int,int> factorial_less_defined, int n) { if (n == 0) then return 1; else if (fprev = lookup(factorial_less_defined, n-1)) then return n * fprev; else return NOT_DEFINED; }
Map<int,int> F(Map<int,int> factorial_less_defined) { Map<int,int> new_factorial = Map.empty(); for (int n in all<int>()) { if (f = factorial_nonrecursive(factorial_less_defined, n) != NOT_DEFINED) new_factorial.put(n, f); } return new_factorial; }