An Exercise Utilising Galois Connections

Given two partial orders (A, ⊑), (B, ≼), two functions f : A → B, g : B → A form a Galois connection between them if for all a : A, b : B we have

  f a ≼ b ≣ a ⊑ g b

We will refer to this defining property as “GC” later. The function f is called the lower adjoint and g the upper adjoint of the Galois connection. Galois connections are interesting because once two functions are identified as such, they immediately satisfy a rich collection of useful properties:

• letting a := g b in GC, we get f (g b) ≼ b;
• letting b := f a, we get a ⊑ g (f a);
• f is monotonic, since:

   f a₁ ≼ f a₂
  ≣   { GC }
   a₁ ⊑ g (f a₂)
  ⇐  {  since a ⊑ g (f a) }
   a₁ ⊑ a₂

• similarly, g is monotonic: b₁ ≼ b₂ ⇒ f b₁ ⊑ f b₂,

and many more.

In the recent work of Sharon and me on maximally dense segments we needed quite a number of functions to be monotonic, idempotent, etc. It only occurred to me after submitting the paper: could they be defined as Galois connections? The number of properties we needed in the paper is huge and it would be nice to establish them on fewer basic properties. And it looks prettier.

Longest Prefix Up to a Certain Sum

One such function is trim in the paper, but it is sufficient to consider a simplification: let sam : [Int] → [Int] (for “sum atmost”) return the longest prefix of the input list whose sum is no larger than a constant U. Denote “x is a prefix of y” by x ⊑ y. We want to show that sam satisfies

• monotonicity: x ⊑ y ⇒ sam x ⊑ sam y, and
• idempotence: sam (sam x) = sam x.

Can they be derived by defining sam as a Galois connection?

I learned from José N. Oliveira‘s talk A Look at Program “G”alculation in IFIP WG 2.1 #65 Meeting how (the uncurried version of) take can be defined as a Galois connection. It turns out that sam is just the same. We consider a slight generalisation sam' : (Int, [Int]) → [Int] that takes an upper bound as a parameter. It can be characterised by:

sum y ≤ b  ∧  y ⊑ x   ≣   y ⊑ sam' (b, x)

There is in fact a Galois connection hidden already! To see that, define ⟨f, g⟩ a = (f a, g a) (in the Haskell Hierarchy Library it is defined in Control.Arrow as &&&), and denote the product of binary relations by ×, that is, if a ≤ b and x ⊑ y then (a,x) is related to (b,y) by ≤×⊑. We write a composed relation as an infix operator by surrounding it in square brackets (a,x) [≤×⊑] (b,y).

Using these notations, the defining equation of sam' can be rewritten as:

⟨sum, id⟩ y [≤×⊑] (b,x)   ≣   y ⊑ sam' (b,x)

Thus sam' is the upper adjoint in a Galois connection between ((Int, [Int]), ≤×⊑) and ([Int], ⊑)!

Now that ⟨sum, id⟩ and sam' form a Galois connection, we have:

• f (g b) ≼ b instantiates to ⟨sum, id⟩ (sam' (b,x)) [≤×⊑] (b,x), that is, sum (sam' (b,x)) ≤ b and sam' (b,x) ⊑ x;
• a ⊑ g (f a) instantiates to x ⊑ sam' (sum x, x). Together with the previous property we have x = sam' (sum x, x);
• monotonicity of the lower adjoint instantiates to y₁ ⊑ y₂ ⇒ sum y₁ ≤ sum y₂ ∧ y₁ ⊑ y₂;
• monotonicity of the upper adjoint instantiates to

  (b₁,x₁) [≤×⊑] (b₂,x₂)   ⇒   sam' (b₁,x₁) ⊑ sam' (b₂,x₂) 

  that is

  b₁ ≤ b₂   ∧  x₁ ⊑ x₂   ⇒   sam' (b₁,x₁) ⊑ sam' (b₂,x₂) 

  a generalisation of the monotonicity we want.

Finally, to show idempotence, we reason

   sam' (b₁, x) ⊑ sam' (b₁, sam' (b₂, x))
≣   { GC }
   ⟨sum, id⟩ (sam' (b₁, x)) [≤×⊑]  (b₁, sam' (b₂, x))
≣   { definitions }
   sum (sam' (b₁, x)) ≤ b₁   ∧   sam' (b₁, x) ⊑ sam' (b₂, x)
⇐  { properties above }
   b₁ ≤ b₂

These are all nice and pretty. There is another function, however, that is much harder to deal with, which I will write about next time.