Calculating Programs from Galois Connections

Galois connections are ubiquitous in mathematics and computing science. One is often amazed that, once two functions are identified as a Galois connection, a long list of nice and often useful properties follow from one concise, elegant defining equation. But how does one construct a program from a specification given as a Galois connection? This is the topic of a recent work of José Nuno Oliveira and I, and this article is an advertisement.

Galois Connections as Specifications

In program construction one often encounters program specification of the form “… the smallest such number”, “the longest prefix of the input list satisfying …”, etc. A typical example is whole number division: given a natural number x and a positive integer y, x / y is the largest natural number that, when multiplied by y, is at most x. For another example, the Haskell function takeWhile p returns the longest prefix of the input list such that all elements satisfy predicate p.

Such specifications can be seen as consisting of two parts. The easy part specifies a collection of solution candidates: numbers that are at most x after multiplication with y, or all prefixes of the input list. The hard part, on the other hand, picks one optimal solution, such as the largest, the longest, etc., among the collection.

Our goal is to calculate programs for such specifications. But how best should the specification be given in the first place? Take division for example, one might start from a specification that literally translates our description above into mathematics:

    x / y = ⋁{ z | z * y ≤ x }

As we know, however, suprema is in general not easy to handle. One could also explicitly name the remainder:

    z = x / y  ≡  (∃ r : 0 ≤ r < y : x = z * y + r)

at the cost of existentially quantifying over the remainder.

A third option looks surprising simpler: given x and y, the value x / y is such that for all z,

    z * y ≤ x  ≡  z ≤ x / y(1)

Why is this sufficient as a definition of x / y? Firstly, by substituting x / y for z, the right hand side of ≡ reduces to true, and we obtain on the left hand side (x / y) * y ≤ x. This tell that x / y is a candidate — it satisfies the easy part of the specification. Secondly, read the definition from left to right: z * y ≤ x ⇒ z ≤ x / y. It says that x / y is the largest among all the numbers satisfying the easy part.

Equations of the form are called Galois connections. Given preorders ⊑ and ≤, Functions f and g form a Galois connection if for all x and z we have

    f z ⊑ x  ≡  z ≤ g x(2)

The function f is called the lower adjoint and g the upper adjoint.

The definition of division above is a Galois connection where f = (* y) and g = (/ y). For another example, takeWhile p can be specified as an upper adjoint:

    map p? zs ⊑ xs  ≡  zs ⊑ takeWhile p xs(3)

where ⊑ is the prefix ordering: ys ⊑ xs if ys is a prefix of xs, and map p? is a partial function: map p? xs = xs if p x holds for each x in xs.

We love Galois connections because once two functions are identified as such, a long list of useful properties follows: f (g x) ⊑ x, z ≤ g (f z), f and g are monotonic, and are inverses of each other in the other’s range… etc.

These are all very nice. But can one calculate a program from a Galois connection? Given ⊑, ≤, and f, how does one construct g?

The “Shrink” Operator

José discovered and proposed a relational operator to handle such calculations. To use the operator, we have to turn the Galois connection (1) into point-free style. We look at the left hand side of (1): f z ⊑ x, and try to write it as a relation between z and x. Let f° denote the relational converse of f — roughly, think of it as the inverse function of f, that it, it maps f z to z, and let ∘ denote relational composition — function composition extended to relations. Thus f z ⊑ x translates to

    f° ∘ (⊑)

It is a relation between z and x: putting x on the left hand side of f° ∘ (⊑), it relates, through ⊑, to f z, which is then mapped to z through f°.

Then we wish that f° ∘ (⊑) can be transformed into a (relational) fold or unfold, which is often the case because the defining components: ⊑, ≤, and f, are often folds or unfolds. Consider the lower adjoint of takeWhile p in (3). Since ⊑, the relation that takes a list and returns a prefix of the list, can be defined as a fold on lists, (map p?)° ∘ (⊑), by fold fusion, is also a fold. Consider (1), since ≤ and (* y) are both folds on natural numbers, (* y)° ∘ (≤) can be both a fold and an unfold.

In our paper we showed that a Galois connection (2) can be transformed into

    g = (f° ∘ (⊑)) ↾ (≥)

where ↾ is the new operator José introduced. The relation S ↾ R, pronounced “S shrunk by R“, is a sub-relation of S that yields, for each input, an optimal result under relation R. Note that the equation made the easy/hard division explicit: f° ∘ (⊑) is the easy part: we want a solution z that satisfies f z ⊑ x, while ≥ is the criteria we use, in the hard part, to choose an optimal solution.

The ↾ operator is similar to the min operator of Bird and de Moor, without having to use sets (which needs a power allegory). It satisfies a number of useful properties. In particular, we have theorems stating when (↾ R) promotes into folds and unfolds. For example,

    (fold S) ↾ R ⊇ fold (S ↾ R)

if R is transitive and S is monotonic on R.

With the theorems we can calculate g. Given g, specified as an upper adjoint in a Galois connection with lower adjoint f, we first try to turn f° ∘ (⊑) into a fold or an unfold, and then apply the theorems to promote (↾ (≥)). For more details, take a look at our paper!