A Class of Graph Algorithms

Jesús N. Ravelo Linacre College, Oxford

January 1996

Submitted in support of an application for transfer to D.Phil. status.

�

Oxford University Computing Laboratory Programming Research Group

A Class of Graph Algorithms

Jesús N. Ravelo

Abstract

Several graph problems are shown to be instances of the abstract problem of selecting representative elements from a closure-generated set. These are the single-source minimum paths problem, the reachability set of a given vertex, and the construction of rooted trees. Algorithms to compute such representatives are derived from the specification of the general problem. Instances of the algorithms include Dijkstra’s minimum paths algorithm, and depth-first/breadth-first graph traversals. A relational calculus for algorithms derivation is used as algebraic framework. This calculus, of a point-free reasoning character, is extended with categorical points to allow a clearer phrasing and manipulation of some algorithmic expressions. Pointwise reasoning can thus be naturally carried out within the extended calculus.

Contents

1 Introduction 1 1.1 Graph Algorithmics . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Program Construction Framework . . . . . . . . . . . . . . . . . 2 1.3 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4

2 A Point-Free Calculus of Relations 5

3 A Class of Graph Problems 8 3.1 Single-Source Minimum Paths . . . . . . . . . . . . . . . . . . . . 8 3.2 Single-Source Shortest Paths – Unweighted Case . . . . . . . . . 11 3.3 Reachability . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.4 Rooted Trees . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.5 Abstract Specification . . . . . . . . . . . . . . . . . . . . . . . . 14

4 Adding Pointwise Reasoning 16 4.1 Using Points . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 4.2 Mins Calculus . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 4.3 Discussion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22

5 Main Derivation 23 5.1 Generalising Closure . . . . . . . . . . . . . . . . . . . . . . . . . 23 5.2 Main Derivation . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 5.3 Towards Functional Refinements . . . . . . . . . . . . . . . . . . 27 5.4 Two Particular Implementations . . . . . . . . . . . . . . . . . . 31

6 Conclusions 34

A The Thinning-the-Closure Rule 40

B Domains and Invariants 44

1 Introduction

Over the last two decades the calculational approach to algorithm design and software construction has become an important area of research in computer science. A formal specification of a problem is taken as the starting point, and transformation rules, guaranteed to preserve semantics, are then successively applied until an algorithm is obtained. The final product is certain to meet its formally stated requirements, and the key insights into the design of the algorithm can be better appreciated. Herein we specify a class of graph problems and derive algorithmic solutions for them. The class of problems include the single-source minimum paths problem, the reachability set of a given vertex, and the construction of rooted trees. They are treated uniformly as instances of an abstract specification. Generic algorithms are obtained, and instantiated to Dijkstra’s minimum paths algorithm, depth-first and breadth-first traversals. The algebraic framework for algorithms derivation used is a categorical calculus of relations developed by Bird and de Moor [13]. This calculus, of a pointfree reasoning character, is extended with categorical points to allow a clearer phrasing of some algorithmic expressions that often arise. Pointwise reasoning can thus be naturally carried out within the extended calculus.

A different presentation of some of the results given here can be found in [9]. Therein, an imperative algorithm is presented and its correctness proved. We now look for derived (instead of proved-correct) functional (instead of imperative) algorithms. Formalisation of the points extension of the calculus was the key to a succesful development. The same class of graph problems has also been tackled by other computer scientists using different calculational frameworks [5, 38, 42]. There are two main features brought together in this work. On one hand, a variety of algorithms linked to the well-developed subject of graph theory and, on the other hand, new methodologies for algorithm design characterised by their emphasis on calculation. A brief account of these subjects follow.

1.1 Graph Algorithmics

Graph theory is nowadays an important tool in the solution of a wide variety of practical problems in many different fields. Much of the theory has actually been developed motivated by its practical applications. This can be seen in what is recognised as the origin of graph theory, Euler’s solution in 1735 of the Königsberg bridge puzzle, and several further developments such as Kirchhoff’s theory of trees in 1847 for its application in the study of electrical networks and Ford and Fulkerson’s theory of network flows in 1956 as an application in operations research. Other fields that have benefited from graph theoretical results include chemistry, biology, economics, geography, architecture, and social sciences (see e.g. [22]). In most practical situations that arise in these fields, graphs that model a real-life problem must be analysed in some way or other, and such graphs tend to be large and complex. Computer assistance to perform those analyses is then most valuable and, consequently, so is the design of efficient algorithms. A large number of graph algorithms have indeed been developed over the last few decades, and a class of graph problems for which efficient algorithms are not likely to be found has been identified, giving birth to the theory of NP-Completeness. A good introduction to graph theory and algorithmics can be found in [47].

Clearly, graph algorithmics is a most relevant subject with applications in many other fields. Most algorithmics textbooks dedicate significant space to its study (see e.g. [16, 29, 48]). However, their presentations follow, more often than not, a traditional approach to algorithm design. Algorithms are first given and afterwards, if at all, shown correct with respect to their specification. Several well-known graph algorithms, though sometimes compactly presented, have complicated correctness proofs. Authors must take pains to present clear proofs and yet, due to the lack of adequate algebras to do so, their efforts often result in arguments that are still difficult to read. In a different style (and serving other purposes), Knuth presents graph “literate programs” in [30] to be both read by humans and interpreted by machines. The presentation parts intended for humans are dedicated to explain features of the algorithms in their final form, with little insight to the design decisions that originated them.

Our main goal is to reveal the core of the strategies used to design algorithms in an algebraic fashion. There is a large variety of well-known graph algorithms based on several different paradigms and equally diverse graph theoretical concepts. Some graph algorithms are instances of general design paradigms. Kruskal’s algorithm and Prim’s algorithm for minimum spanning trees [31, 41], and Dijkstra’s minimum paths algorithm [19] are examples of the greedy strategy. Some others are designed in very specific and peculiar ways, yet based on similar structural graph properties. This is the case of a class of algorithms based on depth-first search traversals, including a version of topological sorting, Hopcroft and Tarjan’s algorithm and Kosaraju and Sharir’s algorithm for strongly connected components [25, 44], Tarjan’s biconnected components [46], and many others. Problems of these two classes are worth analysing in an algebraic framework. The former for their common design patterns, and the latter for their similar graph structural grounds. The effectiveness of such analyses depends on an adequate abstract setting for the study of both program construction and graphs.

1.2 Program Construction Framework

As mentioned earlier, we use a categorical calculus of relations for program construction. Specifications of problems for which algorithmic solutions are to be sought are naturally non-deterministic, associating input data to desired outputs in a relational fashion. Deterministic algorithms that “solve” a specification are just functions that respect such relation, i.e. that are included (in a set-theoretical sense) in it. A calculus of relations permits algorithms and specifications to be inmersed in the same reasoning space. The importance of relations to software development is already present in Dijkstra’s seminal work on predicate transformers for imperative programs [20]. It has evolved into a uniform setting for specifications and programs in Morgan’s refinement calculus [39]. A more general framework is needed if we also want to make space for functional programs. Indeed, Bird and de Moor’s (BdM’s) relational calculus developed from work on a calculus for functional programs by Bird and Meertens [8, 33]. The relevance of functional languages is nowadays largely recognised (see e.g. [26, 27]) after Backus convincingly argued in favour of them in the late 70s [6].

A typical case of indeterminacy is found in optimization problems, because several different solutions can all be optimal. This was one of the motivations for de Moor’s initial work on relational derivation of programs [18]. When it comes to graph problems, optimization is found all over the place: minimum spanning trees, maximum matchings, shortest paths, maximum network flows, etc. Generic algorithmic solutions for several classes of optimisation problems, including some of the aforementioned graph problems, have been worked out within BdM’s calculus [10, 11, 12, 13, 18]. Nevertheless, a number of them remain uncovered, which suggests more research to be undertaken with an eye to graph algorithms.

From a different perspective, the nature of graphs is relational, which makes a relational framework most convenient to reason about them. However, there is a subtle conflict in this dual advantage of a calculus of relations to derive algorithms and manipulate graphs. BdM’s calculus treat specifications/algorithms in a point-free manner, thereby abstracting from data in order to reason more compactly about the processing of it. And graphs are the data to be processed. This will not actually represent a problem, but we need bear in mind the dual role the calculus can play analysing algorithms and graph properties. Schmidt and Ströhlein have exploited the applicability of relational calculi to graphs manipulation. In [43] they present, in relation-algebraic terms, a fair amount of graph theoretical concepts along with applications to databases, games and program verification. More concerned with algorithm derivation, Möller has developed a calculus of formal languages and relations with which compact calculations of some graph and pointer algorithms have been successfully carried out [37, 38, 42]. In his framework, relations are only used to reason about data, while algorithms are manipulated at a functional level. Indeterminacy and partiality are dealt with via set-valued functions, so a relational treatment of algorithms is present in spirit yet not explicitly.

The other important feature of BdM’s calculus is its categorical foundation. Compactness and concision are most valuable in the program transformation area. Excessive detail in the expressions being manipulated makes them long and complex, thereby obscuring argumentations, often unnecessarily. Category theory advocates minimisation of such detail, providing an adequate and welldeveloped framework to build compact mathematical arguments. It had gained a great deal of interest from the computer science community in recent years [7, 40], in particular from the functional programming advocates. Interestingly enough, the laws of the calculus of functions of Bird and Meertens were later found to be governed by more general categorical concepts [45]. Freyd and Ščedrov’s allegories [24] extends category theory, initially concerned with the motivating model of functions, to relations; BdM’s calculus builds on this work. Also, a categorical treatment of datatypes has benefited the program transformation area [32], and the approach is extendable to the relational, or allegorical, setting (see [18]). Backhouse and others at Eindhoven University have been exploring the same idea of relation-algebraic treatment of datatypes [2], yet not relying on categorical grounds. The level of abstraction is high enough to allow concise reasoning about programs parameterised by datatypes; two examples can be found in [4, 14].

1.3 Outline

The present chapter 1 introduces the goals of this work, and related computer science areas. Chapter 2 briefly presents the main features of BdM’s calculus, to proceed with the specification of the class of problems in chapter 3. The relational calculus is extended to include categorical pointwise reasoning in chapter 4, and such extension is immediately applied to the manipulation of part of the generic problem at issue. Chapter 5 contains the main derivation of the graph algorithms. Concluding remarks are given in the final chapter 6.

2 A Point-Free Calculus of Relations

The basics of the calculus of relations of Bird and de Moor, mainly based on axioms drawn from allegory theory [24], are introduced in this chapter. More than what is contained here will be needed, so other features will be reviewed in coming chapters as we proceed. Knowledge of categories and functors is assumed.

Basic Structure We work in the category Rel of sets and relations. Relations are typed backwards, denoting by R : X ← Y a relation to X from Y; we think of relations as taking inputs on the right and delivering outputs on the left. Consistently, composition goes backwards, with R · S : X ← Z for R : X ← Y and S : Y ← Z. Composition is associative with identity relations id : X ← X as units.

Each relation R : X ← Y has a converse relation R^{∘} : Y ← X; converse preserves identities and reverses composition (i.e. (R · S)^{∘} = S^{∘} · R^{∘}). Each homset Rel(X, Y), that is, each set of relations of type X ← Y, forms a complete, completely distributive, complemented lattice (Rel(X, Y), ∪, ∩, , ∅, Π). ∪ and ∩ denote the join and meet operators, the complementation or negation operator, and ∅ and Π are the empty (bottom) and universal (top) relations. Hence, relations can be compared via a partial order ⊆, where R ⊆ S denotes R = R ∩ S, and also S = R ∪ S. This ordering is preserved by converse.

Composition distributes over join, but only weakly distributes over meet in that

(R ∩ S) · T ⊆ R · T ∩ S · T
R · (S ∩ T) ⊆ R · S ∩ R · T

Composition is assumed to bind more tightly than join and meet. Another axiom, called the modular law, gives a weak converse of distributivity over meet:

R · S ∩ T ⊆ R · (S ∩ R^{∘} · T)
R · S ∩ T ⊆ (R ∩ T · S^{∘}) · S

Other Operators We shall use the notions of division, implication and substraction in the calculus. From distributivity of composition and meet over join, and the theory of Galois connections [1], division and implication can be uniquely characterised by

X ⊆ R\S ≡ R · X ⊆ S
X ⊆ S/R ≡ X · R ⊆ S
X ⊆ R ⇒ S ≡ X ∩ R ⊆ S

They can be interpreted set-theoretically as follows:

y (R\S) x ≡ (∀z : z (R) y : z (S) x)
y (S/R) x ≡ (∀z : x (R) z : y (S) z)
y (R ⇒ S) x ≡ (y (R) x ⇒ y (S) x)

Equally, substraction can be defined by

R − S ⊆ X ≡ R ⊆ X ∪ S

In the presence of complementation, implication and substraction satisfy respectively R ⇒ S = \overline{R} ∪ S and R − S = R ∩ \overline{S}. The distribution properties of substraction will be used a good deal:

(R_{1} ∪ R_{2}) − S = (R_{1} − S) ∪ (R_{2} − S)
R − (S_{1} ∪ S_{2}) = R − S_{1} − S_{2}

Functions A relation R is entire if id ⊆ R^{∘}·R, and simple if R·R^{∘} ⊆ id. That is, an entire relation delivers at least one output for each input, and a simple one delivers at most one output for each input. A function is an entire and simple relation. Sets and functions form a subcategory Fun of Rel. Functions will be usually denoted by the letters f, g, h. Useful properties of functions include the so-called shunting rules

f · R ⊆ S ≡ R ⊆ f^{∘}· S
R · f^{∘} ⊆ S ≡ R ⊆ S · f

and that inclusion of functions is equivalent to equality:

f ⊆ g ≡ f = g

Least Fixed Points Since the homsets of relations are complete lattices, monotonic endofunctions ϕ on them (i.e., such that X_{1} ⊆ X_{2} ⇒ ϕX_{1} ⊆ ϕX_{2}) have least fixed points. The well-known Knaster-Tarski theorem states that such a least fixed point is also the least solution of ϕX ⊆ X. We denote it by (μX: ϕX), and characterise it by the two aforementioned properties:

(μX: ϕX) = ϕ(μX: ϕX)
(μX: ϕX) ⊆ Y ⇐ ϕY ⊆ Y

Closure A preorder R is a relation which is both reflexive (id ⊆ R) and transitive (R · R ⊆ R). The reflexive-transitive closure S^{∗} of a relation S is the least preorder that contains S. It is a well-known fact that S^{∗} is also the least solution of other equations:

S^{∗} = (μX : id ∪ X ·S)
= (μX : id ∪ S·X)

The second one is a particular case of the more general result

S^{∗}·T = (μX : T ∪ S·X)

Finally, note that reflexivity and transitivity are preserved by converse. Thus, the converse of a preorder is also a preorder.

Powersets We can move between a relation R : X ← Y and its corresponding set-valued function ΛR : PX ← Y, called the power-transpose of R and defined in set theory as (ΛR) y = { x | x (R) y }. This isomorphism is formalised in the calculus as follows. For every set X there exists a set PX, called the powerset of X, and a relation ∈ : X ← PX, called the membership relation on X. For every relation R : X ← Y, there exists a function ΛR : PX ← Y such that

f = ΛR ≡ ∈ ·f = R  for all functions f : PX ← Y

From the above it follows that power-transpose absorbs functions, that is, for every R relation and f function Λ(R · f) = ΛR · f.

Products and Coproducts For every pair of sets X and Y, we can form its product X × Y and its sum or coproduct X + Y. Products come equipped with projection functions outl and outr, and for each pair of relations R : X ← Z and S : Y ← Z, their “split” ⟨R, S⟩ : X × Y ← Z is defined as

⟨R, S⟩ = outl^{∘}· R ∩ outr^{∘}· S

Analogously, coproducts are equipped with injection functions inl and inr, and for every R : Z ← X and S : Z ← Y, the “case” relation [R, S] : Z ← X + Y is defined as

[R, S] = R · inl^{∘} ∪ S · inr^{∘}

Product and coproduct become functors in Rel defining

R × S = ⟨ R · outl , S · outr ⟩
R + S = [ inl · R , inr · S].

3 A Class of Graph Problems

This chapter presents the specification of the class of graph problems mentioned in the introduction. We start with the richest one, the minimum paths problem, and then proceed with the others. At the end, an abstract specification that unifies them all is presented. Before proceeding with the problems, graphs are introduced.

A graph G is a 4-tuple (V, E, to, from), where V and E are respectively the set of vertices and the set of edges, and to and from are functions of type V ← E that determine the extreme vertices of an edge. As expected, an edge e goes to to e from from e. Note that both loops and multiple edges are allowed. Given a graph G, its adjacency relation vadj : V ← V between vertices is defined as vadj = to · from^{∘}. Although less commonly used, we can also define a adjacency relation eadj :E ← E between edges as eadj = from^{∘} · to.

3.1 Single-Source Minimum Paths

In this problem we are provided with a weighted graph, that is, a graph G and a function weight :IR^{+} ← E that assigns a weight, or cost, to each edge. We are also given a vertex s, called the source. For every vertex v reachable from s, a minimum path to v from s is to be found. We aim to specify this problem in the form

minpaths = selectmins · genallpaths

The generating function genallpaths takes a vertex s and returns the set of all paths in G that start in s. The other component selectmins gives a subset of its input that contains a minimum path for each ending vertex; it is a relation because minima are not unique.

We first proceed with the generator. A path to v from u in a graph G is a sequence

[v_{n}, e_{n}, v_{n−1}, e_{n−1}, … v_{1}, e_{1}, v_{0}],
where (∀i : 1 ≤ i ≤ n : to e_{i} = v_{i} and from e_{i} = v_{i−1})
and v = v_{n}
and u = v_{0}.

Clearly, there is some redundancy in this definition of paths. For a non-empty path (i.e. one in which n ≥ 1), all the information can be recovered from just its subsequence of edges. This is not the case for empty paths, all of which have an empty subsequence of edges. In order to avoid unnecessary redundancy without loss of information, we shall represent a path by its subsequence of edges and the initial vertex [e_{n}, e_{n−1}, … e_{1}, v_{0}]. Symmetrically, the final vertex and edges would do, but the chosen representation suits better the problem in analysis.^{1} Thus, using Orwell-like notation [36] the type Path is defined as

Path ::= wrap V | cons (E, Path).

The set-valued function genallpaths can be specified as the power-transpose of the relation pathfrom : Path ← V such that p (pathfrom) v if p is a path starting in v. We define it as pathfrom = ispath? · start^{∘} where start is the function

start (wrap v) = v
start (cons (e, p)) = start p

and ispath is the predicate

ispath (wrap v) = True
ispath (cons (e, p)) = ispath p ∧ from e = end p

Predicates are modelled by coreflexive relations, i.e., subsets of the identity relation. ispath? above is such that p (ispath?) p if and only if predicate ispath holds for p. The function end is the counterpart to start that gives the final vertex of a path:

end (wrap v) = v
end (cons (e, p)) = to e

Having done with the generator genallpaths, we now turn to selectmins. A minimum path for each ending vertex is wanted. Hence, we can think of partitioning the set of generated paths according to their ends, and then drawing a minimum from each of such classes. This idea can be generalised to a parameterised selector mins(Q, R), with Q an equivalence relation and R a preorder. (An equivalence relation is a symmetric (Q^{∘} = Q) preorder.) The mins relation is typed PX ← PX for Q and R of type X ← X; and x (mins) y if x contains, for each class in y induced by Q, one (and only one) minimum element according to R. Its formal definition is postponed to the end of this chapter. For our specific problem, two paths will be regarded as equivalent if they end in the same vertex:

sameends = end^{∘} · end.

1The mirror version, single-destination minimum paths, would benefit from the final vertex representation of paths. Nevertheless, each version of the problem can be expressed in terms of the other by means of the converse graph conv G = (V, E, from, to).

The cost of a path is defined to be the sum of the weights of its edges. Via such cost function, a preorder better over paths is induced by the standard ordering over numbers:

cost (wrap v) = 0
cost (cons (e, p)) = weight e + cost p
better = cost^{∘} · leq · cost

where the symbol + above refers to addition of real numbers and leq is the less-than-or-equal relation.

The specification for the single-source minimum paths problem then reads

minpaths = mins (sameends, better) · Λpathfrom

Transforming the Generator

We now transform the generator into a more suitable form for later manipulations. For that, we need to review the categorical approach to datatypes. (A good introduction can be found in [32], more complete relational treatments in [2, 13].) The above declaration of the datatype Path declares [wrap, cons] : Path ← FPath to be the initial F-algebra of the functor FX = V + E × X. This means that for every other F-algebra [R, S] : X ← FX there is a unique homomorphism ([R, S]) : X ← Path, called a catamorphism [34], characterised by

T = ([R, S]) ≡ T · [wrap, cons] = [R, S] · FT.

The right-hand side above can be read

T · wrap = R
T · cons = S · (id × T)

With this machinery, we can define start, end, ispath? and cost as follows:

start = ([ id , outr ])
end = ([ id , to · outl ])
ispath? = ([ wrap , cons · step (from^{∘}· end) ])
cost = ([ zero! , plus · (weight × id) ])

The coreflexive step R corresponds to a predicate on pairs that holds on (x, y) if x (R) y. It is defined as step R = id ∩ outl^{∘}·R·outr.

Our generator has the form of a hylomorphism [35], that is, the composition of a catamorphism after the converse of another. Hylomorphisms can be expressed as least fixed points: ([R]) · ([S])^{∘} = (μX : R · FX · S^{∘}). This will allow us to transform pathfrom into a closure expresion:

pathfrom

= { definition and hylomorphisms }

(μX : [ wrap , cons · step (from^{∘}· end) ] · (id + id × X) · [ id , outr ]^{∘})

= { coproducts }

(μX : wrap ∪ cons · step (from^{∘}· end) · (id × X) · outr^{∘})

= { products }

(μX : wrap ∪ cons · step (from^{∘}· end) · outr^{∘} · X)

= { step property }

(μX : wrap ∪ cons · ⟨ from^{∘}· end , id ⟩ · X)

= { closure, introducing extend }

extend^{∗} · wrap

Hence, the generator takes the following shape using the fact that wrap is a function and the power-transpose absorption law:

Λpathfrom = Λ(extend^{∗} · wrap) = Λextend^{∗} · wrap where

extend = cons · ⟨ from^{∘}· end , id ⟩.

3.2 Single-Source Shortest Paths – Unweighted Case

A simpler version of the single-source minimum paths problem is obtained by uniformly assigning a weight of one to each edge. The presence of multiple edges can thus be considered irrelevant, since any of them would contribute equally to the total cost. Assuming there are no multiple edges in a graph, the information provided by its adjacency relation is complete and so we can do only with (V, vadj ) for the graph G = (V, E, to, from). That is, (E, to, from) can be uniquely determined, up to isomorphism, from (V, vadj ) in this case. In allegorical terms, the functions to and from tabulate the relation vadj . A pair of functions f, g is a tabulation of R if R = f · g^{∘} and f, g are jointly monic, i.e., f^{∘}·f ∩ g^{∘}·g = id. The fact that the pair of functions involved in a tabulation are jointly monic correspond to the absence of parallel, or multiple, edges.^{2}

We now proceed as in the last section to specify this variant of the paths problem. We do so only by means of (V, vadj ), ignoring the edges information. A path is now a non-empty sequence of vertices [v_{n}, … v_{1}, v_{0}], such that (∀i : 1 ≤ i ≤ n : v_{i} vadj v_{i−1}). The type Path, the functions start and end, and the “healthiness” coreflexive are redefined accordingly:

2This graph representation issue is also discussed in [43] as the correspondence between, under their terminology, directed graphs and 1-graphs. The discussion is slightly more general there since edges can lack either extreme –or both–; that is, to and from are only required to be simple.

Path ::= wrap V | cons (V, Path)
start = ([ id , outr ])
end = ([ id , outl ])
ispath? = ([ wrap , cons · step (vadj · end) ])

The generator of all paths from the given source is again Λpathfrom, with pathfrom = ispath? · start^{∘}. A manipulation similar to the one of the weighted case yields the desired closure:

pathfrom = extend^{∗} · wrap where

extend = cons · ⟨ vadj · end , id ⟩.

Equivalence and cost ordering of the paths are easily adapted to

sameends = end^{∘} · end
length = ([ zero! , add1 · outr ])
shorter = length^{∘} · leq · length

with add1 the successor function on natural numbers. We finally specify

shpaths = mins (sameends, shorter) · Λpathfrom
= mins (sameends, shorter) · Λextend^{∗} · wrap

3.3 Reachability

This is the simplest problem of all the ones considered herein. Its aim is to find all the vertices that can be reached from a given one. Such a set is trivially obtained using the (vertex) adjacency relation as base generator. As for the parameterisation of the selection, every vertex is relevant on its own so no pair of different elements are set to be equivalent. Using id as the equivalence relation for mins leaves the role of the comparison preorder useless, since each induced class is unitary; we shall use Π as a symbol for “no special preferences”. This vacuous use of mins corresponds to the fact that for every R preorder mins (id, R) = id. The reachability set problem reads

reachset = mins (id, Π) · Λvadj^{∗}

3.4 Rooted Trees

A rooted tree of a graph G is a subgraph G′ of it with a distinguished vertex r (for root) such that: (i) every vertex is reachable from r, (ii) it has no circuits, and (iii) every vertex has at most one predecessor. The problem we treat hereafter is the construction of full rooted trees of a given graph G = (V, E, to, from), with the desired root r ∈ V as input. We mean by a full tree one that contains every vertex reachable from the root.

We shall represent a tree by its set of edges, all the vertices being determined from it via the extreme functions to and from since a tree has no isolated nodes. Only when a tree is composed solely of its root do we have an isolated vertex (and an empty set of edges), such degenerate case will not represent a problem. We shall use a suitable base generator to initially obtain all the edges that can be reached from the given root. (Such full set of edges would comprise what is often called in the literature a rooted graph.) This full set will then be sift through an appropriate instantiation of mins to obtain a tree.

The obvious base generator is the edge adjacency relation. However, a starting edge is lacking since we are given not an edge but a node as starting-point. We tackle this problem defining an extended graph with an additional special vertex and edges leading from it to every other node, thereby creating a oneto-one correspondence between the original vertices and the added edges. Such correspondence provides us the starting edge associated to the input root. This “imaginary” edge will be part of any resulting tree and, therefore, so will be the added new vertex. The above-mentioned degenerate case of tree will then be made up of that single edge instead of none. A formal definition of the described extension for a graph G = (V, E, to, from) follows (prefixes x, orig and new stand for extended, original and new, respectively):

xgraph G = (xverts V, xedges E, xto, xfrom) where

xverts V ::= origv V | newv
xedges E ::= orige E | newe V
xto = ([ origv · to , origv ])
xfrom = ([ origv · from , newv! ])

The defined datatypes correspond to the coproducts V + 1 and E + V. The so-called unit of the allegory, 1, represents a one-element set.

We are now fully equipped to specify the problem. The relational generator is xeadj^{∗}· newe where xeadj = xfrom^{∘}· xto. Its associated set-valued function generates the full subgraph reachable from the inputted root. This subgraph satisfies condition (i) of the definition of rooted tree. To comply with (ii) and (iii), some edges shall be filtered out. Assuming (i), the conjunction of conditions (ii) and (iii) is equivalent to

(ii’) the root has no predecessors, and every other vertex has exactly one.

Since we made up a special predecessor for the root, this condition reads that every original vertex must have exactly one predecessor. The mins selector is used as a sieve setting two edges to be equivalent when they lead to the same node: sameends = xto^{∘} · xto. Among the edges of an equivalence class thereby constructed no one is preferred to any other and, therefore, the universal relation Π will serve as comparison preorder. However, condition (i) could be lost after the filtering. We use a coreflexive connected? after mins to ensure that condition (i) is preserved, i.e., that every edge can still be traced back within the set to the new special node. We specify

rootedtree = connected? · mins (sameends, Π) · Λxeadj^{∗} · newe

3.5 Abstract Specification

A common pattern can be seen in the specifications shown before:

P = mins (Q, R) · ΛS^{∗}

We call P the minimum-representatives of closure problem. Q and R are an equivalence and a preorder that determine the selection of minima, and S is called the base generator or spawning relation. The problems of the sections above are instances of it, some with a particular initialisation, some with an additional post-condition. The next step is to refine P to algorithms that compute such representatives, which will be done in the following chapters. In the process, some conditions will be required on the parameters Q, R, S of the specification. Algorithmic solutions for instances of P can be obtained verifying that those provisos are met by the particular parameters.

For a formal definition of mins, recall that x (mins(Q, R)) y if x contains exactly one R-minimum for each Q-class in y. We define

mins (Q, R) ˆ= uniq Q · thin (Q ∩ R)

where

uniq S = id ∩ ∈\(S ⇒ id)/∋
thin S = ∈\∈ ∩ (∋·S)/∋

Informally, this says that a subset is returned with at most one element per Q-class such that every element of the input has a Q-equivalent but R-better element in the output. This corresponds to the previously stated informal notion of mins. For completeness sake, we spell out another definition of mins, somehow more natural in the sense that the notions of minimum and equivalence classes are directly used but that requires more calculus not introduced (the intersection or cap function and the powerset functor P):

mins (Q, R) = uniq Q · P(min R) · Λ(class Q) where

min R = ∈ ∩ R/∋
class Q = cap · ⟨ ΛQ·∈ , id ⟩

Both definitions are equivalent provided Q is an equivalence relation and R a preorder. The first is more suitable for manipulations to be subsequently carried out.

4 Adding Pointwise Reasoning

Point-free reasoning has been shown to be effective in the area of program transformation. For that reason, among others, allegory theory has provided an adequate foundational framework for BdM’s relational calculus. However, a pointwise proof is sometimes more effective, tabulations being the tool that has been used to carry out such proofs (see [13]). Curtis proposed an alternative way out through graphical representations, which often give hints of next steps in a proof more likely to succeed [17]. Yet another approach is to use categorical points, also called constants or elements: functions from the unit 1. Recall that 1 represents a unitary set.

Most of the cases in which point-free proofs are less effective that pointwise ones involve products and powersets. These two features sometimes make pointfree expressions be pervaded by the combinators outl,outr and the membership relation ∈ in such a way that the meaning of the whole tend to be obscure. In such cases proofs are often hard to work out, contradicting the symbol-guided nature that should characterise a point-free style. We propose to treat these cases extending BdM’s calculus with the aforementioned notion of points. A systematic way to carry out such “categorical pointwise” proofs is shown in this chapter, which is then used to state and prove rules that manipulate the mins selector. These mins rules both show the applicability of this extension to BdM’s and prepare the field for the later manipulation of the representatives of closure problem. It is worth mentioning that most graph problems seem to involve a good deal of the powerset and product combinators that motivated the introduction of points in the first place.

4.1 Using Points

The motivating model of allegory theory is that of sets and relations, yet many other models are accepted by the axioms of a “raw” allegory. Further assumptions, e.g. the existence of tabulations, narrow down the spectrum of models closer to set-theoretic relations. An important feature of relations, being defined as subsets of cartesian products in set theory, is that of being built up from (pairs of) elements. The corresponding notion to such elements in lattice theory is that of an atom, an immediate succesor of bottom. And a lattice is said to be atomic if every lattice member can be built up from atoms. We shall assume the allegory is atomic, meaning that each homset is an atomic lattice. Atoms take the form of a point after the converse of a point. We then have that every relation R satisfies

R = (⋃ x, y : x, y points ∧ x·y^{∘} ⊆ R : x·y^{∘})

Note that x·y^{∘} ⊆ R corresponds to the intuitive appeals to set theory we have been doing of the form x (R) y. Also note that, by shunting of functions, it is equivalent to x ⊆ R· y which, under the right-to-left “operational” interpretation attached to relations, can be read as “x is a possible output of R for input y”. We now count with the following alternatives to prove inclusion of relations:

R ⊆ S ≡ (∀ y : y point : R · y ⊆ S · y)
≡ (∀ x, y : x, y points : x ⊆ R · y ⇒ x ⊆ S · y)

Further rules follow. For example, to manipulate composition, functions and coreflexives, we have

x ⊆ R · S · y ≡ (∃ z : z point : x ⊆ R · z ∧ z ⊆ S · y)
x ⊆ f · y ≡ x = f · y
x ⊆ C · y ≡ x = y ∧ x ⊆ C · x

Recall the modelling-predicates role of coreflexives. We shall denote by C. x the satisfaction of x by C, meaning x ⊆ C·x.

Everything else we shall need to manipulate relations through points will fall down naturally from the rules above and predicate calculus. As an example, we show that R · C ⊆ S can be proved by showing that (C. x ⇒ R·x ⊆ S ·x) for every point x:

R · C ⊆ S
≡ { points-inclusion }
(∀y, x : y ⊆ R · C · x ⇒ y ⊆ S · x)
≡ { points-composition }
(∀y, x : (∃z : y ⊆ R · z ∧ z ⊆ C · x) ⇒ y ⊆ S · x)
≡ { points-coreflexive, predicate calculus }
(∀y, x : y ⊆ R · x ∧ C. x ⇒ y ⊆ S · x)
≡ { predicate calculus }
(∀x : C. x ⇒ (∀y : y ⊆ R · x ⇒ y ⊆ S · x))
≡ { points-inclusion }
(∀x : C. x ⇒ R · x ⊆ S · x)

Power-Products

It was mentioned that points seem to be particularly useful when powersets and products are involved. For powersets, due to the power-transpose isomorphism Fun(PX, 1) ≅ Rel(X, 1), elements of either homset represent points of PX; uppercase and lowercase letters will be used to implicitly denote the correspondence a = ΛA. The same goes to the product isomorphism Fun(X ×Y, 1) ≅ Fun(X, 1) × Fun(Y, 1), with the convention a = ⟨a_{1}, a_{2}⟩.

For later convenience, new notation is introduced to denote points of products of powerset types, e.g. (PX × PY). We shall denote by ⟨|A, B ⟩| the relation ⟨ΛA, ΛB⟩. A kind of right-associativity will be assumed when more than two components are needed, this meaning that ⟨|A, B, C ⟩| denotes ⟨ΛA, ⟨ΛB, ΛC⟩⟩. Consistently, it will sometimes be used even for a single component, ⟨|A ⟩| meaning ΛA.

4.2 Mins Calculus

Recall the formal definition of mins given at the end of chapter 3:

mins (Q, R) ˆ= uniq Q · thin (Q ∩ R) where

uniq S = id ∩ ∈\(S ⇒ id)/∋
thin S = ∈\∈ ∩ (∋·S)/∋

Let us show the pointwise reading of these relations. Bear in mind the naming convention whereby sets are modelled by relations A : X ← 1 that are in a oneto-one correspondence with powerset points a = ΛA : PX ← 1. We manipulate in detail the thin case:

b ⊆ thin S · a
≡ { shunting of functions, definition of thin }
b · a^{∘} ⊆ ∈\∈ ∩ (∋ · S)/∋
≡ { meet, division }
∈· b · a^{∘} ⊆ ∈ ∧ b · a^{∘}·∋ ⊆ ∋ · S
≡ { shunting of functions }
∈· b ⊆ ∈· a ∧ a^{∘}·∋ ⊆ b^{∘}·∋· S
≡ { naming convention, power-transpose, converse }
B ⊆ A ∧ A ⊆ S^{∘}·B

Analogously, we can also get the pointwise description of uniq and mins:

b ⊆ thin S · a ≡ B ⊆ A ∧ A ⊆ S^{∘}·B
uniq Q. a ≡ A·A^{∘}∩ Q ⊆ id
b ⊆ mins (Q, R) · a ≡ \{ \begin{matrix}B·B^{∘}∩ Q ⊆ id ∧ \\ B ⊆ A ∧ A ⊆ (Q ∩ R)^{∘}·B \end{matrix}

Now for the rules.

Mins/Cup The function cup = Λ(∈ · outl ∪ ∈ · outr) returns the union of its two input sets. We aim to analyse the interaction of mins and cup. A way of choosing representatives from the union of two sets is to initially get them solely from the first one and then get the rest from the other only for classes not yet represented. It is safe to do so only if classes present in both sets have a minimum (of the union) in the first. A corresponding point-free statement, but with a stronger precondition, is:

mins · cup ⊇ cup · mins^{2} · (id × drop) · δ · p?

where

drop Q = diff · (EQ × id)
diff = Λ(∈· outr − ∈· outl)
δ is the obvious natural

transformation typed X × (X × Y) ↩ X × Y

p? = step (∈\(Q ⇒ R)/∋)
step S = id ∩ outl^{∘}· S · outr

For this rule, not only a proof using points is more effective, but also the actual statement gets more readable. Application to the (pair of sets) point ⟨|A_{1}, A_{2} ⟩| and some juggling transforms it to

\begin{matrix}mins · Λ(A_{1} ∪ A_{2}) ⊇ cup · ⟨mins · ΛA_{1}, mins · Λ(A_{2} − Q·A_{1})⟩ \\ provided A_{1}·A_{2}^{∘} ∩ Q ⊆ R \end{matrix} \} (4.1)

Let us now proceed with its proof. We will show that

(∀ b : b ⊆ LHS ⇐ b ⊆ RHS)

The antecedent is first manipulated thus

b ⊆ RHS
≡ { points-composition }
(∃ c : b ⊆ cup·c ∧ c ⊆ ⟨ mins · ΛA_{1} , mins · Λ(A_{2} − Q·A_{1}) ⟩)
≡ { naming convention, cup property, products }
(∃ C_{1}, C_{2} : ΛB ⊆ Λ(C_{1} ∪ C_{2})

∧ ΛC_{1} ⊆ mins · ΛA_{1} ∧ ΛC_{2} ⊆ mins · Λ(A_{2} − Q·A_{1}))

≡ { inclusion/equality of functions, power-transpose, pointwise mins }
(∃ C_{1}, C_{2} : B = C_{1} ∪ C_{2}  (i)
∧ C_{1}·C_{1}^{∘} ∩ Q ⊆ id ∧ C_{2}·C_{2}^{∘} ∩ Q ⊆ id  (ii)
∧ C_{1} ⊆ A_{1} ∧ A_{1} ⊆ (Q ∩ R)^{∘}·C_{1}  (iii)
∧ C_{2} ⊆ A_{2} − Q·A_{1} ∧ A_{2} − Q·A_{1} ⊆ (Q ∩ R)^{∘}·C_{2}) (iv)

Assuming it, we prove the consequent, which reads

B·B^{∘} ∩ Q ⊆ id ∧ B ⊆ A_{1} ∪ A_{2} ∧ A_{1} ∪ A_{2} ⊆ (Q ∩ R)^{∘}·B

We proceed with the first conjunct

B·B^{∘} ∩ Q

= { (i), distribution }

(C_{1}·C_{1}^{∘} ∩ Q) ∪ (C_{1}·C_{2}^{∘} ∩ Q) ∪ (C_{2}·C_{1}^{∘} ∩ Q) ∪ (C_{2}·C_{2}^{∘} ∩ Q)

⊆ { (ii), claim: second and third operands equal ∅ }

id

It suffices to prove either part of the claim since they are equivalent (take converses and note that Q is symmetric):

C_{2}·C_{1}^{∘} ∩ Q

⊆ { modular law }
(C_{2} ∩ Q·C_{1}) · C_{1}^{∘}
⊆ { first conjuncts of (iii) and (iv), substraction }
(\overline{Q·A_{1}} ∩ Q·A_{1}) · C_{1}^{∘}
= { complements }
∅

For the second conjunct, we argue

B

⊆ { (i), first conjuncts of (iii) and (iv) }
A_{1} ∪ (A_{2} − Q·A_{1})
⊆ { substraction }
A_{1} ∪ A_{2}

The third and last conjunct is the key one that depends on the proviso of the rule:

A_{1} ∪ A_{2}
= { complements }
A_{1} ∪ (A_{2} ∩ Q·A_{1}) ∪ (A_{2} − Q·A_{1})
⊆ { modular law }
A_{1} ∪ (A_{2}·A_{1}^{∘} ∩ Q)·A_{1} ∪ (A_{2} − Q·A_{1})
⊆ { the proviso is equivalent to A_{2}·A_{1}^{∘} ∩ Q ⊆ (Q ∩ R)^{∘} }
A_{1} ∪ (Q ∩ R)^{∘}·A_{1} ∪ (A_{2} − Q·A_{1})
⊆ { second conjuncts of (iii) and (iv), transitivity of (Q ∩ R)^{∘} }
(Q ∩ R)^{∘}·C_{1} ∪ (Q ∩ R)^{∘}·C_{2}
= { distribution, (i) }
(Q ∩ R)^{∘}·B

We have completed the proof.

A corresponding proof in the point-free style turned out to be more than twice the length of the one above. The core of the matter, though, is that, in the same way that the statement of the rule is less readable without points, the proof was not very easy to work out. The one shown here is far more symbol-guided.

Mins/Uniq A set satisfying uniq has itself, and only itself, as a minimumrepresentatives subset. The point-free rule reads

mins · uniq = uniq

and translates to

mins · a = a  provided uniq.a  (4.2)

We prove it as follows:

b ⊆ mins · a
≡ { pointwise mins }
B·B^{∘}∩ Q ⊆ id ∧ B ⊆ A ∧ A ⊆ (Q ∩ R)^{∘}·B  (*)
≡ { claim }
B = A
≡ { power-transpose, inclusion/equality of functions }
b ⊆ a

The (⇐) part of the claim follows directly from the proviso and reflexivity of (Q ∩ R)^{∘}. For (⇒) we only need to prove A ⊆ B:

A
= { third conjunct of (*), meet }
A ∩ (Q ∩ R)^{∘}·B
⊆ { meet, Q symmetric }
A ∩ Q·B
⊆ { modular law }
(A·B^{∘} ∩ Q)·B
⊆ { second conjunct of (*) }
(A·A^{∘} ∩ Q)·B
⊆ { proviso }
B

Note that we have proved thin · uniq = uniq as well, since the first conjunct of (*) was never used.

Mins/Empty and Mins/Unitary Particular instances of sets satisfying uniq are the empty set and any singleton set. Those facts will be useful in the next chapter. For empty = Λ∅ and τ = Λid, we have

mins · empty = empty  (4.3)
mins · τ = τ  (4.4)

4.3 Discussion

I wonder whether the assumption of atomicity is really necessary in the presence of tabulations. The only purpose it served was to make the point-inclusion and point-composition laws valid. I doubt atomicity follows from the existence of tabulations, but it would suffice that it implies the other above-mentioned laws.

There is yet another aspect of points: definition of relations through their pointwise extension. Given an indeterminate x typed Fun(A, 1) and an expression θ(x) in Rel(B, 1), there exists a unique relation R : B ← A such that R · x = θ(x) for all x. This allows us to define relations by means of their application to points, not having to give a closed point-free expression for them.

5 Main Derivation

We now present the core of the calculation of algorithmic solutions to the minimum-representatives of closure problem:

P = mins(Q, R) · ΛS^{∗}

In order to successfully promote the mins selector into the generator, the closure operation is first suitably generalised. Following that, a key property that relates the thinning part of mins to the generalised closure is stated. All the properties gathered to this point are then put to use deriving a recursion equation satisfied by P (or, rather, a generalisation of it).

5.1 Generalising Closure

Recall that, by definition, S^{∗} is the least preorder that contains S. And that it is the least solution of the equation S^{∗} = (μX : id ∪ S·X), which is a particular case of the more general result

S^{∗}·A = (μX : A ∪ S·X)  (5.1)

If A is a powerset point, i.e. a set, S^{∗}·A can be thought of as the right-to-left image through S^{∗} of A. For the applications we have in mind, algorithms that compute P, the above generalisation will not lead to a terminating recursion. Termination will be ensured by finiteness of the set of equivalence classes of Q. Hence, we should somehow take account of Q-classes that “need not be generated anymore”. Accordingly, we choose to generalise (5.1) as follows

Θ(B, A) ˆ= (μX : A ∪ (S·X − Q·B))

The rest of the section is devoted to state and prove properties of Θ which will be put to use later.

We start out with equations that will allow us to embed P into a suitable generalisation and afterwards carry out a recursion analysis:

Θ(∅, A) = S^{∗}·A  (5.2)
Θ(B, ∅) = ∅  (5.3)
Θ(B, A_{1} ∪ A_{2}) = A_{1} ∪ Θ(B, A_{2} ∪ (S·A_{1} − Q·B))  (5.4)

(5.2) follows from ∅ being a zero of composition and right-unit of substraction, and equation (5.1). Since ∅ is also the unit of join and a left-zero of substraction, note for (5.3) that ∅ is a solution of the recursion equation involved and therefore the least solution. Finally, the rolling rule of the μ-calculus

(μX : ϕ(ψX)) = ϕ(μX : ψ(ϕX))

is used to prove (5.4):

Θ(B, A_{1} ∪ A_{2})
= { definition of Θ }
(μX : A_{1} ∪ A_{2} ∪ (S·X − Q·B))
= { rolling with ϕX := A_{1} ∪ X, ψX := A_{2} ∪ (S·X − Q·B) }
A_{1} ∪ (μX : A_{2} ∪ (S·(A_{1} ∪ X) − Q·B))
= { distribution }
A_{1} ∪ (μX : A_{2} ∪ (S·A_{1} − Q·B) ∪ (S·X − Q·B))
= { definition of Θ }
A_{1} ∪ Θ(B, A_{2} ∪ (S·A_{1} − Q·B))

We shall also need the following property:

Θ(B, A) ⊆ S^{∗}·A  (5.5)

which follows from X − Y ⊆ X, monotonicity of the μ-operator and (5.1). To close this list of properties, we point out that Θ is anti-monotonic on its first argument and monotonic on its second.

Thinning the Closure

A crucial property of Θ in connection to the thinning part of the mins selector follows. Such property relies on the parameters Q, R, S of our problem satisfying two conditions:

S ⊆ R^{∘}  (Hyp.1)
S · (Q ∩ R)^{∘} ⊆ (Q ∩ R)^{∘} · S  (Hyp.2)

The first equation says that the generating relation S does not decrease the R-cost. Therefore, minimum-representatives are likely to be produced sooner rather than later. The second equation states the monotonicity of S on the converse of the thinning mediator (Q ∩ R)^{∘}. This permits the disposal of some intermediate candidates for the presence of others. If one has at some stage x and y such that x (Q ∩ R)^{∘} y, i.e., they are equivalent and y is at least as good as x, then for any element x′ generated from x there will be a y′ generated by y equivalent to and at least as good as x′. Therefore, x can be safely disposed of. These two assumptions allow the (closure-)generating process to be pruned considerably.

The thin/Θ rule formalises the pruning we shall make use of. It reads

\begin{matrix}thin (Q ∩ R) · Λ (Θ(B, A) − Q·C) ⊇ Λ Θ(B ∪ C, A − Q·C) \\ provided & \begin{matrix}C·A^{∘} ⊆ R \\ S·C − Q·B ⊆ A \end{matrix} \end{matrix} \} (5.6)

Its proof can be found in appendix A.

Note that, from (Hyp.1), we have in R^{∘} a preorder that contains S. Therefore, by definition of closure, S^{∗} ⊆ R^{∘} and (5.5) then gives Θ(B, A) ⊆ R^{∘} ·A. It follows that, by transitivity of R,

C·A^{∘} ⊆ R ⇒ C·Θ(B, A)^{∘} ⊆ R  (5.7)

Finally, we shall also use the fact that thin is monotonic in the sense that A ⊆ B implies thin ·ΛA ⊆ thin ·ΛB.

5.2 Main Derivation

We now manipulate the whole of our abstract problem P, first embedding it into an adequate generalisation and then deriving a recursion equation for the latter. Recall the hypotheses (Hyp.1) and (Hyp.2), which act as provisos for the derivation to come.

The calculation makes use of pointwise reasoning. We take a point a and proceed thus with the embedding

P ·a
= { definition of P, power-transpose absorption }
mins · Λ(S^{∗}·a)
= { Θ embeds closure (5.2) }
mins · Λ Θ(∅, a)
= { introduce P′(B, A) := mins · Λ Θ(B, A) }
P′(∅, a)

In the third step two things were actually introduced: a relation P′ satisfying P′ · ⟨|B, A ⟩| = mins · Λ Θ(B, A) and notation P′(B, A) := P′ · ⟨|B, A ⟩|. A case analysis (on A) is now conducted for P′. First, the empty set case. By Θ property (5.3) and mins/empty rule (4.3), we have

P′(B, ∅) = mins · Λ Θ(B, ∅) = mins · Λ∅ = Λ∅

Second, the case of A being the union of two sets. This case includes the first one, so further refinement in later steps will be needed to eliminate the non-determinism. For the time being, it is kept simple. We use a heuristic analoguous to the one used for the mins/cup rule. From the input set (A = A_{1} ∪ A_{2}) a part is processed first (A_{1}), taking representatives of it, and then carrying on with the rest. Conditions under which it is valid to do so will be calculated. So, let us take A′_{1} such that ΛA′_{1} ⊆ mins · ΛA_{1} and then proceed:

P′(B, A_{1} ∪ A_{2})

= { definition of P′ }

mins · Λ Θ(B, A_{1} ∪ A_{2})

⊇ { A_{1} ⊇ A′_{1} by assumption, monotonicity of Θ and thin }

mins · Λ Θ(B, A′_{1} ∪ A_{2})

= { Θ property (5.4) }

mins · Λ ( A′_{1} ∪ Θ(B, A_{2} ∪ (S·A′_{1} − Q·B)) )

⊇ \{ \begin{matrix}mins/cup rule (4.1) \\ • assumption: proviso of the rule \end{matrix}\}

cup · ⟨ mins · ΛA′_{1} , mins · Λ ( Θ(B, A_{2} ∪ (S·A′_{1} − Q·B)) − Q·A′_{1} ) ⟩

⊇ \{ \begin{matrix}mins/uniq rule (4.2), A′_{1} satisfies uniq by assumption; \\ thin/Θ rule (5.6), thin ·X ⊇ Y ⇒ mins ·X ⊇ mins ·Y \\ • assumption: provisos of the rule \end{matrix} \}

cup · ⟨ ΛA′_{1} , mins · Λ Θ(B ∪ A′_{1}, (A_{2} ∪ (S·A′_{1} − Q·B)) − Q·A′_{1}) ⟩

= { definition of P′, distribution }

cup · ⟨ ΛA′_{1} , P′(B ∪ A′_{1}, (A_{2} − Q · A′_{1}) ∪ (S·A′_{1} − Q·B − Q · A′_{1})) ⟩

The additional assumptions made are now collected and analysed. These are

A′_{1} · Θ(B, A_{2} ∪ (S·A′_{1} − Q·B))^{∘} ∩ Q ⊆ R  (i)
A′_{1} · (A_{2} ∪ (S·A′_{1} − Q·B))^{∘} ⊆ R  (ii)
S·A′_{1} − Q·B ⊆ A_{2} ∪ (S·A′_{1} − Q·B)  (iii)

First note that (i) follows from (ii), by an appeal to (5.7) and universal property of meet. And (iii) is true for universal property of join. So we are left only with (ii), but it can be refined to a condition both simpler and only in terms of the actual input (i.e. not involving A′_{1}):

A′_{1} · (A_{2} ∪ (S·A′_{1} − Q·B))^{∘} ⊆ R
⇐ { substraction }
A′_{1} · (A_{2} ∪ S·A′_{1})^{∘} ⊆ R
⇐ { R reflexive, (Hyp.1) }
A′_{1} · (R^{∘}·A_{2} ∪ R^{∘}·A′_{1})^{∘} ⊆ R
⇐ { distribution, converse }
A′_{1} · (A_{2} ∪ A′_{1})^{∘} · R ⊆ R
⇐ { R transitive, monotonicity }
A′_{1} · (A_{2} ∪ A′_{1})^{∘} ⊆ R
⇐ { A′_{1} ⊆ A_{1} by assumption }
A_{1} · (A_{1} ∪ A_{2})^{∘} ⊆ R  (ii’)

In order to state the recursion (in)equation derived above, we now move to the point-free space. The results translate to

P′ · (id × empty) = empty!
P′ · (id × cup) ⊇ cup · (id × P′) · combine · (id × (mins × id) · p?)

where combine and p? are, respectively, the function and coreflexive defined as

combine · ⟨|B, A_{1}, A_{2} ⟩| = ⟨|A_{1}, B ∪ A_{1}, (A_{2} − Q·A_{1}) ∪ (S·A_{1} − Q·B − Q·A_{1}) ⟩|
p?.⟨|A_{1}, A_{2} ⟩| ≡ (ii’)

Now note that

P′

⊇ { above, shunting of functions, join }

empty! · (id × empty^{∘}) ∪

cup · (id × P′) · combine · (id × (mins × id) · p? · cup^{∘})

= { coproducts }

[ empty! , cup ] · (id + id × P′) ·

[ (id × empty) , (combine · (id × (mins × id) · p? · cup^{∘}))^{∘}]^{∘}

= { introducing suitable function g, functor F and relation W }

g · FP′ · W

and that

P
= { point-free version of the embedding }
P′ · ⟨ empty! , id ⟩
= { introduce function h }
P′ · h
⊇ { above inequation for P′, Knaster-Tarski }
(μX : g · FX · W) · h

The core of the calculation has been completed.

5.3 Towards Functional Refinements

In the relational-algebraic approach to derivation of algorithms one starts with a relational, and so potentially non-deterministic, specification P and aims to refine it to a (possibly partial) function, thus deterministic, p. The refinement must respect the original specification, which is formalised through inclusion, and should also work for the same set of inputs. A domain-preserving refinement relation can be defined as

T ⪰ T′ ˆ= T ⊇ T′ ∧ dom T = dom T′.

The domain of a relation R is the coreflexive dom R = id ∩ R^{∘}·R and, dually, its range is ran R = dom R^{∘}. What we want for a specification P are implementations^{3} p of it in the sense that

P is implemented by p ˆ= P ⪰ p ∧ p is simple.

For the representatives of closure problem P we have already derived that P ⊇ (μX : g · FX · W) · h. Equality does not hold in general, so some nodeterminism has been swept away. Yet not all of it since W is not a simple relation. If we are to hope this is leading us to an implementation, we need to check the domain has been preserved so far. For the subsequent domains analysis we impose a new restriction on the mediator parameter R. It is assumed to be well-founded:

dom ∈ ⊆ dom (min R)  (Hyp.3)

Under this new assumption P is entire and so we need entire implementations, i.e. (total) functions. To analyse the domain-preservation, domains of recursion equations need be reasoned about. Inductiveness is the tool we shall use for that purpose.

A relation T is inductive if there are no infinite chains a_{0}, a_{1}, a_{2},… such that (∀i : i ≥ 0 : a_{i+1}T a_{i}).^{4} For a monotonic functor F, T is said to be Finductive if δ · T is inductive, where δ is the membership relation of F (see [23]). Inductiveness is conventionally used to prove termination of programs. In a relational framework, termination is expressed through domains of recursion equations, which we formalise thus:

Proposition 5.8 Let R, S be relations and C a coreflexive such that R is entire, C ⊆ dom (FC · S) and S is F-inductive. Then C ⊆ dom (μX : R · FX · S).

The proof of this result is in appendix B.

We now have an informal look at the F-inductiveness of W. We do so taking an input point to the recursion and finding out what the input is for the next recursive level, seeing what is “below” such point under δ · W:

3This is a very loose notion of implementation, since it does not refer to any computational mechanisms or notions of what is executable. It must be understood in such a general sense.

4This is actually the (informal) characterisation of well-founded relations. However, inductiveness and well-foundedness are equivalent in the presence of negation. See [3, 21] for a very good calculational presentation of these concepts. We reserve the term well-founded for the (related) concept expressed in (Hyp.3).

δ · W · ⟨|B, A ⟩|
= \{ \begin{matrix}membership relations: δF = [ ∅, outr ], \\ definition of W, coproducts \end{matrix} \}
outr · combine · (id × (mins × id) · p? · cup^{∘}) · ⟨|B, A ⟩|

⊇ \{ \begin{matrix}let A_{1}, A_{2} be such that \\ – ⟨|A_{1}, A_{2} ⟩| ⊆ cup^{∘}· ⟨|A ⟩| (≡ (A_{1} ∪ A_{2} = A)) \\ – p?.⟨|A_{1}, A_{2} ⟩| \\ let A′_{1} be such that \\ – ⟨|A′_{1} ⟩| ⊆ mins · ⟨|A_{1} ⟩| \end{matrix} \}

outr · combine · ⟨|B, A′_{1}, A_{2} ⟩|
= { definition of combine, products }
⟨|B ∪ A′_{1}, (A_{2} − Q·A′_{1}) ∪ (S·A′_{1} − Q·B − Q·A′_{1}) ⟩|

Hence, ⟨|B ∪ A′_{1}, … ⟩| ⊆ δ · W · ⟨|B, A ⟩| provided A′_{1} can be extracted from A under the above restrictions. We focus on the first component of the pair and note it seems likely to grow. However, we have to show that it does grow and that such progress is bounded.

First of all, we need A′_{1} to be non-empty. This is solved refining W to W′ by restricting p? to p? · (dom ∈×id). Now, if we knew A′_{1} is not contained in B the growing would be guaranteed. But this would not ensure termination yet since such growing is not taking place within a finite set. (In the instance of minimum paths, the set of paths is, in general, infinite.) However, recall the purpose of that first component is to record the Q-equivalence classes representatives of which have already been sent to the output. Therefore, one would expect A′_{1} to be recording new outputted classes, that is, not to share classes with B. This is indeed the case, since invariantly A (from which A′_{1} was extracted) and B do not share Q-classes. Define the Q-disjoint coreflexive as

disj Q ˆ= step (∈\\overline{Q}/∋),

which pointwisely reads

disj Q.⟨|B, A ⟩| ≡ B·A^{∘} ⊆ \overline{Q}
≡ B·A^{∘} ∩ Q = ∅.

We claim that disj Q is an invariant of the refined algorithm. A brief review of the concept of invariants in this framework follows.

Invariants

Invariants are important in the development of imperative programs, specifically, in the development of loops. An invariant is often just a generalisation of the postcondition to be achieved, that must be set before entering the loop-to-be and maintained after each iteration of the loop-body-to-be. The generalisation must be carefully chosen in order to serve such purpose. In most of the work done in relational derivation of functional algorithms, the concept of invariant seems to disappear. In our specific development of the representatives problem, the success of the calculation was due to the choice of generalisation of the closure operator (definition of Θ in section 5.1). This generalisation of (part of) the specification to get the derivation rolling can be seen as the parallel of the imperative choice of a postcondition-generalised invariant to develop a loop.

Nevertheless, invariants turned out to be needed towards the end of our development: to prove domain-preservation. If a entire specification is refined to a least fixed point, the latter is expected to be entire. A practical result previously used within BdM’s calculus to show certain refinements preserve domains is the following: (μX : R · FX · S) is entire if R and S are entire and S is F-inductive. In our representatives example, we hit a similar recursion equation where S is not F-inductive unless restricted to certain inputs. But the refinement is of the form (μX : R · FX · S) · T, and T delivers only the kind of outputs that guarantee S to terminate. I.e., T delivers results within a certain coreflexive C, S will guarantee that C keeps holding when entering the next recursion level, and the recursion will terminate due to S·C being F-inductive. Comparing again to the imperative approach, we are in the presence of an invariant the purpose of which is showing the variant decreases, rather than showing the output of the computation is the desired one. In Bird’s imperative presentation of the representatives problem [9], both kinds of invariants are used.

Formally, a coreflexive C is said to be F-invariant under S if S·C ⊆ FC ·S. Also, C is said to be set by T if ran T ⊆ C (equivalent to T = C ·T). We now proceed with two small results.

Proposition 5.9 If C is F-invariant under S, then

(μX : R · FX · S) · C = (μX : R · FX · S · C)

The proof is in appendix B. An immediate corollary:

Proposition 5.10 If C is both F-invariant under S and set by T, then

(μX : R · FX · S) · T = (μX : R · FX · S · C) · T

Now, the right proposition to prove our refinements are domain-preserving.

Proposition 5.11 Let R, S, T be entire relations and C be a coreflexive. Suppose C is both F-invariant under S and set by T, and such that S · C is Finductive. Then (μX : R · FX · S) · T is entire.

We argue

(μX : R · FX · S) · T entire

≡ { proposition (5.10) }

(μX : R · FX · S · C) · T entire

⇐ { T entire, domains }

ran T ⊆ dom (μX : R · FX · S · C)

⇐ { C is set by T }

C ⊆ dom (μX : R · FX · S · C)

⇐ { proposition (5.8), R entire, S · C F-inductive }

C ⊆ dom (FC · S · C)

⇐ { C F-invariant under S, duplicity of coreflexives }

C ⊆ dom (S · C)

≡ { S entire }

true

A last property of invariants: they are inherited through inclusion. That is, if S′ ⊆ S and C is F-invariant under S, then C is also F-invariant under S′.

Getting back again to the representatives algorithm, from the main derivation and the last refinement to W, it follows that

P ⊇ (μX : g · FX · W′) · h

We now claim that (i) disj Q is F-invariant under W′ and set by h, (ii) W′ is entire, and (iii) W′ · disj Q is F-inductive. Since g and h are functions, thus entire, it follows from proposition (5.11) that

P ⪰ (μX : g · FX · W′) · h

The proof of (i) is omitted. For (ii), a close look at W′ shows that the empty set gets injected to the left and all non-empty sets to the right. The feasibility of dividing sets in two parts satisfying p? · (dom ∈ × id) is guaranteed by (Hyp.3). The proof of (iii) is also omitted, but we point out that requires yet another condition:

The quotient set of Q is finite  (Hyp.4)

5.4 Two Particular Implementations

We aim to get two particular kinds of implementation for our abstract problem, which we name unitary and levelled. Note that all the non-determinism left is in the subexpression (mins × id) · p? · (dom ∈ × id) · cup^{∘} of W′. It says: split (cup^{∘}) the input set, extracting a non-empty (dom ∈) subset the elements of which are R-minima (p?), take representatives (mins) of those minima and then carry on. Roughly, the unitary and levelled implementations will respectively do so thus:

\begin{matrix}\{a\} ∪ x & ⇝ & \{a\} , & x \\ x & ⇝ & x , & ∅ \end{matrix}

Recall the class of graph problems we abstracted P from in chapter 3. The unitary solution provides Dijkstra’s minimum paths algorithm and both depthfirst and breadth-first reachability algorithms. From the levelled solution, the breadth-first search and unweighted shortest paths algorithms that work by levels are obtained. Conditions that suffice to get an implementation, i.e. to adequately refine W′, follow:

Let split be a simple relation and q? be a coreflexive such that

split · q? ⊆ (mins × id) · p? · (dom ∈ × id) · cup^{∘}  (i)
dom split = dom ∈  (ii)
combine · split · q? ⊆ (id × q?) · combine · split  (iii)
h ⊆ q? · h  (iv)

Then P is implemented by M ·h where

M = (μX : g · FX · V)
V = [ (id × empty) , (combine · split)^{∘}]^{∘}

Three things need be shown: P ⊇ M ·h, dom P = dom (M ·h), and that M ·h is simple.

First note that (i) and (iii) imply, respectively, (i’) V · q? ⊆ W′ and (iii’) V · q? ⊆ Fq? · V. Then

M · h
= { (iii’), (iv), proposition (5.10) }
(μX : g · FX · V · q?) · h
⊆ { (i’) }
(μX : g · FX · W′) · h
⊆ { last section }
P

Next, note that, by (i’), V ·q? inherits from W′ its two properties in relation to disj Q: having it as F-invariant and being F-inductive when restricted to it. Therefore, (q? · disj Q) is F-invariant under V and V · (q? · disj Q) is F-inductive.

And V is entire by (ii). We have got the provisos of proposition (5.11) that show M ·h to be entire. Finally, M · h simple follows from split being simple.

Now for the two solutions...

Unitary Split Let getmin be a simple relation such that

getmin ⊆ step (τ · min R) · cup^{∘}

Then split, q? := getmin, id provide an implementation as required above.

Full Split (Levelled Solution) Let r be a function such that r ⊆ mins (Q, Π) and define getlevel to be

getlevel = ⟨ r, empty! ⟩ · dom ∈

Then split, q? := getlevel, unif R where unif R is the coreflexive denoting sets of elements with uniform R-cost, satisfy the provisos to get an implementation. For unif R to be invariant an extra condition must be satisfied:

S · R · S^{∘} ⊆ R  (Hyp.Extra)

To implement the derived algorithms in a functional language like Orwell or Gofer, the sets involved would have to be data-refined to, for instance, lists. The generating relation S should be required to spawn finite sets in order to fulfill this last step of the development:

ran ΛS ⊆ finite?  (Hyp.5)

All the instance problems of chapter 3 satisfy the five conditions required for the unitary implementation. The special requirement (Hyp.Extra) for a levelled solution is met by all but the first –minimum paths over a weighted graph–. For the rooted trees problem, it should be proved that the derived algorithms establish the additional post-condition needed.

6 Conclusions

We have specified the abstract problem of finding minimum-representatives of closure, and identified a few graph problems as instances of it. Also, algorithms to compute such representatives have been derived, requiring some conditions on the parameters of the specification. The task of obtaining algorithmic solutions for instance problems is reduced to verify the provisos are met by the particular parameters. This approach to algorithm design compares positively to other conventional approaches (see e.g. [16, 29, 47, 48]) both for its algebraic nature and the higher level of abstraction used. Algebraic presentations of algorithm design facilitates the visualisation of the points where crucial design decision are made. The higher level of abstraction permits the solution of several, sometimes seemingly disparate, problems all at once. The relational calculus of Bird and de Moor provided an adequate algebraic framework to carry out the development. However, its point-free nature sometimes limited the clarity of expression. Categorical points provided a smooth way of extending the calculus to ease such difficulty. Also, a few propositions regarding the use of invariants to reason about termination and domain-preservation of refinements were stated and proved.

The graph problems presented here are clearly related to each other. Some conventional presentations of graph algorithmics actually call the attention to the relationship between them; however, this is often done at the algorithm level rather than at the specification level, which we believe is the right place to do so. In chapter 3 the specification of each problem was developed separately, without showing much of the conceptual link between them. The missing point is that all can be regarded as path problems. The following equations hold for the generators given (gen i denotes the generator of problem 3.i):

gen2 = ([ wrap , cons · (to × id) ]) · gen1
gen3 = ([ id , to · outl ]) · gen1
gen4 = ([ newe , orige · outl ]) · gen1

This is much in the same spirit of [42], where the original abstract specification is already bound to paths. Since the representatives of closure problem in itself does not deal with paths, its applicability to problems of other kinds is not restricted beforehand. Oege de Moor has suggested its application to a busstops problems drawn from the operations research field.

Others have studied this same class of graph problems. Backhouse et al have done so using regular algebra of matrices, by means of a correspondence between graphs and adjacency matrices [5]. Möller and Russling have tackled it using another relational framework [38, 42]; however, the weighted graph case is not considered and only breadth-first solutions are shown. Clenaghan showed that the two aforementioned approaches can be formally unified using a dynamic algebra framework [15].

To what extent graph algorithms can be classified, according to the design strategies that govern their construction, is an important goal to pursue. The present work encourages the undertaking of more research in such direction using the relational calculus. For instance, the connection to depth-first search can be used to explore the variety of algorithms based on it. King and Launchbury, in [28], give functional implementations of some DFS-based algorithms. They show how the change of presentation ease the task of reasoning about such programs, compared to traditional imperative views. However, no derivation of the algorithms are presented.

References

[1] C.J. Aarts. Galois connections presented calculationally. Graduating Dissertation, Eindhoven University of Technology, July 1992.

[2] C.J. Aarts, R.C. Backhouse, P. Hoogendijk, E. Voermans, and J. van der Woude. A relational theory of datatypes. Working document, December 1992. Available via anonymous ftp from ftp.win.tue.nl in directory

pub/math.prog.construction.

[3] R.C. Backhouse and H. Doornbos. Mathematical induction made calculational. CS report 94-16, Eindhoven University of Technology, March 1994. Submitted for publication.

[4] R.C. Backhouse, H. Doornbos, and P. Hoogendijk. A class of commuting relators. Department of Mathematics and Computing Science, Eindhoven University of Technology, September 1992. Available via anonymous ftp

from ftp.win.tue.nl in directory pub/math.prog.construction.

[5] R.C. Backhouse, J.P.H.W. van den Eijnde, and A.J.M. van Gasteren. Calculating path algorithms. Science of Computer Programming, 22(1-2), April 1994.

[6] J. Backus. Can programming be liberated from the von neumann style? a functional style and its algebra of programs. Communications of the ACM, 21(8), August 1978.

[7] M. Barr and C. Wells. Category Theory for Computing Science. Prentice-Hall, 2nd edition, 1995.

[8] R.S. Bird. A calculus of functions for program derivation. In D.A. Turner, editor, Research Topics in Functional Programming. Addison-Wesley, 1990.

[9] R.S. Bird. On computing representatives. Oxford University Computing Laboratory, Programming Research Group, 1995.

[10] R.S. Bird and O. de Moor. Between dynamic programming and greedy: Data compression. Oxford University Computing Laboratory, Programming Research Group, 1992.

[11] R.S. Bird and O. de Moor. From dynamic programming to greedy algorithms. In B. Möller, H. Partsch, and S. Schumann, editors, State-of-the-Art Report on Formal Program Development. Springer-Verlag LNCS 755, 1992.

[12] R.S. Bird and O. de Moor. Solving optimisation problems with catamorphisms. In R.S. Bird, C.C. Morgan, and J.C.P. Woodcock, editors, Mathematics of Program Construction. Springer-Verlag LNCS 669, 1992.

[13] R.S. Bird and O. de Moor. The Algebra of Programming. Prentice-Hall, to appear 1996.

[14] R.S. Bird, P. Hoogendijk, and O. de Moor. Generic programming with relations and functors. Submitted to Journal of Functional Programming, 1993.

[15] K. Clenaghan. Calculational graph algorithmics: Reconciling two approaches with dynamic algebra. Report CS-R9518, CWI, March 1995.

[16] T.H. Cormen, C.E. Leiserson, and R.L. Rivest. Introduction to Algorithms. MIT Press, 1990.

[17] S. Curtis and G. Lowe. A graphical calculus. In B. Möller, editor, Mathematics of Program Construction. Springer-Verlag LNCS 947, 1995.

[18] O. de Moor. Categories, Relations and Dynamic Programming. PhD thesis, Oxford University Computing Laboratory, Programming Research Group, 1992.

[19] E.W. Dijkstra. A note on two problems in connexion with graphs. Numerische Mathematik, 1, 1959.

[20] E.W. Dijkstra. A Discipline of Programming. Prentice-Hall, 1976.

[21] H. Doornbos and R.C. Backhouse. Induction and recursion on datatypes. In B. Möller, editor, Mathematics of Program Construction. Springer-Verlag LNCS 947, 1995.

[22] L.R. Foulds. Graph Theory Applications. Springer-Verlag, 1992.

[23] P. Freyd, O. de Moor, and P. Hoogendijk. Membership of datatypes. Unpublished Draft.

[24] P. Freyd and A. Ščedrov. Categories, Allegories. North-Holland, 1990.

[25] J.E. Hopcroft and R.E. Tarjan. Efficient algorithms for graph manipulation. Communications fo the ACM, 16(6), 1973.

[26] P. Hudak. Conception, evolution, and application of functional programming languages. ACM Computing Surveys, 21(3), September 1989.

[27] J. Hughes. Why functional programming matters. The Computer Journal, 32(2), 1989.

[28] D.J. King and J. Launchbury. Structuring depth-first search algorithms in haskell. Proceedings of the 22nd. ACM Symposium on Principles of Programming Languages, USA, January 1995.

[29] J.H. Kingston. Algorithms and Data Structures: Design, Correctness, Analysis. Addison-Wesley, 1990.

[30] D.E. Knuth. The Stanford GraphBase: A Platform for Combinatorial Computing. ACM Press, Addison-Wesley, 1994.

[31] J.B. Kruskal. On the shortest spanning subtree of a graph and the traveling salesman problem. Proceedings of the American Mathematical Society, 7, 1956.

[32] G.R. Malcolm. Algebraic Data Types and Program Transformation. PhD thesis, Rijksuniversiteit Groningen, September 1990.

[33] L. Meertens. Constructing a calculus of programs. In J.L.A. van de Snepscheut, editor, Mathematics of Program Construction. Springer-Verlag LNCS 375, 1989.

[34] L. Meertens. Paramorphisms. Formal Aspects of Computing, 4(5), 1992.

[35] E. Meijer, M. Fokkinga, and R. Paterson. Functional programming with bananas, lenses, envelopes and barbed wire. In J. Hughes, editor, Functional Programming Languages and Computer Architecture. Springer-Verlag LNCS 523, 1991.

[36] Q. Miller and P. Wadler. An introduction to Orwell 6. Oxford University Computing Laboratory, Programming Research Group, 1993.

[37] B. Möller. Derivation of graph and pointer algorithms. Report Nr. 280, Institus für Mathematik der Universität Augsburg, 1993.

[38] B. Möller and M. Russling. Shorter paths to graph algorithms. Science of Computer Programming, 22(1-2), April 1994.

[39] C. Morgan. Programming from Specifications. Prentice-Hall, 2nd edition, 1994.

[40] B.C. Pierce. Basic Category Theory for Computer Scientists. MIT Press, 1991.

[41] R.C. Prim. Shortest connection networks and some generalizations. Bell System Technical Journal, 36, 1957.

[42] M. Russling. A general scheme for breadth-first graph traversal. In B. Möller, editor, Mathematics of Program Construction. Springer-Verlag LNCS 947, 1995.

[43] G. Schmidt and T. Ströhlein. Relations and Graphs. EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1993.

[44] M. Sharir. A strong-connectivity algorithm and its applications in data flow analysis. Computers and Mathematics with Applications, 7(1), 1981.

[45] M. Spivey. A categorical approach to the theory of lists. In J.L.A. van de Snepscheut, editor, Mathematics of Program Construction. Springer-Verlag LNCS 375, 1989.

[46] R.E. Tarjan. Depth first search and linear graph algorithms. SIAM Journal on Computing, 1(2), 1972.

[47] K. Thulasiraman and M.N.S. Swamy. Graphs: Theory and Algorithms. John Wiley and Sons, 1992.

[48] M.A. Weiss. Data Structures and Algorithm Analysis. Benjamin / Cummings Publishing Company, 1992.

A The Thinning-the-Closure Rule

We first state yet another property of Θ that will be needed.

Θ(B, A) = Θ(B, A) − Q·C provided \begin{matrix}A ∩ Q·C = ∅ \\ ∧ C ⊆ B \end{matrix}  (A.1)

To prove it, we argue

Θ(B, A)
= { definition of Θ, fixed point }
A ∪ (S·Θ(B, A) − Q·B)
= \{ \begin{matrix}complements: X = (X ∩ Y) ∪ (X − Y); \\ second conjunct of proviso, join: B = B ∪ C \end{matrix} \}
(A ∩ Q·C) ∪ (A − Q·C) ∪ (S·Θ(B, A) − Q·(B ∪ C))
= { first conjunct of proviso; distribution }
(A − Q·C) ∪ (S·Θ(B, A) − Q·B − Q·C)
= { distribution }
(A ∪ (S·Θ(B, A) − Q·B)) − Q·C
= { definition of Θ, fixed point }
Θ(B, A) − Q·C

Now for the big main task: the thin/Θ rule. In order to reduce the uses of converse in the proof, we restate the rule with R := R^{∘}. It is valid to do so due to the isomorphism between preorders and converses of them. The new spelling out of the rule goes

thin (Q ∩ R^{∘}) · Λ (Θ(B, A) − Q·C) ⊇ Λ Θ(B ∪ C, A − Q·C)
provided \begin{matrix}A·C^{∘} ⊆ R \\ S·C − Q·B ⊆ A \end{matrix}

By universal property of thin, we have to prove

Θ(B ∪ C, A − Q·C) ⊆ Θ(B, A) − Q·C  (a)
Θ(B, A) − Q·C ⊆ (Q ∩ R) · Θ(B ∪ C, A − Q·C)  (b)

(a) takes only two steps:

Θ(B ∪ C, A − Q·C)
= { Θ property (A.1) }
Θ(B ∪ C, A − Q·C) − Q·C
⊆ { monotonicity properties of Θ }
Θ(B, A) − Q·C

For (b), immediate intuition suggests that Q·C be moved to the right-hand side by universal property of substraction and Knaster-Tarski applied on Θ(B, A). Unfortunately, by so doing we arrive at a false statement. We pull out a rabbit that will permit a safe application of Knaster-Tarski. Note first that

X − Y = X − (Z ∩ Y)  provided X ⊆ Z.

Using it to transform the left-hand side of (b) with a suitable Z allows us to proceed as intuition hinted initially. We use Z := (Q ∩ R) · Θ(B, A) –validly since (Q ∩ R) is reflexive–.

(b)

≡ \{ \begin{matrix}introduce V := Θ(B, A), W := Θ(B ∪ C, A − Q·C); \\ rabbit described above \end{matrix} \}

V − ((Q ∩ R)·V ∩ Q·C) ⊆ (Q ∩ R)·W

≡ { substraction }

V ⊆ (Q ∩ R)·W ∪ ((Q ∩ R)·V ∩ Q·C)

≡ { introduce X := (Q ∩ R)·W, Y := (Q ∩ R)·V ∩ Q·C }

V ⊆ X ∪ Y

⇐ { Knaster-Tarski }

A ∪ (S·(X ∪ Y) − Q·B) ⊆ X ∪ Y

≡ { distribution, join }
A ⊆ X ∪ Y  (b1)
∧ S·X − Q·B ⊆ X ∪ Y  (b2)
∧ S·Y − Q·B ⊆ X ∪ Y  (b3)

For (b1), we argue

A
= { complements }
(A − Q·C) ∪ (A ∩ Q·C)
⊆ \{ \begin{matrix}by fixed point and join: \\ Θ(J, K) = K ∪ (S·Θ(J, K) − Q·J) ⊇ K, \\ hence W ⊇ A − Q·C and V ⊇ A \end{matrix} \}
W ∪ (V ∩ Q·C)
⊆ { (Q ∩ R) reflexive, definitions of X and Y }
X ∪ Y

For (b2), the left-hand side is first manipulated thus

S·X − Q·B

⊆ { definition of X, (Hyp.2) }

(Q ∩ R)·S·W − Q·B

⊆ \{ \begin{matrix}by meet and Q transitive: (Q ∩ R)·Q ⊆ Q, \\ substraction anti-monotonic on right-hand operand \end{matrix} \}

(Q ∩ R)·S·W − (Q ∩ R)·Q·B

⊆ { substraction: X ·Y − X ·Z ⊆ X ·(Y − Z) }

(Q ∩ R) · (S·W − Q·B)

= { complements, distribution }

(Q ∩ R) · (S·W − Q·B − Q·C) ∪ (Q ∩ R) · ((S·W − Q·B) ∩ Q·C)

= { introduce Z_{1} and Z_{2} }

Z_{1} ∪ Z_{2}

Hence, it suffices to show that Z_{1} ⊆ X and Z_{2} ⊆ Y. The first half:

Z_{1}

⊆ \{ \begin{matrix}by fixed point and join: \\ Θ(J, K) = K ∪ (S·Θ(J, K) − Q·J) ⊇ S·Θ(J, K) − Q·J, \\ hence W ⊇ S·W − Q·B − Q·C \end{matrix} \}

(Q ∩ R)·W

= { definition of X }

X

The second half:

Z_{2}

⊆ { by monotonicity properties of Θ: W ⊆ V }

(Q ∩ R) · ((S·V − Q·B) ∩ Q·C)

⊆ \{ \begin{matrix}by fixed point and join: \\ Θ(J, K) = K ∪ (S·Θ(J, K) − Q·J) ⊇ S·Θ(J, K) − Q·J, \\ hence V ⊇ S·V − Q·B \end{matrix} \}

(Q ∩ R) · (V ∩ Q·C)

⊆ { meet }

(Q ∩ R)·V ∩ (Q ∩ R)·Q·C

⊆ \{ \begin{matrix}by meet and Q transitive: (Q ∩ R)·Q ⊆ Q, \\ definition of Y \end{matrix} \}

Y Lastly, for (b3), we proceed

S·Y − Q·B

= { definition of Y }

S · ((Q ∩ R)·V ∩ Q·C) − Q·B

⊆ { modular law }

S · ((Q ∩ R)·V ·C^{∘} ∩ Q) · C − Q·B

⊆ { Θ property (5.7), first proviso }

S · ((Q ∩ R)·R ∩ Q) · C − Q·B

⊆ { by meet and R transitive: (Q ∩ R)·R ⊆ R }

S·(R ∩ Q)·C − Q·B

⊆ { (Hyp.2) }

(Q ∩ R)·S·C − Q·B

⊆ \{ \begin{matrix}by meet and Q transitive: (Q ∩ R)·Q ⊆ Q, \\ substraction anti-monotonic on right-hand operand \end{matrix} \}

(Q ∩ R)·S·C − (Q ∩ R)·Q·B

⊆ { substraction: X ·Y − X ·Z ⊆ X ·(Y − Z) }

(Q ∩ R) · (S·C − Q·B)

⊆ { second proviso }

(Q ∩ R)·A

⊆ { (b1) proved above, distribution }

(Q ∩ R)·X ∪ (Q ∩ R)·Y

⊆ \{ \begin{matrix}definition of X, (Q ∩ R) transitive; \\ definition of Y, meet \end{matrix} \}

X ∪ ((Q ∩ R)·V ∪ (Q ∩ R)·Q·C)

⊆ \{ \begin{matrix}by meet and Q transitive: (Q ∩ R)·Q ⊆ Q, \\ definition of Y \end{matrix} \}

X ∪ Y

Done!

B Domains and Invariants

Formally, R is inductive if and only if

(∀C : C coreflexive : R \ −C ⊆ C ⇒ id ⊆ C)

The coreflexive-division operator \ − is defined as R \ −C = id ∩ R\(C·Π). Proposition 5.8 Let R, S be relations and C a coreflexive such that R is entire, C ⊆ dom (FC · S) and S is F-inductive. Then C ⊆ dom (μX : R · FX · S). Its proof follows:

C ⊆ dom (μX : R · FX · S)

≡ { introduce M := (μX : …), division }

id ⊆ C\dom M

≡ { meet }

id ⊆ id ∩ C\dom M

⇐ { S F-inductive, that is, δ · S inductive }

(δ · S) \ −(id ∩ C\dom M) ⊆ id ∩ C\dom M

≡ { X \ −D coreflexive, meet, division }

C · (δ · S) \ −(id ∩ C\dom M) ⊆ dom M

And for the last inequation we argue

C · (δ · S) \ −(id ∩ C\dom M)

= { a coreflexive equals its domain }

dom (C · (δ · S) \ −(id ∩ C\dom M))

⊆ \{ \begin{matrix}proviso on C and S, and \\ domains: dom (dom X · Y) = dom (X · Y) \end{matrix} \}

dom (FC · S · (δ · S) \ −(id ∩ C\dom M))

= { coreflexive division: (δ · X) \ −D = X \ −FD }

dom (FC · S · S \ −F(id ∩ C\dom M))

= { coreflexive division: X · X \ −D ⊆ D · X }

dom (FC · F(id ∩ C\dom M) · S)

⊆ { meet, monotonic functors, division }

dom (F(dom M) · S)

⊆ \{ \begin{matrix}domains and monotonic \\ functors: F(dom X) ⊆ dom FX \end{matrix} \}

dom (dom FM · S)

= { domains }
dom (FM · S)
= { R entire }
dom (R · FM · S)
= { definition of M, fixed point }
dom M.

Proposition 5.9 If C is F-invariant under S, then

(μX : R · FX · S) · C = (μX : R · FX · S · C)

The proof is by mutual inclusion. Name M_{1}, M_{2} the least fixed point expressions on the left and right-hand side respectively. We start with (⊇):

M_{2}
= { definition of M_{2}, fixed point }
R · FM_{2} · S · C
= { duplicity of coreflexives, fixed point back again }
M_{2} · C
⊆ { C coreflexive, monotonicity of μ }
M_{1} · C

(⊆) takes a little longer:

M_{1} · C ⊆ M_{2}
≡ { division }
M_{1} ⊆ M_{2}/C
⇐ { definition of M_{1}, Knaster-Tarski }
R · F(M_{2}/C) · S ⊆ M_{2}/C
≡ { division }
R · F(M_{2}/C) · S · C ⊆ M_{2}

And the last line is proved thus

R · F(M_{2}/C) · S · C
⊆ { duplicity of coreflexives, C F-invariant under S }
R · F(M_{2}/C) · FC · S · C
⊆ { monotonic functors, division }
R · FM_{2} · S · C
= { definition of M_{2}, fixed point }
M_{2}.