In constructing a large program, it is vital to be able to divide the program into parts, often called modules, and to specify these modules with sufficient precision that one can program each module knowing only the specification of the other modules.

One of the main benefits of modern type theory is the realization that the type of a module is in fact a formal specification of the module. Indeed (although we will not discuss them in this book) there are implemented type-based systems such as NuPrl and Coq which can handle specifications of functional programs that are as expressive and flexible as the specifications of imperative programs in Chapter 3. As with the specifications of Chapter 3, however, considerable human assistance is needed to insure that a program meets its specification.

In this chapter, we will examine more limited systems for which the check that a module meets its specification can be performed efficiently and without human intervention. What is surprising is the extent to which these less expressive systems can still detect programming errors.

We begin with a discussion of type definitions, especially abstract type definitions that make it possible to separate the definition of an abstract type, including both its representation and the relevant primitive operations, from the part of the program that uses the abstract type but is independent of its representation and the implementation of the primitives. We then examine a more general approach based on existentially quantified types and polymorphic functions.

A nondeterministic program is one that does not completely determine the behavior of a computer, so that different executions of the same program with the same initial state and input can give different results. Although concurrent programs are usually nondeterministic, the topics of nondeterminism and concurrency are distinct, and it is pedagogically sensible to consider nondeterminism by itself before plunging on to concurrency.

Moreover, even with purely sequential computation, nondeterministic programs are often desirable because they avoid unnecessary commitments. Such commitments can make programs harder to read and to reason about. Even more seriously, in programs that use abstract types, they can place unnecessary constraints on the choice of data representations.

(Just as one can have nondeterministic sequential programs, one can also have deterministic concurrent ones — often called parallel programs — as will be evident when we consider functional programming languages.)

In this chapter we will explore Dijkstra's guarded commands, which are the most widely accepted and studied mechanism for extending the simple imperative language to nondeterministic programming.

In contrast to the previous chapters, we will begin with operational semantics, extending the development of the previous chapter. Then, after introducing powerdomains, we will give a direct denotational semantics for our nondeterministic language (excluding intermediate input and output). Finally, we will extend the specification methods of Chapter 3 to nondeterminism (again excluding input and output) and also deal briefly with weakest preconditions.

Before proceeding further, however, we must clear up a potential confusion. In automata theory, the result of a nondeterministic automaton is defined to be the the union of the results of all possible executions.

Most serious programming languages combine imperative aspects, which describe computation in terms of state-transformation operations such as assignment, and functional or applicative aspects, which describe computation in terms of the definition and application of functions or procedures. To gain a solid understanding, however, it is best to begin by considering each of these aspects in isolation, and to postpone the complications that arise from their interactions.

Thus, beginning in this chapter and continuing through Chapter 7 (nondeterminism) and Chapters 8 and 9 (concurrency), we will limit ourselves to purely imperative languages. Then, beginning in Chapter 10, we will turn to purely functional languages. Languages that combine imperative and functional aspects will be considered in Chapter 13 (Iswim-like languages) and Chapter 19 (Algol-like languages).

In this chapter, we consider a simple imperative language that is built out of assignment commands, sequential composition, conditionals (i.e. if commands), while commands, and (in Section 2.5) variable declarations. We will use this language to illustrate the basic concept of a domain, to demonstrate the properties of binding in imperative languages, and, in the next chapter, to explore formalisms for specifying and proving imperative program behavior. In later chapters we will explore extensions to this language and other approaches to describing its semantics.

At an intuitive level, the simple imperative language is so much a part of every programmer's background that it will hold few surprises for typical readers. As in Chapter 1, we have chosen for clarity's sake to introduce novel concepts such as domains in a familiar context. More surprising languages will come after we have sharpened our tools for specifying them.

In this chapter, we extend the simple imperative language and the methods for reasoning about its programs to include one-dimensional arrays with integer subscripts. Although more elaborate and varied forms of arrays are provided by many programming languages, such simple arrays are enough to demonstrate the basic semantical and logical properties of arrays.

There are two complementary ways to think about arrays. In the older view, which was first made explicit in early work on semantics by Christopher Strachey, an array variable is something that one can apply to an integer (called a subscript) to obtain an “array element” (in Strachey's terminology, an “L-value”), which in turn can be either evaluated, to obtain a value, or assigned, to alter the state of the computation. In the newer view, which is largely due to Hoare but has roots in the work of McCarthy, an array variable, like an ordinary variable, has a value — but this value is a function mapping subscripts into ordinary values. Strachey's view is essential for languages that are rich enough that arrays can share elements. But for the simple imperative language, and especially for the kind of reasoning about programs developed in the previous chapter, Hoare's view is much more straightforward.

Abstract Syntax

Clearly, array variables are a different type of variable than the integer variables used in previous chapters.

Partial recursive, or computable functions, may be defined in a number of equivalent ways. This is what Church's thesis is about: all definitions of computability turn out to be equivalent. Church's thesis justifies some confidence in ‘semi-formal’ arguments, used to show that a given function is computable. These arguments can be accepted only if at any moment, upon request, the author of the argument is able to fully formalize it in one of the available axiomatizations.

In this summary, functions are always partial, unless otherwise specified.

Partial recursive functions

The most basic way of defining computable functions is by means of computing devices of which Turing machines are the most well known. A given Turing machine defines, for each n, a partial function f : ωn → ω. More mathematical presentations are by means of recursive program schemes, or by means of combinations of basic recursive functions.

Theorem A1.1.1 (Gödel-Kleene)For any n, the set of Turing computable functions from ωn to ω) is the set of partial recursive functions from ωn to ω, where by definition the class of partial recursive (p.r.) functions is the smallest class containing:

• : ω → ω defined by 0(x) = 0.

• succ : ω → ω (the successor function).

• Projections πn,i : ωn → ω defined by πn,i(x1,…,xn) = xi, and closed under the following constructions:

• Composition: If f1 : ωm → ω, …, fn : ωm → ω and g : ωn → ω are partial recursive, then g ∘ 〈f1, …, fn〉 : ωm → ω is partial recursive.

• […]

In this chapter, we provide a finer analysis of algebraicity. The central result – which was conjectured by Plotkin and was first proved in [Smy83a] – is that there exists a maximum cartesian closed full subcategory (full sub-CCC) of ω Acpo (the category of ω-algebraic cpo's). Jung has extended this result: he has characterized the maximal cartesian closed full subcategories of Acpo and Adcpo (and of ω Adcpo as well).

In section 5.1, we define continuous dcpo's, which are dcpo's where approximations exist without being necessarily compact. Continuous lattices have been investigated in depth from a mathematical perspective [GHK+80]. Our interest in continuous dcpo's arises from the fact that retracts of algebraic dcpo's are not algebraic in general, but are continuous. Much of the technical work involved in our quest of maximal full cartesian closed subcategories of (d)cpo's involves retracts. In section 5.2, we introduce two cartesian closed categories: the category of profinite dcpo's and the category of L-domains, both with continuous functions as morphisms. In section 5.3, we show that the algebraic L-domains and the bifinite domains form the two maximal cartesian closed full subcategories of Acpo, and derive Smyth's result for ωAcpo with little extra work. In section 5.4, we treat more sketchily the situation for Adcpo. The material of sections 5.3 and 5.4 is based on [Jun88]. In section 5.5, we show a technical result needed in section 5.3: a partial order is a dcpo if and only if all its well-founded subsets have a lub.

Girard's linear logic [Gir87] is an extension of propositional logic with new connectives providing a logical treatment of resource control. As a first hint, consider the linear λ-terms, which are the λ-terms defined with the following restriction: when an abstraction λx.M is formed, then x occurs exactly once in M. Linear λ-terms are normalized in linear time, that is, the number of reduction steps to their normal form is proportional to their size: a linear β-redex (λx.M)N involves no duplication of the argument N. Thus all the complexity of normalization comes from non-linearity.

Linear logic pushes the limits of constructivity much beyond intuitionistic logic. A proper proof theoretical introduction to linear logic is beyond the scope of this book. In this chapter, we content ourselves with a semantic introduction. By doing so, we actually follow the historical thread: the connectives of linear logic arose from the consideration of (a particularly simple version of) the stable model.

In section 13.1, we examine stable functions between coherence spaces, and discover two decompositions. First the function space E → E′ is isomorphic to a space (!E)⊸E′, where ⊸ constructs the space of linear functions, and where! is a constructor which allows reuse of data. Intuitively, linear functions, like linear terms, can use their input only once. On the other hand, the explicit declaration of reusability,!, allows us to recover all functions and terms.

We introduce a fundamental duality that arises in topology from the consideration of points versus open sets. A lot of work in topology can be done by working at the level of open sets only. This subject is called the pointless topology, and can be studied in [Joh82]. It leads generally to formulations and proofs of a more constructive nature than the ones ‘with points’. For the purpose of computer science, this duality is quite suggestive: points correspond to programs, and open sets to program properties. The investigation of Stone duality for domains has been pioneered by Martin-Löf [ML83] and by Smyth [Smy83b]. The work on intersection types, particularly in relation with the D∞ models, as exposed in chapter 3, appears as an even earlier precursor. We also recommend [Vic89], which offers a computer science oriented introduction to Stone duality.

In section 10.1, we introduce locales, and Stone duality in its most abstract form. In sections 10.2 and 10.4, we specialize the construction to various categories of dcpo's and continuous functions, most notably those of Scott domains and of profinite dcpo's (cf. definition 5.2.2). On the way, in section 10.3, we prove Stone's theorem: every Boolean algebra is order-isomorphic to an algebra of subsets of some set X, closed under set theoretical intersection, union, and complementation. The proof of Stone's theorem involves a form of the axiom of choice (Zorn's lemma), used in the proof of an important technical lemma known as Scott open filter theorem.

Denotational semantics is concerned with the mathematical meaning of programming languages. Programs are to be interpreted in categories with structure by which we mean initially sets and functions, and later, suitable topological spaces and continuous functions. The main goals of this branch of computer science are, in our belief:

• To provide rigorous definitions that abstract away from implementation details, and that can serve as an implementation independent reference.

• To provide mathematical tools for proving properties of programs: as in logic, semantic models are guides in designing sound proof rules, that can then be used in automated proof-checkers like LCF.

Historically the first goal came first. In the sixties Strachey was writing semantic equations involving recursively defined data types without knowing if they had mathematical solutions. Scott provided the mathematical framework, and advocated its use in a formal proof system called LCF. Thus denotational semantics has from the beginning been applied to the two goals.

In this book we aim to present in an elementary and unified way the theory of certain topological spaces, best presented as order theoretical structures, that have proved to be useful in the modelling of various families of typed λ-calculi considered as core programming languages and as meta-languages for denotational semantics. This theory is now known as Domain Theory, and has been founded as a subject by Scott and Plotkin.

The notion of continuity used in domain theory finds its origin in recursion theory.

Category theory has been tightly connected to abstract mathematics since the first paper on cohomology by Eilenberg and Mac Lane [EML45] which establishes its basic notions. This appendix is a reminder of a few elementary definitions and results in this branch of mathematics. We refer to [ML71, AL91] for adequate introductions and wider perspectives.

In mathematical practice, category theory is helpful in formalizing a problem, as it is a good habit to ask in which category we are working in, if a certain transformation is a functor, if a given subcategory is reflective, etc. Using category theoretical terminology, one can often express a result in a more modular and abstract way. A list of ‘prescriptions’ for the use of category theory in computer science can be found in [Gog91].

Categorical logic is a branch of category theory that arises from the observation due to Lawvere that logical connectives can be suitably expressed by means of universal properties. In this way one represents the models of, say, intuitionistic propositional logic, as categories with certain closure properties where sentences are interpreted as objects and proofs as morphisms (cf. section 4.3).

The tools developed in categorical logic begin to play a central role in the study of programming languages. A link between these two apparently distant topics is suggested by:

• The role of (typed) λ-calculi in the work of Landin, McCarthy, Strachey, and Scott on the foundations of programming languages.

• […]

In first approximation, typed λ-calculi are natural deduction presentations of certain fragments of minimal logic (a subsystem of intuitionistic logic). These calculi have a natural computational interpretation as core of typed functional languages where computation, intended as βη-reduction, corresponds to proof normalization. In this perspective, we reconsider in section 4.1 the simply typed λ-calculus studied in chapter 2. We exhibit a precise correspondence between the simply typed λ-calculus and a natural deduction formalization of the implicative fragment of propositional implicative logic.

Next, we address the problem of modelling the notions of βη-reduction and equivalence. It turns out that simple models can be found by interpreting types as sets and terms as functions between these sets. But, in general, which are the structural properties that characterize such models? The main problem considered in this chapter is that of understanding what is the model theory of simply typed and untyped λ-calculi. In order to answer this question, we introduce in section 4.2 the notion of cartesian closed category (CCC). We present CCC's as a natural categorical generalization of certain adjunctions found in Heyting algebras. As a main example, we show that the category of directed complete partial orders and continuous functions is a CCC.

The description of the models of a calculus by means of category theoretical notions will be a central and recurring topic of this book. We will not always fully develop the theory but in this chapter we can take advantage of the simplicity of the calculus to go into a complete analysis.