It is always exciting and fruitful when two disparate scientific fields are found to have much in common. Each field is enriched by the different perspective and insights of the other. This has happened recently with category theory and theoretical computer science.

The relations between category theory and computer science constitute an extremely active area of research at the moment. Some evidence of this is given in the short list of references at the end of the book. Among the many places where research is being done are: Aarhus, Carnegie-Mellon, Cambridge, Edinburgh, Glasgow, London, Milan, Oxford, Paris, Pennsylvania, Pisa, Stanford, and Sydney. Topics of current interest include the connections between category theory and functional programming, polymorphism, concurrency, abstract data structures, object-oriented programming, and hardware design.

This book is an introduction to category theory in which several of the connections with computer science are discussed in sufficient detail to give the reader some technical expertise and a feeling for the rich possibilities arising from the happy connection between these two subjects.

What is category theory?

The notion of function is one of the most fundamental in mathematics and science. Functions are used to model variation — for example, the motion of a particle in space; the variation of a quantity like temperature over a space; the symmetries of a geometric object, or of physical laws; the variation of the state of a system over time.

In this section we will introduce the typed formal language PBC for the Propositional logic of Boolean Categories which may be regarded as loop-free propositional dynamic logic with data types. The main result is that the set of formulas valid in all Boolean categories coincides precisely with the set of formulas true in Mfn. We give two proofs. The first works only for atomic Boolean categories, but the construction is very straightforward. The second, general proof uses ultrafilters and follows that of [Kozen 1980] for dynamic algebras.

The language PDL of [Fischer and Ladner 1979] defines programs and formulas by mutual recursion as follows (where we have made notational changes to conform to previous sections of this paper):

Atomic programs are programs; ∅ is a program; if α, β are programs and P is a formula then αβ, α + β, α* and p (the guard corresponding to P) are programs.

Atomic formulas are formulas; true and false are formulas; if P, Q are formulas and α is a program then P∪Q, P′ and < α > P are formulas.

The Kripke model semantics which is standard for PDL is, essentially, Mfn so that α + β = α∪β and α* are available. In particular, if-then-else can be expressed as in 8.24. The identity program is expressible as 0*.

Formal semantics is a topic of major importance in the study of programming languages. Its applications include documenting language design, establishing standards for implementations, reasoning about programs, and generating compilers.

This book is about action semantics, a recently-developed framework for formal semantics. The primary aim of action semantics is to allow useful semantic descriptions of realistic programming languages.

Action semantics combines formality with many good pragmatic features. Regarding comprehensibility and accessibility, for instance, action semantic descriptions compete with informal language descriptions. Action semantic descriptions scale up smoothly from small example languages to full-blown practical languages. The addition of new constructs to a described language does not require reformulation of the already-given description. An action semantic description of one language can make widespread reuse of that of another, related language. All these pragmatic features are highly desirable. Action semantics is, however, the only semantic framework that enjoys them! (For syntax, context-free grammars have similar features, which perhaps accounts for their popularity in language reference manuals.)

Action semantics is compositional, like denotational semantics. The main difference between action semantics and denotational semantics concerns the universe of semantic entities: action semantics uses entities called actions, rather than the higher-order functions used with denotational semantics. Actions are inherently more operational than functions: when performed, actions process information gradually.

Primitive actions, and the various ways of combining actions, correspond to fundamental concepts of information processing. Action semantics provides a particular notation for expressing actions.

• Denotational semantics has poor pragmatic features, due to its use of the λnotation.

• Several so-called algebraic frameworks are essentially operational.

• Genuinely axiomatic frameworks are prone to incompleteness and inconsistency.

• Operational semantics is useful; action semantics makes it easier.

Action semantics is not the only available framework for giving formal semantic descriptions of programming languages. Other frameworks include denotational semantics, various kinds of algebraic semantics, axiomatic semantics, and operational semantics. What is wrong with them all? Why should one prefer action semantics—at least for describing full-scale, realistic programming languages?

Let us look briefly at most of the other frameworks in turn, pointing out their major defects in comparison to action semantics. To make the discussion accessible to those not familiar with the various frameworks, we indicate their main features, and cite primary references. However, a full appreciation of the comparisons requires in-depth familiarity with both action semantics and the other frameworks, as well as a more thorough discussion than can be provided here.

Almost all frameworks for formal semantics are based on context-free abstract syntax, although the notations that they use to specify abstract syntax are quite varied. The grammars that we use in action semantic descriptions perhaps have some significant advantages over other ways of specifying abstract syntax. But our main interest here is in the essential differences concerning the specification of semantics, once abstract syntax has been specified, so let us not pursue this point further.

Part II introduces the details of action notation systematically, explaining the underlying concepts and the intended interpretation of the symbols. It is intended to be read together with Part III, which illustrates the use of action notation in semantic descriptions.

Some of the Appendices provide further details of the foundations of action notation, and summarize the explanations given throughout Part II. Appendix B specifies some algebraic properties of the entire action notation; this also reduces action notation to a reasonably small kernel. Appendix C defines the abstract syntax of the kernel, and gives the formal definition of its meaning, using structural operational semantics. Appendix D summarizes the informal explanations of the full action notation, for convenience of reference. Appendix E gives the complete algebraic specification of the data notation included in action notation.

Navigation

• If this is your first reading, proceed in parallel through Parts II and III: Chapter 4) Chapter 11, Chapter 5, Chapter 12, and so on. This way, you see an illustration of the use of each part of action notation immediately after its introduction

• Alternatively, you could look at each chapter of Part III before the corresponding chapter of Part II. This way, the illustrations in Part III motivate the action notation introduced in Part II.

• If you are revising, and would like an uninterrupted presentation of action notation, proceed straight through Part II.

Part II introduces Boolean categories and establishes their basic structure. A Boolean category is intended to be a minimal framework for the semantics of loop-free control structures including a high-level specification language based on propositional dynamic logic. Coproducts are given a fundamental role in this approach. The axioms on a Boolean category are designed to justify the intuition that a binary coproduct decomposes an object into two disjoint alternatives.

• Basic statements include sequencing, choices, loops, and exits.

• The semantic description of statements illustrates the use of the basic action notation introduced in Chapter 4.

• No special semantic entities are required.

Statements, sometimes called commands, are basic constructs of many programming languages. Together with other constructs, they mainly serve to specify the order in which parts of a program are intended to be performed. We call the performance of a statement its execution.

Implementations usually follow the intended order of performance, although any order providing the same observable behaviour is allowed. Moreover, when the intended order is only partially specified, implementations are free to choose any order consistent with the specified order. Of course, when different orders of performance can lead to different observable behaviours, an implementation only provides one of the possible behaviours in each execution.

The so-called imperative programming languages contain a wide variety of statements. This is in contrast to functional programming languages, where the primary concern is with data rather than with order of performance. Most statements, however, have other kinds of phrases as components, such as expressions and declarations. The few statements that do not involve other kinds of construct don't provide much of a programming language: they allow for sequences, nondeterministic choices, and loops, but not much else. Nevertheless, the semantic description of these simple statements does provide some illustration of the use of the basic action notation introduced in Chapter 4.

• Declarations of variables involve types, which indicate the values that may be assigned to the variables. Assignments are statements.

• The semantics of variable declarations and assignment statements illustrates the use of the imperative action notation introduced in Chapter 8.

• Semantic entities now include variables, types, and access values.

In programs, variables are entities that refer to stored data. The value of a variable is the data to which it currently refers; a variable may be assigned a succession of different values.

This concept of a program variable is quite different from that of a mathematical variable. In mathematics, variables are used to stand for particular unknown values—often the arguments of functions being defined. Although these variables can be ‘assigned’ values, e.g., by function application, their values do not subsequently vary! In the scope of a variable, all occurrences of that variable refer to the same value. In fact mathematical variables correspond exactly to the constant identifiers of programming languages, described in Chapter 14.

A declaration of a variable in a program determines a new variable: one whose value is, in general, independent of that of the values of all other variables. This is called allocating the variable. The declaration then binds an identifier to the variable. Usually the declaration specifies the type of the variable, indicating what sort of value may be assigned to it.

• Action semantic descriptions are divided into modules.

• Grammars are used to specify abstract syntax.

• Semantic equations are used to specify semantic functions.

• Action semantics provides a standard notation for specifying semantic entities (actions, data, yielders).

• The standard notation can be extended and specialized by means of algebraic specifications.

A semantic description consists of three main parts, concerned with specifying abstract syntax, semantic functions, and semantic entities. We specify these parts as separate modules, which, in larger specifications, may themselves be divided into submodules, just as we normally divide technical reports and textbooks into sections and subsections.

Let us adopt the following discipline in our modular specifications: each module has to have a title, and it has to be self-contained, in the sense that all the notation used in a module must be specified there too. Of course, when some module M uses notation that is already specified in another module M′, there is no point in repeating all of M′ literally in M: it is sufficient to refer to Mi from M, using its title. Similarly, when the submodules Mi of a module M use some common notation, we may as well specify that notation just once, at the level of M, letting it be inherited by each Mi. A reference to a module M thus provides not only the notation specified directly in M and its submodules, but also that which is specified in modules referenced by M and in supermodules enclosing M.

• This Appendix gives some examples of possible course assessment projects. They concern MODULA-3, ADA, and functional programming languages. Your lecturer or supervisor might either let you choose between them, or designate which one you are to attempt.

• Your completion of such a project not only documents your active participation in the course, it also serves some important pedagogical purposes. For instance, it gives you the opportunity to revise the material already covered, it helps you appreciate the inherent modularity of action semantic descriptions, and it lets you check whether you have indeed acquired a working knowledge of action semantics.

• You are advised to finish the description of straightforward constructs before proceeding to the more challenging ones. Try to reuse the description of AD as much as possible!

• At Aarhus, the students are expected to work in groups of two or three, handing in as much as they can manage after 25 hours work—without sacrificing quality for quantity! They are given access to the LATEX formatting macros used for the semantic descriptions in this book, and to the LATEX source for Appendix A.

• Actions are semantic entities, used to represent behaviour.

• Action notation includes a basic action notation for specifying control flow.

• Basic actions are not explicitly concerned with any particular kind of information.

• Chapter 11 illustrates the use of basic action notation in the semantic description of statements.

Actions are semantic entities that represent potential information-processing behaviour, i.e., the semantics of programs and of their component phrases, such as statements. Each performance of an action corresponds to a possible behaviour. In this chapter, we restrict our attention to the actions provided by basic action notation. These basic actions are closely related to fundamental concepts of control flow. In subsequent chapters, we enhance basic actions to process various kinds of information, and introduce further actions.

Before we look at our formal notation for actions, let us consider the concepts of control flow that underlie the intended interpretation of the notation. An action performance consists of some atomic steps, made by one or more agents. For now we only consider single-agent performances, and we assume that in any particular performance, steps occur in a definite order, rather than concurrently. This ensures that the current information available when performing a step is well-defined, and that conflicting changes to the current information cannot arise. Chapter 10 explains multi-agent performances, where a dynamically-changing distributed system of agents proceeds to perform separate actions with ‘true’ concurrency, with asynchronous sending of messages between agents.

• The meta-notation used in this book consists of positive Horn clauses, constraints, and modules, together with some convenient abbreviations.

• The informal summary of the meta-notation given in this Appendix provides a concise explanation of each construct.

• The description of the formal abbreviations used in the meta-notation reduces the metanotation to a simple kernel.

• A context-free grammar specifies the abstract syntax of the meta-notation, and suggests its concrete syntax.

• The logic used for reasoning about the meta-notation consists of the standard inference rules for Horn clause logic with equality, together with some Horn clause axioms.

• The formal semantics of the meta-notation is, unfortunately, out of the scope of this book.

Informal Summary

Meta-notation is for specifying formal notation: what symbols are used, how they may be put together, and their intended interpretation.

Our meta-notation here supports a unified treatment of sorts and individuals: an individual is treated as a special case of a sort. Thus operations can be applied to sorts as well as individuals. A vacuous sort represents the lack of an individual, in particular the undefined result of a partial operation. Sorts may be related by inclusion; sort equality is just mutual inclusion. But a sort is not determined just by the set of individuals that it includes: it has an intension, stemming from the way it is expressed.

• Reflective action notation is for specifying abstractions and their enaction.

• Abstractions are data that incorporate actions. The incorporated action can be supplied with transients and bindings.

• Chapter 16 illustrates the use of reflective action notation in the semantic description of procedure declarations.

An abstraction is a datum that merely incorporates a particular action. It corresponds to the ‘code’ for the action, which could be implemented as a sequence of machine instructions, or as a pointer to such a sequence. We use abstractions to represent the semantics of programming constructs such as procedures.

We may form an abstraction directly from an action. The abstraction, just like any other datum, can then be given as a transient, bound to a token, etc. Ultimately, the abstraction should be enacted, so as to perform the incorporated action.

Forming an abstraction may be regarded as a kind of reification, and enacting it as reflection. Reification and reflection are general concepts concerned with passing from components of an implicit, underlying computational state to values that can be manipulated explicitly, and vice versa [FW84]. Thus the evaluation of yielders for referring to the given transients, current bindings, etc., can also be regarded as reification, with the performance of primitive actions such as give Y and produce Y corresponding to reflection.

The action incorporated in an abstraction is usually performed in a context different to that where the abstraction itself occurs.