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.