VDM Semantics of Programming Languages: Combinators and Monads - Formal Methods and Hybrid Real-Time Systems - page 484

points, and acknowledges the major contributions to formal semantics of Dines
Bjørner and his colleagues over more than three decades.

2 Denotational Semantics

Denotational semantics was initiated by Christopher Strachey in the 1960s [4,5].
Originally it was based on mapping phrases of programs to the untyped λ -
calculus. 1 At the time, it was conjectured that there was no mathematical model
of self-applicable functions, which were allowed by the untyped λ -calculus and
used to define the so-called paradoxical combinator Y (needed by Strachey for
expressing the semantics of loops and recursive procedures). In 1969, Dana Scott
discovered how to construct the missing model, and developed a theory of do-
mains, providing solid foundations for denotational descriptions [3,7].
This section recalls the fundamental principles of denotational semantics. De-
tails specific to the original Oxford style, and the differences between the VDM
and Oxford styles, are covered in the following two sections.
A denotational semantics of a programming language maps each phrase of
the language to its denotation . The denotation represents the contribution of
the phrase to the overall behaviour of any complete program that contains it; in
particular, the denotation of a complete program represents its entire behaviour
when run with particular input. The denotation of a phrase is composed from
the denotations of its subphrases, and is independent of its context.
A programming language is essentially just a set of strings (the texts of the
syntactically legal programs) together with some criteria for implementations of
the language to be regarded as conforming. A language can have many different
denotational semantics, depending on the choice of:

- phrase structure: how programs can be uniquely decomposed into phrases;
- program behaviour: when programs are regarded as equivalent; and
- denotations: how contributions to behaviour are represented by abstract
entities.

The above differences concern the semantic function that maps phrases to de-
notations, and are independent of the framework used to specify that function.
Let us consider them in a bit more detail.

Phrase structure: A set of strings can have many different phrase structures. The
choice of a particular phrase structure determines the compositional structure of
denotations, which may in turn affect the possibilities for choosing denotations.
For example, consider the set of binary numerals: a string of 0s and 1s could be
grouped to the left or to the right (or even both ways). Suppose that the leftmost
digit of a binary numeral is the most significant, and that the 'behaviour' of a
numeral is its numerical value; then grouping to the left is the obvious choice

1 Peter Landin's approach [6] was superficially similar, but involved an extended λ -
calculus with imperative features.