This chapter contains the second part of our presentation of set notation. It is devoted to the study of the construction of mathematical objects: that is, finite sets, natural numbers, finite sequences, and finite trees. All such constructions are realized by using the same inductive method based on the fixpoint theorem of Knaster and Tarski. We shall also describe the way recursive functions on these objects can be formally defined.

At the beginning of the chapter generalized intersection and union are presented, then we introduce the framework that we shall use in order to construct our objects. Then the construction of each of the mentioned objects follows in separate sections. Finally, at the end of the chapter, we present the concept of well-foundedness, which unifies completely each of the previous constructs.

Hurried readers, who are not interested in the details of these formal constructions, can skip them. They can go to Appendix A, where the notations are all listed.

Generalized Intersection and Union

Before presenting the framework that will allow us to construct mathematical objects in a systematic manner (section 3.2), we need first to introduce two important set theoretic concepts called generalized intersection and generalized union.

As usual, we first introduce our concepts syntactically, then we give an informal explanation and some examples, and finally we state and prove their basic properties. We now present the syntax of the new constructs.

The main objective of this chapter, and of the next one, is to make precise part of the notation that we intend to use in order to specify and design software systems. As a matter of fact, this notation is nothing but the one used, more or less formally, by every scientist: that of set theory.

Clearly, in order to perform our subsequent formal developments, we could have stayed within some extensions of the logic introduced in the previous chapter. For the following three reasons it is my view that set theory is a better choice.

First, when using set theory, one remains within first order logic while it is clearly possible to manipulate objects of “high order” such as sets and relations of any depth (that is, sets and relations built themselves on sets and relations, and so on). In any case, such constructs are objects (not predicates) and are thus licit candidates for first order quantifications.

Second, and more importantly, the use of set theory allows one, very often, to eliminate quantifiers. In fact, most of the set-theoretic concepts are introduced precisely because they hide some quantifications. Typical examples are: set inclusion, relational composition, and generalized intersection or union of sets of sets.

Third, set theory has the (apparently innocent but, in fact, very important) property of handling negation in a very controlled way: it is simply because the complement of a set is still a set. That is, negation does not extend beyond certain limits.

This book is much more than a new programming manual. It introduces a method in which the program design is included in the global process that goes from understanding the problem to the validation of its solution.

The mathematical basis of the method provides the exactness while the proposed notation eliminates the ambiguities of the vernacular language. At the same time, the process is simple enough for an industrial use “Industrial” is in fact the key word.

The general aim of formal methods is to provide correctness of the problem specification. Here we can see how the solution can be found, step by step, by a continuously monitored process. The mathematical verification of each step is so closely bound to the refinement activity that it is no longer possible to separate the design choices from the checking process. Imagination is helped by exactness!

But how about the efficiency? Isn't the design too long? Are the design people able to do this work? Are the machines powerful enough to implement the method? The answers are easy to give. Let me tell you.

My company has been involved, since the sixties, in the realisation of train control systems, which must meet stringent safety requirements. As soon as we began to use programmed logic (end of the seventies) we had to solve the problem of software correctness. Together with other methods, we chose to use the program proving method proposed by C.A.R. Hoare. In 1986, J.-R. Abrial introduced us to the B method. We decided to learn it and to use it. The tools did not exist at the time.

Categorical structures suitable for describing partial maps, viz. domain structures, are introduced and their induced categories of partial maps are defined.

The representation of partial maps as total ones is addressed. In particular, the representability (in the categorical sense) and the classifiability (in the sense of topos theory) of partial maps are shown to be equivalent (Theorem 3.2.6).

Finally, two notions of approximation, contextual approximation and specialisation, based on testing and observing partial maps are considered and shown to coincide. It is observed that the approximation of partial maps is definable from testing for totality and the approximation of total maps; providing evidence for taking the approximation of total maps as primitive.

Categories of Partial Maps

To motivate the definition of a partial map, observe that a partial function u : A ⇀ B is determined by its domain of definition dom(u) ⊆ A and the total function dom(u) → B induced by the mapping a ↦ u(a). Thus, every partial function A ⇀ B can be described by a pair consisting of an injection D ↣ A and a total function D → B with the same source.

In this chapter we study the categorical constructions for interpreting data types. We start by observing that the notion of pairing in a category of partial maps (with a minimum of structure) cannot be the categorical product. The appropriate interpretation for product types (partial products) is the categorical product in the category of total maps endowed with a pairing operation on partial maps extending the pairing of total maps. Once the notion of product is established, partial exponentials are defined as usual, and some properties of Poset-partial-exponentials are presented. Next colimits are studied. The situation is completely different from that of limits. For example, an object is initial in the category of total maps if and only if it is so in the category of partial maps. A characterisation of certain colimits (including coproducts) in a category of partial maps, due to Gordon Plotkin, is given. We further relate colimits in the category of total maps and colimits in the category of partial maps by means of the lifting functor. Finally, we provide conditions on a Cpo-category of partial maps under which ω-chains of embeddings have colimits. This is done in the presence of the lifting functor, and for arbitrary categories of partial maps.

Partial Binary Products

The data type for pairing in pΚ cannot be the categorical product because, under reasonable assumptions, this would lead to inconsistency.

We have initiated an abstract approach to domain theory as needed for the denotational semantics of deterministic programming languages. To provide an explicit semantic treatment of non-termination, we decided to make partiality the core of our theory. Thus, we focussed on categories of partial maps. We have studied the representability of partial maps and shown its equivalence with classifiability. We have observed that, once partiality is taken as primitive, a notion of approximation may be derived. In fact, two notions of approximations based on testing and observing partial maps have been considered and shown to coincide. Further we have characterised when the approximation relation between partial maps is domain-theoretic in the (technical) sense that the category of partial maps Cpo-enriches with respect to it.

Concerning the semantics of type constructors in categories of partial maps we have: presented a characterisation of colimits of diagrams of total maps due to Gordon Plotkin; studied order-enriched partial cartesian closure; and provided conditions to guarantee the existence of the limits needed to solve recursive type equations. Concerning the semantics of recursive types we have: made Peter Freyd's notion of algebraic compactness the central concept; motivated the compactness axiom; established the fundamental property of parameterised algebraically compact categories (slightly extending a previous result of Peter Freyd); and shown that in algebraically compact categories recursive types reduce to inductive types. Special attention has been paid to Cpo-algebraic compactness, leading to the identification of a 2-category of kinds with very strong closure properties.

We thoroughly study the semantics of inductive and recursive types. Our point of view is that types constitute the objects of a category and that type constructors are bifunctors on the category of types. By a bifunctor on a category we mean a functor on two variables from the category to itself, contravariant in the first, covariant in the second.

First, following Peter Freyd, the stress is on the study of algebraically complete categories, i.e. those categories admitting all inductive types (in the sense that every endofunctor on them has an initial algebra—this is understood in a setting in which the phrase “every endofunctor” refers to a class of enriched endofunctors—see Definition 6.1.4). After observing that algebraic completeness guarantees the existence of parameterised initial algebras, we identify, under the name of parameterised algebraically complete categories, all those categories which are algebraically complete and such that every parameterised inductive type constructor gives rise to a parameterised inductive type (see Definition 6.1.7). Type constructors on several variables are dealt with by Bekič's Lemma, from which follow both the Product Theorem for Parameterised Algebraically Complete Categories (Theorem 6.1.14) and also the dinaturality of Fix (the functor delivering initial algebras).

Second, again following Peter Freyd, algebraic completeness is refined to algebraic compactness by imposing the axiom that, for every endofunctor, the inverse of an initial algebra is a final coalgebra. The compactness axiom is motivated with a simple argument showing that every bifunctor on an algebraically compact category admits a fixed-point.