An Algebraic Construction of Predicate Transformers

Paul Gardiner 1, Clare Martin 2 and Oege de Moor 1

1 Oxford University Computing Laboratory, Programming Research Group, Keble Road,

Oxford OX1 3QD, UK 2 University of Buckingham, Buckingham MK18 1EG, UK

Abstract. In this paper we present an algebraic construction of monotonic predicate transformers, using a categorical construction which is similar to the algebraic construction of the integers from the natural numbers. When applied to the category of sets and total functions once, it yields a category isomorphic to the category of sets and relations; a second application yields a category isomorphic to the category of monotonic predicate transformers. This hierarchy cannot be extended further: the category of total functions is not itself an instance of the categorical construction, and can only be extended by it twice.

1 Introduction

Predicate transformers were introduced originally by Dijkstra [8] in order to provide an elegant semantics for his programming language. Their strength lies in the fact that they can be used to model non-deterministic and non-terminating behaviour in terms of total functions, rather than relations. Not all monotonic predicate transformers represent programs in Dijkstra’s language, but the language has various extensions such as the refinement calculus [26, 1, 28] in which they do all represent either programs or specifications. Indeed, monotonic predicate transformers provide a uniform framework for the specification and derivation of non-deterministic programs, in the same way that relations do for the specification and derivation of efficient functional programs [4]. In this paper we explore the mathematical properties underlying this similarity.

As motivation, the paper begins with a discussion of some algebraic properties which are common to the categories of relations and predicate transformers. Then the categorical construction which unifies the two categories is introduced. It is a slight variation of the standard construction of the category of spans [22], where a span is simply a pair of arrows with joint source. The category of relations can be constructed by forming the class of spans of all total functions, and identifying those which are equivalent with respect to an appropriate equivalence relation. So the construction is similar to the standard algebraic construction of the integers as a set of equivalence classes of pairs of natural numbers. The advantage of using categories instead of sets is that it is not necessary to provide an additional definition of the associated ordering and composition: both are incorporated into the definition of the span category. We call the new construction which unifies the categories of relations and predicate transformers a skew span category. It differs from the standard construction by taking into consideration an ordering relation associated with the category from which it is constructed. When applied to the category of sets and total functions once, it yields a category isomorphic to the category of sets and relations; a second application yields a category isomorphic to the category of monotonic predicate transformers.

The view of predicate transformers taken in this paper has some potential applications to programming and specification languages which have not yet been fully explored. At present, languages for program derivation such as the refinement calculus are untyped. The skew span construction of relations and predicate transformers provides a mechanism whereby certain aspects of the rich type structure of the category of total functions can be promoted to predicate transformers. In particular, the promotion of functors and adjunctions to lax functors and local adjunctions in span categories respectively [17] is still valid for skew span categories. Furthermore, recent research [25] has shown that data types defined by initial algebras in the category of total functions are transformed to final coalgebras under the embedding into the category of monotonic predicate transformers. Such results could prove useful for the future incorporation of types into the refinement calculus, and will be discussed in Sect. 5. The application on which we will focus at the end of this paper was suggested by Hoare [16], who has interpreted the findings in the context of specifications involving Hoare logic. When translated to the refinement calculus this provides new single complete rules for refinement and composition.

An application which will not be discussed in this paper concerns a recent result on the completeness of data refinement. In [11], it is shown that one of the reasons why monotonic predicate transformers provide a logical setting for the derivation of non-deterministic programs is that there is a single complete rule for data refinement. The same is true of the relational setting for the derivation of functional programs. A unified proof of both these observations is given in [9], where the specific results of [11] are generalized to arbitrary skew span categories.

This paper is organised as follows. In Sect. 2 we discuss the factorization properties of relations and predicate transformers which facilitate their skew span representation. The properties are described in the broader context of order enriched categories. In Sect. 3 we introduce skew span categories, and in Sect. 4 we show how such categories may be identified by their factorization properties. In Sect. 5 we briefly discuss the relevance of this work to the future development of a typed version of the refinement calculus, and in Sect. 6 we show how it provides the existing calculus with two extra proof rules.

2 Order Enriched Categories

We assume familiarity with the basic definitions of category theory, but will begin by summarizing some other standard definitions. We use the notation (p;q) to denote the composite of each pair of arrows p : A → B, q : B → C. Functional composition is denoted by juxtaposition, and associates to the right.

A preorder (P, ⊑) is a special case of a category: its objects are the members of a set P, and arrows are exactly the pairs (p, q) for which p ⊑ q, where ⊑ is a reflexive and transitive relation. There is an equivalence relation (≡) associated with every preorder which is defined by:

p ≡ q ⇔ (p ⊑ q and q ⊑ p) .

Any equivalence relation on a set X gives rise to a partition of X into disjoint equivalence classes of the form (|a|) = {x ∈ X|x ≡ a}. The set of all equivalence classes of (P, ⊑) under the equivalence relation associated with ⊑ forms a partial order ((|P |), ≤); a partial order (or poset) is a preorder which is anti-symmetric. The partial order ≤ on (|P |) is defined by

(|p|) ≤ (|q|) ⇔ p ⊑ q .

A preorder enriched category (C, ⊑) is a category C with a preorder ⊑ defined on homsets, with respect to which the categorical composition ; is monotonic:

(p ⊑ q and r ⊑ s) ⇒ p;r ⊑ q;s

for all p, q : A → B and r, s : B → C. Poset enriched categories are defined in the same way, except that instead of a preorder, each homset is a poset. Both these kinds of order enriched category can be thought of as a ‘2-dimensional’ category: the arrows of C represent the horizontal dimension and the those of the order relation the vertical dimension. This property is formalized by the notion of a 2-category [12], of which preorder enriched categories are a special case. Functors between such categories must preserve both the horizontal and vertical structure, which in this case means that functors must be monotonic. Therefore when we refer to a functor between order enriched categories, we will always mean a monotonic functor.

As most of the following examples illustrate, order enriched categories are well suited for modelling programming languages with types and scopes. The object structure matches the type structure of strictly typed programming languages, and composition represents sequential execution. Furthermore, the refinement relation on programs imposes a preorder enriched structure on such categories. One program p is refined by another q if for any purpose whatsoever and in any context of use q will perform at least as well, and perhaps better than p. The associated relation is clearly reflexive, and it is transitive since if the behaviour of the program p is in all respects as good as that of the program q which in turn is as good as r, then p too is as good as r.

Examples 1.

1. (M, ≤) a commutative monoid. A monoid is a triple ⟨M, ⊕, e⟩ where M is a set, and ⊕ is an associative binary operator ⊕ : M × M → M with identity e. A commutative monoid is a monoid where the operator ⊕ is also commutative. A monoid determines a category with one object, usually denoted ∗. The arrows of the category are the elements of M, with ∗ as source and target; composition is the binary operator ⊕. Since this category has only one object it has just one homset; the preorder is defined for all m, n ∈ M by

m ≤ n ⇔ (∃k ∈ M • m ⊕ k = n) .

The operator ⊕ is monotonic in both arguments with respect to this ordering, so (M, ≤) is a preorder enriched category.

2. (Set,=), the category of total functions whose class of objects is the class of all sets; whose homsets Set(A, B) are the sets of total functions from A to B; and whose composition is the usual composition of functions. Two total functions from A to B are comparable if and only if they are equal, so the partial order on each homset is the trivial equality relation. This category can be used to model typed functional programming languages in which all programs are terminating and deterministic. One such program refines another only if they compute the same function, so the refinement ordering is correctly represented by equality.

3. (Rel, ⊆), the category of relations whose class of objects is the class of all sets; whose homsets Rel(A, B) are the sets of subsets of A × B regarded as relations from A to B; and whose composition is the usual composition of relations. Subset inclusion is a reflexive, transitive and anti-symmetric relation, so each homset (Rel(A, B), ⊆) is a partial order. Relational composition is monotonic with respect to subset inclusion, so (Rel,⊆) is a poset enriched category. This category is the natural setting in which to embed models of imperative programming languages which exhibit (angelic) non-determinism. Programs are represented by relations, and sequential composition by relational composition.

4. (Pow, ⊑), the category of monotonic predicate transformers whose class of objects is the class of all powersets; whose homsets Pow(IPA, IPB) are the sets of total monotonic functions from IPA to IPB; and whose composition is the usual composition of functions. The subset inclusion relation determines a partial order on each object of this category, which is promoted to the pointwise order on arrows: if p, q : IPA → IPB, then

p ⊑ q ⇔ (p X ⊆ q X for all X ⊆ A) .

The resulting partial order on each homset (Pow(IPA, IPB), ⊑) is preserved by functional composition since all the functions are monotonic, so (Pow,⊑) is a poset enriched category. The name of this category derives from the fact that each arrow in Pow is equivalent to a total function from predicates to predicates, usually called a predicate transformer [8]. For if PA denotes the set of predicates of classical logic with free variables drawn from the set A, then the poset (PA, ⇒) can be identified with (IPA, ⊆) by interpreting each predicate in PA as the set of values in A satisfying it. This category can be used to model specification formalisms like the refinement calculus.

Future references to order enriched categories will not necessarily include the associated order relations. So for example, (Rel, ⊆) will be referred to as Rel.

Maps

Order enriched categories can accommodate a far greater range of constructs than ordinary categories, since all the standard categorical definitions can be weakened by substituting inequalities for equalities. An example of such a definition is that of a map [7] which is a weak analogue of the standard concept of an isomorphism. It is introduced here in order to define the factorization property shared by relations and predicate transformers.

An arrow p : A → B of a preorder enriched category (C, ⊑) is called a map if there exists another arrow p^{∗} : B → A such that

I_{A} ⊑ p;p^{∗}  (1)
p^{∗};p ⊑ I_{B} .  (2)

In the trivial case that the preorder ⊑ is the equality relation, this definition coincides with the definition of isomorphism, and in the same way that isomorphisms are preserved by functors, maps are preserved by monotonic functors. Clearly all identities are maps, and the composites of maps are maps, so the maps form a preorder enriched subcategory of C, which is usually denoted by Map(C). An arrow p^{∗} that satisfies the conditions of the above definition will be referred to here as a comap. Each map p determines up to equivalence its comap p^{∗}, in the sense that if there exists another arrow q : B → A which can be substituted for p^{∗} in (1) and (2), then p ≡ q. This is immediate from the following property of maps: let p : C → D, q : A → B be maps in C, then for all r : A → C, s : B → D in C

r;p ⊑ q;s ⇔ q^{∗};r ⊑ s;p^{∗} .  (3)

The subcategory of maps in the first two categories of Examples 1 simply consist of the isomorphisms; the last two provide more interesting examples.

Examples 2.

1. Map(Rel) = Set The relational converse of a relation r is denoted by r^{∘}. All total functions f : A → B in Rel are maps, since

I_{A} ⊆ f; f^{∘} total
f^{∘}; f ⊆ I_{B} functional .

Conversely, any relation which satisfies the first map axiom (1) must be total, and if it also satisfies (2) it must be functional.

2. Map(Pow) ≅ Rel A well-known property of monotonic functions between complete lattices [18] implies that an arrow p : IPA → IPB in Pow is a map if and only if it preserves arbitrary unions, which is to say that for all S ⊆ IPA,

p(∪S) = ∪{p X | X ∈ S} .  (4)

It is easy to check that all maps in Pow have this property, and conversely any p satisfying (4) has a comap p^{∗} defined for all Y ∈ IPB by

p^{∗} Y ˆ= ∪{X ∈ IPA | p X ⊆ Y } .

There is an isomorphism between Rel and the subcategory of Pow containing all functions which preserve arbitrary unions, which is defined by the existential image functor ⟨ ⟩ : Rel → Map(Pow) where for all r : A → B in Rel and X ∈ IPA

\begin{matrix}⟨A⟩ & ˆ= & IPA \\ ⟨r⟩X & ˆ= & \{b ∈ B | ∃a ∈ X • a(r)b\} . \end{matrix}

The comap of the map ⟨r⟩ corresponding to each relation r is called the universal image of r, and will be written here as [r].

Map Factorization

We will now introduce a factorization property associated with maps and comaps which resembles the standard concept of epi/monic factorization. Although neither of the categories Rel and Pow has epi/monic factorization, both have the factorization property introduced in this section.

Let (C, ⊑) be a preorder enriched category. We say that C has map factorization if every arrow p : A → B has a factorization

A \overline{}^{p} B = A \overline{}^{n^{∗}} E \overline{}^{m} B

where n^{∗} is a comap and m is a map.

Examples 3.

1. Rel has map factorization. For let r : A → B be a relation, and let R denote that subset of the cartesian product A × B determined by r. The associated projections are given by:

\begin{matrix}π : R → A & and & μ : R → B \\ π(a, b) = a & & μ(a, b) = b & . \end{matrix}

Since both projections are total functions, we have the map factorization

r = π^{∘};μ.

2. Pow has map factorization: one such factorization is constructed using the union function ∪_{A} : IPIPA → IPA which sends each subset of IPA to its union, together with the powerset function IP_{A} : IPA → IPIPA that sends each set in IPA to the set of its subsets. Let p : IPA → IPB be an arrow in Pow. The effect of applying p to some subset X of A is equivalent to mapping X to its powerset IPX, applying p to each element of the powerset, and taking the union of the resulting set of sets. So the map factorization of p is given by

p = IP_{A};⟨p⟩;∪_{B}

where ⟨ ⟩ is the existential image functor introduced in Examples 2. In Sect. 5, we will use the following version of this factorization, which is expressed in terms of the epsiloff [10] relation ∋_{A}: IPA → A, the converse of the membership relation:

IPA \overline{}^{p} IPB = IPA [∋_{A}] ; \overline{}IPIPA⟨p;∋_{B}⟩ ; \overline{}IPB

where [ ] is the universal image functor introduced in Examples 2. This example also appears in [14].

Uniqueness of Factorization

The map factorization in Rel and Pow has a uniqueness property which is similar to that normally associated with epi/monic factorization [13].

Let (C, ⊑) be a preorder enriched category with map factorization. We will say that the map factorization in C is unique up to equivalence if for all comap/map pairs (n^{∗} : N → E, m : E → M) and (n^{′∗} : N → E′, m′ : E′ → M),

n^{∗};m ⊑ n^{′∗};m′ ⇔ ∃h ∈ Map(C) • (h;n′ ⊑ n and m ⊑ h;m′) .  (5)

If the preorder ⊑ is a partial order we will simply refer to this property as unique map factorization. The following lemma gives a restatement of the above definition which is useful for validating concrete examples.

Lemma 1. If a preorder enriched category (C, ⊑) has map factorization, then the factorization is unique up to equivalence if and only if whenever m : A → C and m′ : B → C are maps in C, then for all r : A → B

m ⊑ r;m′ ⇒ ∃k ∈ Map(C) • (k ⊑ r and m ⊑ k;m′) .  (6)

Proof. First suppose that (C, ⊑) is a preorder enriched category with unique map factorization. Let m : A → C, m′ : B → C ∈ Map(C), and suppose that m ⊑ r;m′ for some r : A → B ∈ C. Let p^{∗};q be a map factorization of r, so

m ⊑ p^{∗};q;m′ .

By (5) and (3) there exists a map h such that

h ⊑ p^{∗} and m ⊑ h;q;m′ .

So k = h;q is a map which establishes (6).

Conversely, suppose that (6) is satisfied. Let (n^{∗} : N → E, m : E → M) and (n^{′∗} : N → E′, m′ : E′ → M) be comap/map pairs which satisfy

n^{∗};m ⊑ n^{′∗};m′  ⇒ { (3) }
m ⊑ n;n^{′∗};m  ⇒ { (6) }
∃k ∈ Map(C) • (k ⊑ n;n^{′∗} and m ⊑ k;m′) ⇒ { (3) }
∃k ∈ Map(C) • (k;n′ ⊑ n and m ⊑ k;m′)

which establishes the uniqueness of factorization 5.

□

Examples 4.

1. Rel has unique map factorization. For suppose that m ⊆ r;m′ in Rel where m : A → C and m′ : B → C are maps and r : A → B. We require a map k such that

k ⊆ r and m ⊆ k;m′ .

Since k is a map in Rel it must be a total function. It is constructed as follows: let a ∈ A, and take c such that (a, c) ∈ m ⊆ r;m′. By definition of composition there exists b such that

(a, b) ∈ r and (b, c) ∈ m′ .

Defining k(a) = b establishes the result. Note that this construction of k requires the axiom of choice. Indeed, to say that Rel has unique map factorization is to assert the axiom of choice.

2. Pow has unique map factorization. For suppose that m ⊑ p;m′ in Pow, where m : IPA → IPC and m′ : IPB → IPC are maps and p : IPA → IPB. We require an arrow k : IPA → IPB which satisfies the conditions of Lemma 1. Let

k X = ∪{p{x}|x ∈ X} for all X ∈ IPA

then clearly k preserves arbitrary unions, so it is a map in Pow. Since p is monotonic, k ⊑ p. So it remains to check that m ⊑ k;m′. Let X ∈ IPA, then

m X  = { m ∈ Map(Pow) }
∪{m{x}|x ∈ X}  ⊆ { m ⊑ p;m′ }
∪{m′p{x}|x ∈ X} = { m′ ∈ Map(Pow) }
m′(∪{p{x}|x ∈ X}) = { definition of k }
m′kX

which establishes the result.

3 Skew Span Categories

We will now introduce the skew span category which will be shown to provide the uniform construction of the categories of relations and predicate transformers in Sect. 4.

There are two categorical techniques for constructing the category of relations from the category of total functions. One is known as the category of relations and the other is known as the locally posettal reflection of the category of spans [6]. Both of these constructions can only be carried out for categories with certain properties. The second construction is much simpler than the first one, to the point of being naive. It was this simplicity that first directed our attention to the categorical theory of relations [22]. Here we consider a generalization of that construction which can be applied to any preorder enriched category (C, ⊑) provided that C has an asymmetric kind of weak pullback. If the preorder ⊑ in C is the equality relation =, then the new construction is identical to that in [22].

Preordered Spans

Let (C, ⊑) be a preorder enriched category. A span in C is an ordered pair of arrows with a common source

(n : E → N, m : E → M) .

For example, let (IN, ≤_{IN}) be the preorder enriched category represented by the monoid of natural numbers under addition (IN, +, 0). Since all arrows in a monoid have the same source, a span is just a pair of natural numbers (n, m).

We define a preorder on spans similar to that associated with the uniqueness of map factorization; it is defined in terms of skew span morphisms. Let R = (n : E → N, m : E → M) and R′ = (n′ : E′ → N, m′ : E′ → M) be spans in C. We define a skew span morphism to be an arrow (h : E → E′) in C such that

m ⊑ h; m′ and h; n′ ⊑ n .  (7)

We will use the notation (h : R ⇒ R′) to denote a skew span morphism from R to R′. This definition is illustrated by the semi-commuting diagram below:

[figure: E; n; m; N; ⊒; h; ⊒; M; n′; m′; E′]

The direction of the inequalities in this definition is chosen to attune with the definition of unique map factorization, as is highlighted by Examples 5 (2) below. The standard definition of a span morphism, as used in [22, 6] is a special case of this one, in which the preorder ⊑ is the equality relation. The preorder on spans is given by: R ≤ R′ if and only if there is a skew span morphism from R to R′. We will write (|n, m|) for the class of spans that are equivalent to (n, m) with respect to this preorder. The preorder on spans gives rise to a partial order on equivalence classes of spans in the usual way.

Examples 5.

1. The category of natural numbers (IN, ≤_{IN}) provides a simple illustration of the skew span preorder. Using ordinary subtraction of integers, we have

(n, m) ≤ (n′, m′) ⇔ (m − n) ≤_{IN} (m′ − n′) .

In contrast, the preorder on pairs of natural numbers induced by standard span morphisms implies that the corresponding integers are equal.

2. Consider any poset enriched category (C, ⊑) with map factorization. To say that the map factorization in C is unique is the same as saying that for all spans (n : E → N, m : E → M), (n′ : E′ → N, m′ : E′ → M) in Map(C)

(n, m) ≤ (n′, m′) ⇔ n^{∗};m ⊑ n^{′∗};m′ .

Pullovers

One way that two spans (n : E → N, m : E → M) and (n′ : D → M, m′ : D → M′) can be combined into a single span is by taking the pullback of the inner pair of arrows (m : E → M, n′ : D → M). The pullback is the usual composition operator on spans [3], but it cannot be used here because it is not necessarily monotonic with respect to the preorder defined by skew span morphisms. Instead we introduce the notion of a pullover in a preorder enriched category, which is a weak analogue of a pullback. Its definition is related to that of subequalizers which were introduced by Lambek [19]. If subequalizers are substituted for equalizers in the construction of pullbacks from products and equalizers, then the result is nearly the same as a pullover.

Let (C, ⊑) be a preorder enriched category. We define the pullover of a pair of arrows m : E → M and n : D → M in C to be a span (r, q) such that for all spans

(r′, q′)
q′; n ⊑ r′; m ⇔ (r′, q′) ≤ (r, q) .  (8)

Diagramatically, a pullover is represented by

[figure: P′; h; ⊒; q′; r′; ⊒; P; q; D; r; ⊒; n; E; m; M]

Whereas pullbacks are defined up to isomorphism, pullovers are only determined up to equivalence of spans. The following lemma is similar to a result about pullbacks in [7], and provides a simple method for finding concrete examples of pullovers.

Lemma 2. Let (C, ⊑) be a category with unique map factorization. Then the semicommuting diagram

[figure: P; q; D; r; ⊒; n; E; m; M]

is a pullover diagram in Map(C) if and only if

r^{∗};q = m;n^{∗} .  (9)

Proof. Suppose that m, n, q, r satisfy (9) and that (r′ : P′ → E, q′ : P′ → D) is another span of maps, then

q′;n ⊑ r′;m ⇔ { (3) }
r^{′∗};q′ ⊑ m;n^{∗} ⇔ { (9) }
r^{′∗};q′ ⊑ r^{∗};q  ⇔ { Examples 5(2) }
(r′, q′) ≤ (r, q) .

Hence (r, q) is the pullover of (m, n). Since any two pullovers of the same pair of arrows are equivalent with respect to the skew span preorder, by Examples 5 (2) all pullovers of (m, n) must satisfy (9).

□

The first two of the following examples can be verified using this lemma.

Examples 6.

1. In (Set,=) the pullover coincides with the pullback:

PSet = { (x, y) | x ∈ E ∧ y ∈ D ∧ n y = m x } .

The span (r, q) is the pair of left and right projections

(π : PSet → E, μ : PSet → D) .

Pullovers in categories of the form (C, =) are not necessarily the same as pullbacks: the substitution of equality for the inequality ⊑ in the definition of the pullover yields only the definition of a weak pullback [22]. A weak pullback is like a pullback except that the universal arrow is not required to be unique.

2. Although pullbacks do not exist in Rel, it does have pullovers: one form of the pullover in Rel is given by

PRel = { (x, y) | x ∈ IPE ∧ y ∈ IPD ∧ ⟨n⟩ y ⊆ ⟨m⟩ x }.

Here the span (r, q) is the pair of projections

((π;∋) : PRel → E, (μ;∋) : PRel → D) .

3. Pullovers do not exist in Pow [21].

The skew span category Span(C)

Pullovers provide a monotonic composition operator on spans, which can now be used to define a category of spans.

Let (C, ⊑) be a preorder enriched category with pullovers. The skew span category (Span(C), ≤) is the category whose class of objects consists of all the objects in C, and whose homsets (Span(C))(N, M) consist of the equivalence classes of spans

(|n : E → N, m : E → M|)

for all such n, E, m in C. Composition in Span(C) is defined as follows: let

(|n, m|) : N → M and (|n′, m′|) : M → K

be arrows in Span(C). Their composition is

(|n, m|) ;(|n′, m′|) = (|r; n, q; m′|)  (10)

where (r, q) is a pullover of (m, n′). In a diagram:

[figure: P; r; q; E; ⊒; D; n; m; n′; m′; N; M; K]

Composition is associative and monotonic and (|I_{N}, I_{N} |) is the identity arrow associated with each object N. Since skew span morphisms define a partial order on objects in Span(C), the monotonicity of composition is sufficient to ensure that it is also well-defined. The ordering ≤ on homsets in Span(C) is the partial order on equivalence classes associated with the preorder defined by skew span morphisms.

4 Characterization Theorem

We will now show how skew span categories, like ordinary span categories can be characterized in terms of their factorization properties alone. It is then immediate that the categories of relations and monotonic predicate transformers are isomorphic to skew span categories.

It is well-known [6] that the span category of any suitable category C has map factorization, and that its subcategory of maps is isomorphic to C. We will begin by showing that the same is true of skew span categories. The functor which embeds a category into its span category is called the graph functor G : C → Span(C) where

\begin{matrix}GM & ˆ= & M \\ G(m : E → M) & ˆ= & (|I, m|) : E → M. \end{matrix}

The graph functor has the property that for all arrows m, m′ : E → M in (C, ⊑),

m ⊑ m′ ⇔ (Gm ≤ Gm′) .  (11)

This is indicative of the way that the skew span category is really a 2-categorical concept, since the graph functor preserves not only the arrows of C but also the corresponding order relation. It also shows that whenever the relation ⊑ is a partial order the graph functor is injective. For each arrow m : E → M in C, Gm is a map in Span(C): its comap is given by

(Gm)^{∗} = (|m, I|) : M → E .

Furthermore, every arrow (|n, m|) in Span(C) can be teased apart into the following map factorization:

(|n, m|) = (Gn)^{∗};Gm .  (12)

The following theorem shows that all maps in Span(C) can be expressed in the form Gm for some m ∈ C.

Theorem 3. Let (C, ⊑) be a poset enriched category with pullovers. Then

Map(Span(C)) ≅ C .

Proof. The isomorphism is defined by the functor which sends each arrow in C to its graph in Map(Span(C)). We have already seen from (11) that the functor is monotonic and injective, and it is clearly surjective on objects. Therefore it remains to show that every map in Span(C) can be written as the graph of an arrow in C. Let

p = (|n, m|) and p^{∗} = (|n′, m′|) .

be a map and comap in Span(C), and suppose that (q, r) is a pullover of (m, n′). By (1) together with the definition of span composition (10) and skew span morphism (7), there exists h ∈ C such that

I ⊑ h;q;m′  (13)
h;r;n ⊑ I .  (14)

We will now use mutual inclusion to show that p can be written in the form of a graph. Using these inequalities we can write p in the form of a graph. For it follows from (8) and (14) that

(h;r) : (I, h;q;n′) ⇒ (n, m) .

Therefore

G(h;q;n′) ≤ p .

Conversely,

p  ≤ { (13) and monotonicity of G and ; }
G(h;q;m′) ;p  = { G is a functor }
G(h;q) ;Gm′;p  ≤ { (1) and monotonicity of ; }
G(h;q) ;Gn′;(Gn′)^{∗};Gm;p = { G is a functor }
G(h;q;n′) ;(Gn′)^{∗};Gm′;p = { (12) }
G(h;q;n′) ;p^{∗};p  ≤ { (2) and monotonicity of ; }
G(h;q;n′)

and therefore p = G(h;q;n′) as required.

□ It follows trivially from this theorem that if C is a category such that C ≅ Span(D) for some D, then C ≅ Span(Map(C)). This suggests that under appropriate conditions the the Span and Map functions might be mutually inverse operators on categories. The following theorem shows that the condition under which this is the case is the familiar unique map factorization property.

Theorem 4 Characterization Theorem. (C, ⊑) is a poset enriched category with unique map factorization if and only if

Span(Map(C)) ≅ C .

Proof. Suppose that Span(Map(C)) ≅ C, then by (12) C clearly has map factorization. The uniqueness of this factorization follows from Theorem 3 and the definition of the span preorder.

Conversely, suppose that C is a poset enriched category with unique map factorization. Then by Lemma 2, Map(C) has pullovers, so the category Span(Map(C)) certainly exists. The functor which defines its isomorphism with C is obviously F : Span(Map(C)) → C, where

\begin{matrix}F N & ˆ= & N \\ F ((|n, m|) : N → M) & ˆ= & (n^{∗};m : N → M) . \end{matrix}

Since C has map factorization, F is clearly surjective. It is also monotonic, welldefined and bijective, since Examples 5 (2) showed that the preorder on spans is the same as that on map factorizations. It remains to show that it is a functor: suppose that (|n, m|) : N → M and (|n′, m′|) : M → M′ are classes of spans in Map(C), and that (r, q) is a pullover of (m, n′), then

F ((|n, m|) ;(|n′, m′|)) = { (10) }
F (|r;n, q;m′|)  = { definition of F }
(r;n)^{∗};(q;m′)  = { contravariance of ^{∗} }
n^{∗};r^{∗};q;m′  = { Lemma 2 }
n^{∗};m;n^{′∗};m′  = { definition of F }
F (|n, m|) ;F (|n′, m′|) .

Therefore since F is monotonic and preserves identities, it is a functor, which establishes the result.

□

We have now established that skew span categories and categories with unique map factorization are essentially the same. The following corollary is now immediate, since the skew span construction preserves isomorphism.

Corollary 5.

Rel ≅ Span(Set)
Pow ≅ Span(Rel) .

The category Set is not itself isomorphic to a skew span category, since its only maps are bijections. Moreover, it is not possible to construct the skew span category of predicate transformers, since Pow does not have pullovers. So this hierarchy of span categories cannot be extended further in either direction. The relationship between predicate transformers and relations can be generalized however [23]: if Rel_{C} is the category of relations overs an arbitrary topos C, then the skew span category of Rel_{C} exists and is isomorphic to a category of predicate transformers.

5 Extending Functors

Associated with the construction of skew span categories is an extension of functors and adjunctions to lax functors and local adjunctions similar to that associated with ordinary span categories [17]. In this section we will first describe this extension of functors in the context of categories with unique map factorization, and then outline its application to programming languages.

Suppose that (C, ⊆) and (D, ⊑) are poset enriched categories where C has unique map factorization. Let F : Map(C) → Map(D) be a monotonic functor. Then F has a well-defined extension to F′ : C → D where for all spans (n, m) in Map(C),

F′(n^{∗};m) ˆ= (F n)^{∗};F m .

This extension is a monotonic graph morphism, but it is not necessarily a functor, only a lax functor: a lax functor H : C → D is a monotonic graph morphism such that for all composable pairs of arrows p, q and objects A in C,

\begin{matrix}HI_{A} & ⊑ & I_{HA} \\ H(p;q) & ⊑ & Hp;Hq . \end{matrix}

If F′ is a functor, then it is the unique extension of F in the sense that if G : C → D is another monotonic functor that agrees with F on Map(C), then G = F′. This is immediate from the fact that monotonic functors preserve maps and comaps: for all p ∈ Map(C),

Gp^{∗} = (Gp)^{∗} .

The following theorem shows that even if F′ is only a lax functor it is unique in the sense that it is the least extension of F.

Theorem 6. Suppose that (C, ⊆) and (D, ⊑) are poset enriched categories where C has unique map factorization. Let F : Map(C) → Map(D) be a functor and G : C → D be a lax functor that agrees with F on Map(C), that is F p = Gp for all p ∈ Map(C). Then F′ ⊑ G.

Proof. Suppose (n^{∗};m) ∈ C, then

F′(n^{∗};m)  = { definition of F′ }
(F n)^{∗};F m  = { F and G agree on Map(C) }
(F n)^{∗};Gm  ⊑ { (2) and monotonicity of G }
(F n)^{∗};G(n;n^{∗};m) ⊑ { G is a lax functor }
(F n)^{∗};Gn;G(n^{∗};m) = { F and G agree on Map(C) }
(F n)^{∗};F n;G(n^{∗};m) ⊑ { (1) }
G(n^{∗};m) .

□

These observations show that every endofunctor F in Rel is the unique extension of an endofunctor in Set and has a canonical extension to Pow which is isomorphic to the lax endofunctor F^{⋆} defined by

F^{⋆}p ˆ= [F ∋] ;⟨F (p;∋)⟩

where this definition uses the map factorization of predicate transformers given in Examples 3.

The technique of extending functors has applications to the theory of typed non-deterministic programming languages. Whereas deterministic languages like the lambda calculus have a definitive type structure provided by the cartesian closed category of sets and total functions, that of non-deterministic languages with either a relational or a predicate transformer semantics is less clearly defined, since neither category is cartesian closed. Therefore, when seeking to endow such languages with a natural type structure, it is useful to know that there is only one way to extend functors, and hence type constructors, from total functions to relations and predicate transformers. This fact was exploited in [24], where a relational calculus for program derivation was developed as a canonical extension of an established calculus for the derivation of functional programs [5]. Using the resulting calculus it was possible to unify a varied collection of dynamic programming algorithms.

The data types used in the functional calculus of [5] and its extensions are defined in [20] as fixed points of endofunctors in Set. Each data type occurs as either the initial algebra or final coalgebra of a functor, and the familiar functional programming operators such as fold or reduce are defined as homomorphisms on these data types. The reason that the calculus can be generalized so effectively to relations is that initial algebras are preserved under the extension of functors from total functions to relations. It has now been shown [25] that the extension of functors from relations to predicate transformers simply dualizes the universal properties of initial algebras by transforming them to final coalgebras. This means that the theoretical foundations for the future development of a corresponding calculus of predicate transformers are fully established. Such a calculus would combine all the benefits of the refinement calculus with the additional capability of reasoning about types.

6 An Application

In [16], it is shown how the description of specifications in terms of Hoare logic [15] can clarify the intuition behind the skew span representation of predicate transformers. Specification statements are represented as spans of relations, and the inference rules of Hoare logic are used to show that the refinement ordering on specifications is equivalent to the preorder on spans. Similarly, the inference rule for composition is used to show that the composition operator for spans would also be a suitable operator for specifications. In this section we will discuss the implications of these observations on the laws of the refinement calculus of [27]. In particular, they provide single complete rules for the refinement and composition of certain commands.

Until now we have only discussed the mathematical model of the refinement calculus: the monotonic predicate transformers. The language itself consists of a notation and a set of refinement laws for deriving programs from their specifications. It takes its inspiration from the earlier methods of Hoare and Dijkstra, but is innovative in incorporating both programs and specifications within a single framework: each command of the refinement calculus represents either a guarded command from Dijkstra’s programming language [8] or a non-executable specification. The transition from each specification to executable code is broken down into a sequence of development steps, each of which is justified by one of the refinement laws. Therefore it is important to know whether the set of laws is complete, which is to say that every valid refinement can be verified using only the given laws. We will now show how the span representation of predicate transformers provides two such completeness results.

One of the most general forms of specification statement in the refinement calculus is the following:

|[con X:E • [pre, post]]| .  (15)

We will call such statements transition statements. As we will see, it is possible to express any statement of the refinement calculus as a transition specification. Any program satisfying specification (15) will, when activated in a state satisfying pre, establish a final state satisfying post. The two predicates pre and post have free variables drawn from a set of program variables V and a set of logical variables E; the purpose of the logical variables is to relate initial and final values of the program variables. They are assumed to denote the same value when they occur in the precondition pre as they do in the postcondition post, and therefore must not be altered by programs in order to meet the specification. A simple example of a transition specification is that met by the program which increments the value of the program variable x by 1:

|[con X:E • [x = X, x = X + 1]]| .

The results of Sect. 4 show that the meaning of any command in the refinement calculus can be expressed not only as a monotonic predicate transformer, but also as an equivalence class of spans of relations. The predicates pre and post in (15) both describe a relationship between the two sets of variables E and V so they can be considered alternatively as relations from E to V, as it is observed in [16]. By doing so, and using the laws of the refinement calculus to calculate the meaning of (15), we find that it has the following simple expression as a class of spans of relations:

(|post, pre|) .

So every monotonic predicate transformer, and therefore any statement of the refinement calculus, corresponds to an equivalence class of transition specifications. The refinement ordering on specifications is defined to be the pointwise ordering on the corresponding predicate transformers, which is equivalent to the skew span preorder on spans of relations. Therefore, the latter can be translated into a single complete rule for the refinement of transition specifications. Let pre and post be a pair of logical formulae with free variables drawn from the set of the program variables V and the set of logical variables E. Similarly for the pair pre′ and post′ with respect to the sets V and E′. When it is necessary to make the set of free variables associated with a predicate explicit we will use subscripts to do so: for example pre would be written as pre_{EV}. The definition of the preorder on spans of relations translates to the following preorder relation between specifications:

Span P reorder :

|[con X:E • [pre, post]]| ⊑ |[con X′:E′ • [pre′, post′]]|

ˆ=

∃h_{EE′}• (pre ⇒ (∃X′:E′ • h ∧ pre′)) ∧ ((∃X′:E′ • h ∧ post′) ⇒ post) .

This rule can be broken down into the following three more familiar rules, which are together equivalent to it. For simplicity suppose now that unless indicated otherwise, all predicates share the same two sets of free variables E and V. Then the Span Preorder rule is equivalent to the following:

1. W eaken P recondition: If pre ⇒ pre′ then

|[con X:E • [pre, post]]| ⊑ |[con X:E • [pre′, post]]| .

2. Strengthen P ostcondition: If post′ ⇒ post then

|[con X:E • [pre, post]]| ⊑ |[con X:E • [pre, post′]]| .

3. Change logical variable:

|[con X′:E′ • [(∃X:E • h_{EE′} ∧ pre), (∃X:E • h_{EE′} ∧ post)]]|

⊑

|[con X:E • [pre, post]]| .

Both the first two of these laws occur among the laws of the refinement calculus. Law (3) is not listed explicitly, but is derivable within the calculus, so this shows that the laws of the refinement calculus are complete for proving refinements of transition specifications.

Similar reasoning can be used to translate the skew span composition operator into a composition law for transition specifications. For simplicity we will just consider the case where the specifications being composed share the same set of logical variables and program variables E and V respectively. The composition becomes:

Span Composition :
|[con X:E • [pre, mid]]|;|[con X:E • [mid′, post]]|
ˆ=
|[con Y :D • [(∃X:E • h_{DE} ∧ pre), (∃X:E • h′_{DE} ∧ post)]]|

where (h, h′) is any pair of predicates such that for all predicates ψ such that Y does not occur free in ψ,

(∃Y :D • (h ∧ (∀X:E • h′ ⇒ ψ)) = (∀x:V • mid ⇒ (∃X:E • mid′ ∧ ψ)) .

One suitable choice for h and h′ is the following: let PE denote the set of predicates with free variables drawn from E, and let D = PE × PE. Then for all Y : D there exist predicates ϕ_{E} and ψ_{E} such that Y = (ϕ, ψ), so we can define h and h′ as follows

\begin{matrix}mids_{D} & ˆ= & (∃X:E • mid ∧ ϕ) ⇒ (∃X:E • mid′ ∧ ψ) \\ h & ˆ= & mids ∧ ψ \\ h′ & ˆ= & mids ∧ ϕ . \end{matrix}

This definition of composition is rather unwieldy, and unlike the law for refinement, it cannot be proved from the laws of the refinement calculus, although it is possible to show that the expression on the right of the definition is refined by that on the left. Therefore the laws are complete for proving refinements of specifications into smaller pieces. The laws are usually only used in this way, since the process of derivation usually involves breaking a specification down into manageable parts, each of which is independently refined to code. However, it is conceivable that it might be useful sometimes to have a rule which does the opposite, and combines two specifications into a larger one. For example, it might be possible to substitute a library procedure which meets the composite of two specifications, but neither individually. Or, more probably, it might be useful once derivation is completed, to calculate the loosest specification satisfied by the composite of two programs whose separate specifications are known.

Acknowledgements

The authors would like to thank Tony Hoare and Carroll Morgan for their comments and encouragement. We gratefully acknowledge the financial support of the SERC and British Petroleum International, which made our cooperation possible.

References

1. Back, R.J.R.: A Calculus of Refinements for Program Derivation. Acta Informatica 25 (1988) 593-624

2. Barr, M.: Relational Algebras. In Reports of the Midwest Category Seminar IV, Springer-Verlag Lecture Notes in Mathematics 137 (1069) 435-477

3. Benabou, J.: Introduction to Bicategories. Springer-Verlag Lecture Notes in Mathematics 47 (1967)

4. Bird, R.S.,de Moor, O.: Solving Optimisation Problems with Catamorphisms. (1992) This volume.

5. Bird, R.S.: Lectures on Constructive Functional Programming. In M. Broy, editor. Constructive Methods in Computing Science, Springer-Verlag NATO ASI series F 55 (1989) 151-216

6. Carboni, A.,Kasangian, S.: Bicategories of Spans and Relations. Journal of Pure and Applied Algebra 33 (1984) 259-267

7. Carboni, A., Kelly, M., and Wood, R.: A 2-Categorical Approach to Geometric Morphisms I. Sydney Pure Mathematics Research Reports 89-19 (1989). Department of Pure Mathematics, University of Sydney, NSW 2006, Australia.

8. Dijkstra, E.W.: A Discipline of Programming. Prentice-Hall, Englewood Cliffs (1976)

9. Gardiner, P.H.B.: Data Refinement of Maps. Draft (1990)

10. Freyd, P.J. and Scedrov, A.: Categories, Allegories, North-Holland (1990)

11. Gardiner, P.H.B., Morgan, C.C.: A Single Complete Rule for Data Refinement. Technical Report PRG-TR-7-89, Programming Research Group, 11 Keble Road, Oxford OX1 3QD, 1989.

12. Gray, J.W.: Formal Category Theory: Adjointness for 2-categories. Springer-Verlag Lecture Notes in Mathematics 391 (1974)

13. Herrlich H., Strecker G.E.: Category Theory. Allyn and Bacon Inc., Boston (1973)

14. Hesselink, W.H.: Modalities of Nondeterminacy. In Beauty is Our Business: A Birthday Salute to Edsger W. Dijkstra. Springer-Verlag, (1990) 182-193

15. Hoare, C.A.R.: An Axiomatic Basis for Computer Programming. Communications of the ACM 12(10) (1969) 576-580,583

16. Hoare, C.A.R. Handwritten note (1991)

17. Jay, C.B.: Local Adjunctions. Journal of Pure and Applied Algebra 53 (1988) 227-238 18. Johnstone, P.T.: Stone Spaces Cambridge University Press (1982)

19. Lambek, J.: Subequalizers. Bulletin Amer. Math. Soc. 13(3) (1970) 337-349

20. Malcolm, G.: Data Structures and Program Transformation. Science of Computer Programming 14 (1990) 255-279

21. Martin, C.E.: Preordered Categories and Predicate Transformers. D. Phil Thesis. Programming Research Group, 11 Keble Road, Oxford OX1 3QD. (1991)

22. de Moor, O.: Categories, Relations and Dynamic Programming. PRG Technical Report PRG-TR-18-90, Programming Research Group, 11 Keble Road, Oxford OX1 3QD. (1990)

23. de Moor, O., Gardiner, P.H.B., and Martin, C.E.: Factorizing Predicate Transformers in a Topos. Draft (1991)

24. de Moor, O.: Categories, Relations and Dynamic Programming. D. Phil Thesis. PRG Technical Monograph PRG-98, Programming Research Group, 11 Keble Road, Oxford OX1 3QD. (1992)

25. de Moor, O.: Inductive Data Types for Predicate Transformers. Information Processing Letters (to appear)

26. Morgan, C.C.: Programming From Specifications. Prentice-Hall (1990)

27. Morgan, C.C., Robinson, K. and Gardiner, P.H.B.: On the Refinement Calculus. PRG Technical Monograph PRG-70. Programming Research Group, 11 Keble Road, Oxford OX1 3QD. (1988)

28. Morris, J.M.: Laws of Data Refinement. Acta Informatica 26 (1989) 287-308

This article was processed using the LaTEX macro package with LLNCS style