This chapter is devoted to the semantics of sequentiality. At first order, the notion of sequential function is well-understood, as summarized in theorem 6.5.4. At higher orders, the situation is not as simple. Building on theorem 13.3.18, Ehrhard and Bucciarelli have developped a model of strongly stable functions, which we have described in section 13.3. But in the strongly stable model an explicit reference to a concept of sequentiality is lost at higher orders. Here there is an intrinsic difficulty: there does not exist a cartesian closed category of sequential (set theoretical) functions (see theorem 14.1.12). Berry suggested that replacing functions by morphisms of a more concrete nature, and retaining information on the order in which the input is explored in order to produce a given part of the output, could be a way to develop a theory of higher order sequentiality. This intuition gave birth to the model of sequential algorithms of Berry and Curien, which is described in this chapter [BC82, BC85].

In section 14.1, we introduce Kahn and Plotkin's (filiform and stable) concrete data structures and sequential functions between concrete data structures [KP93]. This definition generalizes Vuillemin's definition 6.5.1. A concrete data structure consists of cells that can be filled with a value, much like a PASCAL record field can be given a value. A concrete data structure generates a cpo of states, which are sets of pairs (cell, value), also called events (cf. section 12.3).

This chapter presents general techniques for the solution of domain equations and the representation of domains and functors over a universal domain. Given a category of domains C we build the related category Cip (cf. chapter 3) that has the same objects as C and injection-projection pairs as morphisms (section 7.1). It turns out that this is a suitable framework for the solution of domain equations. The technique is applied in section 7.2 in order to solve a predicate equation. In turn, the solution of the predicate equation is used in proving an adequacy theorem for a simple declarative language with dynamic binding.

The category of injection-projection pairs is also a suitable framework for the construction of a universal homogeneous object (section 7.3). The latter is a domain in which every other domain (not exceeding a certain size) can be embedded. Once a universal object U is built, it is possible to represent the collection of domains as the domain FP(U) of finitary projections over U, and functors as continuous functions over FP(U). In this way, one obtains a rather handy poset theoretical framework for the solution of domain equations (section 7.4). If, moreover, FP(U) is itself (the image of a) projection, then projections can be used to give a model of second order typed λ-calculus (see exercise 7.4.8 and section 11.3).

A third approach to the solution of domain equations consists in working with concrete representations of domains like information systems, event structures, or concrete data structures (introduced in definitions 10.2.11, 12.3.3 and 14.1.1, respectively).

The main goal of this chapter is to introduce λ-calculi with dependent and second order types, to discuss their interpretation in the framework of traditional domain theory (chapter 15 will mention another approach based on realizability), and to present some of their relevant syntactic properties.

Calculi with dependent and second order types are rather complex syntactic objects. In order to master some of their complexity let us start with a discussion from a semantic viewpoint. Let T be a category whose objects are regarded as types. The category T contains atomic types like the singleton type 1, the type nat representing natural numbers, and the type bool representing boolean values. The collection T is also closed with respect to certain data type constructions. For example, if A and B are types then we can form new types such as a product type A × B, a sum type A + B, and an exponent type A → B.

In first approximation, a dependent type is a family of types indexed over another type A. We represent such a family as a transformation F from A into the collection of types T, say F : A → T. As an example of dependent type we can think of a family Prod. bool: nat → T that given a number n returns the type bool × … × bool (n times).

This chapter introduces the untyped λ-calculus. We establish some of its fundamental theorems, among which we count the syntactic continuity theorem, which offers another indication of the relevance of Scott continuity (cf. section 1.1 and theorem 1.3.1).

The λ-calculus was introduced around 1930 by Church as part of an investigation in the formal foundations of mathematics and logic [Chu41]. The related formalism of combinatory logic had been introduced some years ealier by Schönfinkel and Curry. While the foundational program was later relativized by such results as Gödel's incompleteness theorem, λ-calculus nevertheless provided one of the concurrent formalizations of partial recursive functions. Logical interest in λ-calculus was resumed by Girard's discovery of the second order λ-calculus in the early seventies (see chapter 11).

In computer science, the interest in λ-calculus goes back to Landin [Lan66] and Reynolds [Rey70]. The λ-notation is also important in LISP, designed around 1960 by MacCarthy [Mac60]. These pioneering works have eventually led to the development of functional programming languages like Scheme or ML. In parallel, Scott and Strachey used λ-calculus as a meta-language for the description of the denotational semantics of programming languages. The most comprehensive reference on λ-calculus is [Bar84]. A more introductory textbook is [HS86]. We refer to these books for more historical pointers.

In section 2.1, we present the untyped λ-calculus. The motivation to prove a strong normalization theorem leads us to the simply typed λ-calculus.

When considering the λ-calculus as the kernel of a programming language it is natural to concentrate on weak reduction strategies, that is, strategies where evaluation stops at λ-abstractions. In presenting the semantic counterpart of these calculi it is useful to emphasize the distinction between value and computation. A first example coming from recursion theory relies on the notions of total and partial morphism. In our jargon a total morphism when given a value always returns a value whereas a partial morphism when given a value returns a possibly infinite computation. This example suggests that the denotation of a partial recursive algorithm is a morphism from values to computations, and that values are particular kinds of computations.

In domain theory the divergent computation is represented by a bottom element, say ⊥, that we add to the collection of values. This can be seen as the motivation for the shift from sets to flat domains. More precisely, we have considered three categories (cf. definition 1.4.17).

• The category Dcpo in which morphisms send values to values, say D → E. This category is adapted to a framework where every computation terminates.

• The category pDcpo which is equivalent to the one of cpo's and strict functions, and in which morphisms send values to computations, say D → (E)⊥. This category naturally models call-by-value evaluation where functions' arguments are evaluated before application.

• […]

In chapter 4, we have provided semantics for both typed and untyped λ-calculus. In this chapter we extend the approach to typed λ-calculus with fixpoints (λY-calculus), we suggest formal ways of reasoning with fixpoints, and we introduce a core functional language called PCF [Sco93, Plo77]. PCF has served as a basis for a large body of theoretical work in denotational semantics. We prove the adequacy of the interpretation with respect to the operational semantics, and we discuss the full abstraction problem, which has triggered a lot of research, both in syntax and semantics.

In section 6.1, we introduce the notion of cpo-enriched CCC's, which serves to interpret the λY-calculus. In section 6.2, we introduce fixpoint induction and show an application of this reasoning principle. In section 6.3, we introduce the language PCF, define its standard denotational semantics and its operational semantics, and we show a computational adequacy property: the meaning of a closed term of basic type is different from ⊥ if and only if its evaluation terminates. In section 6.4, we address a tighter correspondence between denotational and operational semantics, known as the full abstraction property. In section 6.5, we introduce Vuillemin's sequential functions, which capture first order PCF definability. In section 6.6, we show how a fully abstract model of PCF can be obtained by means of a suitable quotient of an (infinite) term model of PCF.

As the computation of a program proceeds, some (partial) information is read from the input, and portions of the output are gradually produced. This is true of mathematical reasoning too. Consider the following abstraction of a typical highschool problem for simple equation solving. The student is presented with three numerical figures – the data of the problem (which might themselves be obtained as the results of previous problems). Call them u, v, and w. The problem has two parts. In part 1, the student is required to compute a quantity x, and in the second part, using part 1 as a stepping stone, he (or she) is required to compute a quantity y. After some reasoning, the student will have found that, say, x = 3u + 4, and that y = x – v. Abstracting away from the actual values of u, v, w, x, and y, we can describe the problem in terms of information processing. We consider that the problem consists in computing x and y as a function of u, v, w, i.e., (x, y) = f(u, v, w). A first remark is that w is not used. In particular, if computing w was itself the result of a long, or even diverging, computation, the student would still be able to solve his problem. A second remark is that x depends on u only. Hence, again, if finding v is very painful, the student may still achieve at least part 1 of his problem.

In this chapter we address the fundamental domain equation D = D → D which serves to define models of the untyped λ-calculus. By ‘equation’, we actually mean that we seek a D together with an order-isomorphism D ≅ D → D. Taking D = {⊥} certainly yields a solution, since there is exactly one function f: {⊥} → {⊥}. But we are interested in a non-trivial solution, that is a D of cardinality at least 2, so that not all λ-terms will be identified! Domain equations will be treated in a general setting in chapter 7.

In section 3.1, we construct Scott's D∞ models as order theoretical limit constructions. In section 3.2, we first define a general notion of λ-model, and then discuss some specific properties of the D∞ models: Curry's fixpoint combinator is interpreted as the least fixpoint operator, and the theory induced by a D∞ model can be characterized syntactically, using Böhm trees. In section 3.3, we present a class of λ-models based on the idea that the meaning of a term should be the collection of properties it satisfies in a suitable ‘logic’. This point of view will be developed in more generality in chapter 10. In section 3.4, we relate the constructions of sections 3.1 and 3.3, following [CDHL82]. Finally, in section 3.5, we use intersection types as a tool for the syntactic theory of the λ-calculus [Kri91, RdR93].

The functional view of computation finds perhaps its most serious limitation in the analysis of concurrent systems (cf. chapter 9). The challenge is then to cope with the problems offered by concurrent systems while retaining some of the mathematically brilliant ideas and techniques developed in the pure functional setting.

In this chapter we introduce a simple extension of CCS known as π-calculus. The π-calculus is a rather minimal calculus whose initial purpose was to represent the notion of name or reference in a concurrent computing setting. It turns out that the π-calculus allows us for simple encodings of various functional and concurrent models. It can then be used as a privileged tool to understand in which sense functional computation can be embedded in a concurrent model.

Section 16.1 is dedicated to the introduction of some basic theory of the π-calculus. In section 16.2, we illustrate the expressive power of the π-calculus by encoding into it a concurrent functional language, called λ∥-calculus, that can be regarded as the kernel of concurrent extensions of the ML programming language such as LCS, CML and Facile where an integration of functional and concurrent programming is attempted. In section 16.3, we study the adequacy of the encoding of the λ∥-calculus in the π-calculus.

This chapter presents an operational phenomenon but fails to give a denotational account of it. As this book goes to press, there have been a few attempts in this direction [FMS96, Sta96].

The theory of stable functions is originally due to Berry [Ber78]. It has been rediscovered by Girard [Gir86] as a semantic counterpart of his theory of dilators. Similar ideas were also developed independently and with purely mathematical motivations by Diers (see [Tay90a] for references).

Berry discovered stability in his study of sequential computation (cf. theorem 2.4) and of the full abstraction problem for PCF (cf. section 6.4). His intuitions are drawn from an operational perspective, where one is concerned, not only with the input-output behaviour of procedures, but also with questions such as: ‘which amount of the input is actually explored by the procedure before it produces an output’. In Girard's work, stable functions arose in a construction of a model of system F (see chapter 11); soon after, his work on stability paved the way to linear logic, which is the subject of chapter 13.

In section 12.1, we introduce the conditionally multiplicative functions, which are the continuous functions preserving binary compatible glb's. In section 12.2, we introduce the stable functions, focusing on minimal points and traces. Stability and conditional multiplicativity are different in general, but are equivalent under a well-foundedness assumption. They both lead to cartesian closed categories. The ordering on function spaces is not the pointwise ordering, but a new ordering, called the stable ordering.

We next develop the theory on algebraic cpo's, as in chapter 5. In Section 12.3, we introduce Berry's dI-domains, which are Scott domains satisfying two additional axioms.

The remaining four chapters describe general techniques for designing functional data structures. We begin in this chapter with lazy rebuilding, a variant of global rebuilding [Ove83].

Batched Rebuilding

Many data structures obey balance invariants that guarantee efficient access. The canonical example is balanced binary search trees, which improve the worst-case running times of many tree operations from the O(n) required by unbalanced trees to O(log n). One approach to maintaining a balance invariant is to rebalance the structure after every update. For most balanced structures, there is a notion of perfect balance, which is a configuration that minimizes the cost of subsequent operations. However, since it is usually too expensive to restore perfect balance after every update, most implementations settle for approximations of perfect balance that are at most a constant factor slower. Examples of this approach include AVL trees [AVL62] and red-black trees [GS78].

However, provided no update disturbs the balance too drastically, an attractive alternative is to postpone rebalancing until after a sequence of updates, and then to rebalance the entire structure, restoring it to perfect balance. We call this approach batched rebuilding. Batched rebuilding yields good amortized time bounds provided that (1) the data structure is not rebuilt too often, and (2) individual updates do not excessively degrade the performance of later operations.

When a C programmer needs an efficient data structure for a particular problem, he or she can often simply look one up in any of a number of good textbooks or handbooks. Unfortunately, programmers in functional languages such as Standard ML or Haskell do not have this luxury. Although most of these books purport to be language-independent, they are unfortunately language-independent only in the sense of Henry Ford: Programmers can use any language they want, as long as it's imperative. To rectify this imbalance, this book describes data structures from a functional point of view. We use Standard ML for all our examples, but the programs are easily translated into other functional languages such as Haskell or Lisp. We include Haskell versions of our programs in Appendix A.

Functional vs. Imperative Data Structures

The methodological benefits of functional languages are well known [Bac78, Hug89, HJ94], but still the vast majority of programs are written in imperative languages such as C. This apparent contradiction is easily explained by the fact that functional languages have historically been slower than their more traditional cousins, but this gap is narrowing. Impressive advances have been made across a wide front, from basic compiler technology to sophisticated analyses and optimizations.

The term bootstrapping refers to “pulling yourself up by your bootstraps”. This seemingly nonsensical image is representative of a common situation in computer science: problems whose solutions require solutions to (simpler) instances of the same problem.

For example, consider loading an operating system from disk or tape onto a bare computer. Without an operating system, the computer cannot even read from the disk or tape! One solution is a bootstrap loader, a very tiny, incomplete operating system whose only purpose is to read in and pass control to a somewhat larger, more capable operating system that in turn reads in and passes control to the actual, desired operating system. This can be viewed as a instance of bootstrapping a complete solution from an incomplete solution.

Another example is bootstrapping a compiler. A common activity is to write the compiler for a new language in the language itself. But then how do you compile that compiler? One solution is to write a very simple, inefficient interpreter for the language in some other, existing language. Then, using the interpreter, you can execute the compiler on itself, thereby obtaining an efficient, compiled executable for the compiler. This can be viewed as an instance of bootstrapping an efficient solution from an inefficient solution.

Over the past fifteen years, amortization has become a powerful tool in the design and analysis of data structures. Implementations with good amortized bounds are often simpler and faster than implementations with comparable worst-case bounds. In this chapter, we review the basic techniques of amortization and illustrate these ideas with a simple implementation of FIFO queues and several implementations of heaps.

Unfortunately, the simple view of amortization presented in this chapter breaks in the presence of persistence―these data structures may be extremely inefficient when used persistently. In practice, however, many applications do not require persistence, and for those applications, the implementations presented in this chapter are excellent choices. In the next chapter, we will see how to reconcile the notions of amortization and persistence using lazy evaluation.

Techniques of Amortized Analysis

The notion of amortization arises from the following observation. Given a sequence of operations, we may wish to know the running time of the entire sequence, but not care about the running time of any individual operation. For instance, given a sequence of n operations, we may wish to bound the total running time of the sequence by O(n) without insisting that every individual operation run in O(1) time. We might be satisfied if a few operations run in O(log n) or even O(n) time, provided the total cost of the sequence is only O(n).

A distinctive property of functional data structures is that they are always persistent―updating a functional data structure does not destroy the existing version, but rather creates a new version that coexists with the old one. Persistence is achieved by copying the affected nodes of a data structure and making all changes in the copy rather than in the original. Because nodes are never modified directly, all nodes that are unaffected by an update can be shared between the old and new versions of the data structure without worrying that a change in one version will inadvertently be visible to the other.

In this chapter, we examine the details of copying and sharing for two simple data structures: lists and binary search trees.

Lists

We begin with simple linked lists, which are common in imperative programming and ubiquitous in functional programming. The core functions supported by lists are essentially those of the stack abstraction, which is described as a Standard ML signature in Figure 2.1. Lists and stacks can be implemented trivially using either the built-in type of lists (Figure 2.2) or a custom datatype (Figure 2.3).

Remark The signature in Figure 2.1 uses list nomenclature (cons, head, tail) rather than stack nomenclature (push, top, pop), because we regard stacks as an instance of the general class of sequences.