What we mean by semantics

David Turner reviews a new textbook on computer programming languages.

The theory of programming languages is an important and well-developed part of computer science. John Reynolds has made notable contributions to the field over a period of several decades, so a textbook from him on the subject is to be welcomed.

The theories covered are semantic ones, of three kinds: denotational semantics, operational semantics such as transition systems, and inference rules for proving theorems about programs. The initial chapter introduces predicate calculus and uses it to illustrate the four fundamental ideas used throughout the book - abstract syntax, denotational semantics, inference rules and binding rules.

The book covers a wide range of languages in 19 chapters. Each is followed by exercises and generally excellent bibliographic notes. The main emphasis of the book is on topics that were well understood by the mid-1980s, but more recent topics are covered by the suggested references at the end of each chapter.

The book breaks with tradition by dealing with imperative languages before functional languages. The denotational semantics of simple imperative languages are developed systematically in four chapters, starting from store semantics and leading up to continuation semantics in a series of steps as more language features are added. There is a succinct and clear exposition of elementary domain theory to support this. Both Hoare and Dijkstra-style proof rules are developed, for partial and total correctness respectively, each rule being derived from the denotational semantics. This includes reasoning about arrays.

An approach to operational semantics based on transition systems is then introduced, and applied over four chapters to the exposition of non-determinism and concurrency, covering guarded commands, monitors and critical regions, and communicating sequential processes (CSP).

The second part of the book deals with functional languages and imperative languages supporting functional abstraction (procedures are not discussed in the first part of the book). Topics covered include the lambda calculus, eager and lazy functional languages and ISWIM-like languages (that is, lambda calculus plus imperative features). Both direct and continuation semantics are explored, and the relationship between them.

The last section of the book (apart from a chapter at the end exploring properties of Algol-60) deals with type systems and theories of type, starting with simple types and proceeding via subtypes and intersection types to the second-order lambda calculus.

Some general comments: the mathematics used is clearly explained and elementary in character - some set theory, functions, relations - and is summarised in an appendix. Some difficult but important topics are avoided - for example the domain theory does not cover solving recursive domain equations. Philosophical issues are also avoided. The first example of denotational semantics is a metacircular definition of first-order logic, with no mention of any possible controversy about the meaning of the logical operators.

I was unhappy that data types are introduced so late, and that there is no discussion of associated induction principles. In my opinion types should have been a basic theme from the opening chapter. It is also curious that the book omits discussion of the widely used Hindley/Milner system of polymorphic typing, while treating the more complex polymorphism of the second-order lambda calculus.

The treatment of functional languages is less satisfactory than that of imperative languages. There is no discussion of equational reasoning, which is their main advantage and the analogue for them of the Hoare or Dijkstra proof rules for imperative languages. Even in the case of the lambda calculus it is not mentioned that there is an equational theory.

A decision to present all the languages in the book in the same uniform syntax suppresses features of modern functional notation, such as pattern matching, which are closely related to equational reasoning.

The main emphasis is on various evaluation models of functional programming and their denotational semantics. Unlike the chapters on imperative programming there is no parallel development of proof rules.

Topics not covered include: coinduction (or even induction on simple data types), parametricity and propositions-as-types.

The semantics attributed by Reynolds to non-strict ("lazy") functional languages makes a distinction in the function space between the wholly undefined value and a function that always returns undefined. In fact, in a strongly typed and purely functional non-strict language there would be no possible observation that could distinguish between these two entities. Necessarily so, since a function is an abstract value that can be inspected only by applying it to an argument. The reduction relation that Reynolds gives for what he calls "normal order evaluation", and distinguishes from classical normal order reduction, leads to a theory that is insufficiently abstract to provide the correct model for typed lazy functional languages.

In summary, this is a book of mixed qualities. The first half of the book provides a very serviceable survey of the main semantic theories of imperative languages, including concurrency, although it is dated in not discussing any concurrent language model more recent than CSP. I would certainly consider using these nine chapters in a senior undergraduate course, but for theories of functional programming and of types I would be concerned that the material in the book is too focused on denotational semantics to the exclusion of other theories.

David Turner is professor of computation, University of Kent at Canterbury.