Order theory for computer scientists

Haskell code

The header for the Haskell code in this file is:

import Data.Map as Map hiding (map)
import Data.Set as Set hiding (map)

type ℙ a = Set.Set a

type k :-> v = Map.Map k v

And, the ghc extensions used are:

 -XTypeOperators -XTypeSynonymInstances \
 -XParallelListComp -XFlexibleInstances

Preorders

A binary relation $\sqsubseteq$ on a set $X$ is a preorder iff the relation $\sqsubseteq$ is both reflexive and transitive.

A binary relation $R$ is reflexive if $x \mathrel{R} x$ for any $x$.

A binary relation $R$ is transitive if $a \mathrel{R} b$ and $b \mathrel{R} c$ implies $a \mathrel{R} c$.

Equivalence relations

An equivalence relation $\equiv$ is a preorder that is also symmetric.

A binary relation $R$ is symmetric if $a \mathrel{R} b$ implies $b \mathrel{R} a$.

An equivalence relation $\equiv$ divides a set $S$ into equivalence classes.

The equivalence class of the element $x$ is $[x]_\equiv$:

\[ [x]_\equiv = \{ y \mathrel{|} x \equiv y \} \text. \]

The set of all equivalence classes on $X$ under the relation $\equiv$ is the set $X/\equiv$.

Equivalence relations from preorders

Every preorder $\sqsubseteq$ induces a natural equivalence relation $\equiv_{\sqsubseteq}$:

\[ a \mathrel{\equiv_{\sqsubseteq}} b \text{ iff } a \sqsubseteq b \text{ and } b \sqsubseteq a \text. \]

Partial orders

A partial order is a preorder that is antisymmetric.

A partially ordered set or poset is a set $X$ equipped with a partial order $\sqsubseteq$, often described as the pair $(X,\sqsubseteq)$.

A binary relation $R$ is antisymmetric if $a \mathrel{R} b$ and $b \mathrel{R} a$ implies $a = b$.

In Haskell, we can define a partial order through type classes:

class PartialOrder t where
 (⊑) :: t -> t -> Bool

Total orders

A total order $\leq$ is a binary relation that is total, transitive and antisymmetric.

A binary relation $R$ is total if for any two values $a$ and $b$, $a \mathrel{R} b$ or $b \mathrel{R} a$.

Totality implies reflexivity, which means that every total order is also a partial order.

Meet semilattices

A meet semilattice is a poset for which any two elements $a$ and $b$ have a greatest lower bound, denoted $a \sqcap b$.

The greatest lower bound of $a$ and $b$ is the largest element that is still less than both of them.

In a lattice, the greatest lower bound must be unique.

The greatest lower bound of $a$ and $b$ is also called the meet or infimum of $a$ and $b$.

The greatest lower bound has the following properties:

• $(a \sqcap b) \sqsubseteq a$.
• $(a \sqcap b) \sqsubseteq b$.
• $c \sqsubseteq a$ and $c \sqsubseteq b$ implies $c \sqsubseteq (a \sqcap b)$.

Join semilattices

A join semilattice is a poset for which any two elements $a$ and $b$ have a least upper bound, denoted $a \sqcup b$.

The least upper bound of $a$ and $b$ is the smallest element that is still greater than both.

In a lattice, the least upper bound must be unique.

The least upper bound of $a$ and $b$ is also called the join or supremum of $a$ and $b$.

The least upper bound has the following properties:

• $a \sqsubseteq (a \sqcup b)$.
• $b \sqsubseteq (a \sqcup b)$.
• $a \sqsubseteq c$ and $b \sqsubseteq c$ implies $(a \sqcup b) \sqsubseteq c$.

Lattices

If a poset is both a meet semilattice and a join semilattice, then the poset is also a lattice.

In Haskell, a lattice is a partial order with meet and join defined:

class PartialOrder t => Lattice t where
 (⊔) :: t -> t -> t
 (⊓) :: t -> t -> t

Bounded lattices

A lattice $(L,\sqsubseteq)$ is bounded if there exists a maximum element (top or $\top$) and a minimum element (bottom or $\bot$) in the set $L$.

For any element $x$ in the lattice, it must be the case that:

• $x \sqsubseteq \top$ and
• $\bot \sqsubseteq x$.

In Haskell, the type class for a bounded lattice defines a top and a bottom:

class Lattice t => BoundedLattice t where
 bot :: t
 top :: t

Complete lattices

A lattice $(L,\sqsubseteq)$ is a complete lattice if every (possibly infinite) subset $S$ of $L$ has both a least upper bound ($\mathit{sup}(S)$) and a greatest lower bound ($\mathit{inf}(S)$).

Every complete lattice $(L,\sqsubseteq)$ is a bounded lattice:

• $\bot = \mathit{inf}(L)$.
• $\top = \mathit{sup}(L)$.

Monotonic functions

Given posets $(X,\sqsubseteq_X)$ and $(Y,\sqsubseteq_Y)$, a function $f : X \to Y$ is monotonic or order-preserving if $x \mathrel{\sqsubseteq_X} x'$ implies $f(x) \mathrel{\sqsubseteq_Y} f(x')$.

Continuous functions

To define continuous function, we first need to define member-wise function application across sets.

Given a function $f : X \to Y$, if $S \subseteq X$, then $f.S = \{ f(x) \mathrel{|} x \in S \}$.

Alternately, $f.\{x_1,\ldots,x_n\} = \{f(x_1), \ldots, f(x_n)\}$.

(In some texts, member-wise function application is not notationally distinguished from ordinary function application.)

Given lattices $(X,\sqsubseteq_X)$ and $(Y,\sqsubseteq_Y)$, a function $f : X \to Y$ is Scott-continuous if $S \subseteq X$ implies $f(\mathit{sup}(S)) = \mathit{sup}(f.S)$.

Scott-continuous functions are also monotonic.

Fixed points

Given a function $f : X \to X$, $x$ is a fixed point of $f$ if $x = f(x)$.

Regions

With respect to a monotonic function $f : X \to X$ on a complete lattice $(X,\sqsubseteq)$, we can divide the set $X$ into regions:

• $\mathit{Fix}(f) = \{ x \mathrel{|} x = f(x) \}$ is the fixed-point region.
• $\mathit{Asc}(f) = \{ x \mathrel{|} x \sqsubseteq f(x) \}$ is the ascending region.
• $\mathit{Desc}(f) = \{ x \mathrel{|} x \sqsupseteq f(x) \}$ is the descending region.

It is useful to distinguish the least and greatest fixed points:

• $\mathit{lfp}(f) = \mathit{inf}(\mathit{Fix}(f))$.
• $\mathit{gfp}(f) = \mathit{sup}(\mathit{Fix}(f))$.

The following properties hold for these regions:

• $\mathit{Fix}(f) = \mathit{Asc}(f) \cap \mathit{Desc}(f)$.
• If $x \in \mathit{Asc}(f)$, then $f(x) \in \mathit{Asc}(f)$.
• If $x \in \mathit{Desc}(f)$, then $f(x) \in \mathit{Desc}(f)$.
• $\bot \in \mathit{Asc}(f)$.
• $\top \in \mathit{Desc}(f)$.

I recommend proving these properties as short exercises.

Kleene chain

Given a monotonic function $f : L \to L$ on a lattice $(L,\sqsubseteq)$, the Kleene chain starting at the point $x \in L$ is the set $K(x)$:

\[ K(x) = \{ f^i(x) \mathrel{|} i \geq 0 \} \]

The $f^i$ notation means iterated function composition:

\[ f^0(x) = x \text{ and } f^i(x) = f^{i-1}(f(x)) \text. \]

If $x \in \mathit{Asc}(f)$, then there will be an ascending order to the chain $K(x)$, since $f^i(x') \sqsubseteq f^{i+1}(x')$ for any $x' \in \mathit{Asc}(f)$.

In Haskell, an infinite list represents the Kleene chain starting at bottom:

kleene :: (BoundedLattice t) => (t -> t) -> [t]
kleene f = bot:(map f (kleene f))

Kleene's fixed point theorem

On lattices, Kleene's fixed point theorem says:

Moreover, for a lattice of finite height, there exists a natural $n$ such that: \[ \mathit{lfp}(f) = f^n(\bot)\text. \]

This fact leads to a simple algorithm for computing fixed points.

The stable function looks for the first element in a sequence to repeat its neighbor:

stable :: Eq a => [a] -> a
stable (x:fx:tl) | x == fx   = x
                 | otherwise = stable (fx:tl)

So, the least fixed point function looks for a stable point in the Kleene sequence:

lfp :: (BoundedLattice t, Eq t) => (t -> t) -> t
lfp f = stable (kleene f)

Natural lifts for lattices

There are several natural liftings for posets and lattices across the foundational discrete data structures: flat sets, power sets, Cartesian products, sums, sequences and functions.

Pointed sets

Given a set $S$, the pointed poset $S_\bot$ contains a bottom:

\[ S_\bot = S + \bot \text. \]

And, the pointed poset $S^\top$ contains a top:

\[ S^\top = S + \top \text. \]

If $(S,\sqsubseteq)$ is a poset, then the order is extended under pointing, so that for the lattice $(S^\top_\bot,\sqsubseteq')$:

• $\bot \mathrel{\sqsubseteq'} x$ for any $x$.
• $x \mathrel{\sqsubseteq'} \top$ for any $x$.
• $x \mathrel{\sqsubseteq'} x'$ iff $x \mathrel{\sqsubseteq} x'$ for any $x,x' \in S$.

In Haskell:

data Pointed a = PTop
               | PBot
               | PEl a 

instance PartialOrder a => PartialOrder (Pointed a) where 
 PBot ⊑ x = True
 x ⊑ PTop = True
 (PEl a) ⊑ (PEl b) = a ⊑ b

Flat lattices

Given a set $S$, we can lift $S$ into a flat lattice $(L,\sqsubseteq)$:

\[ L = S^\top_\bot\text = S + \bot + \top\text. \]

where $x \sqsubseteq y$ iff:

• $x = \bot$ or
• $y = \top$ or
• $x = y$.

In Haskell:

data Flat a = Top 
            | Bot
            | El a

instance (Eq a) => PartialOrder (Flat a) where
 Bot ⊑ x = True
 x ⊑ Top = True
 (El a) ⊑ (El b) = a == b

instance (Eq a) => Lattice (Flat a) where
 Bot ⊔ x = x
 x ⊔ Bot = x

 Top ⊔ x = Top
 x ⊔ Top = Top

 (El a) ⊔ (El b) | a == b    = El a
                 | otherwise = Top

 Bot ⊓ x = Bot
 x ⊓ Bot = Bot

 Top ⊓ x = x
 x ⊓ Top = x

 (El a) ⊓ (El b) | a == b    = El a
                 | otherwise = Bot

instance (Eq a) => BoundedLattice (Flat a) where
 bot = Bot
 top = Top

Partial orders over sums

Given a collection of posets $(X_1,\sqsubseteq_1),\ldots,(X_n,\sqsubseteq_n)$ we can naturally lift the partial order into the poset $(X_1 + \cdots + X_n, \sqsubseteq)$:

\[ x \sqsubseteq x' \text{ iff } x \mathrel{\sqsubseteq_i} x' \text{ for some } i\text. \]

If the posets are lattices, then the resulting poset is not a lattice by default.

To make it into a lattice, it must pointed.

Lattices over Cartesian products

Given lattices $(L_1,\sqsubseteq_1)$ and $(L_2,\sqsubseteq_2)$, the natural component-wise Cartesian product lattice is $(L_1 \times L_2, \sqsubseteq)$:

\[ (a,b) \sqsubseteq (a',b') \text { iff } a \mathrel{\sqsubseteq_1} a' \text{ and } b \mathrel{\sqsubseteq_2} b'\text. \]

so that:

• $(a,b) \sqcup (a',b') = (a \sqcup a', b \sqcup b')$; and
• $(a,b) \sqcap (a',b') = (a \sqcap a', b \sqcap b')$; and
• $\bot = (\bot_{L_1},\bot_{L_2})$; and
• $\top = (\top_{L_1},\top_{L_2})$.

In Haskell:

instance (PartialOrder a, PartialOrder b) => PartialOrder (a,b) where
 (x,y) ⊑ (x',y') = x ⊑ x' && y ⊑ y'

instance (Lattice a, Lattice b) => Lattice (a,b) where
 (x,y) ⊔ (x',y') = (x ⊔ x', y ⊔ y')
 (x,y) ⊓ (x',y') = (x ⊓ x', y ⊓ y')

instance (BoundedLattice a, BoundedLattice b) => 
         BoundedLattice (a,b) where
 bot = (bot,bot)
 top = (top,top)

Partial orders over sequences

Given a poset $(L,\sqsubseteq)$ the natural sequence poset is $(L^*,\sqsubseteq^*)$:

\[ \langle x_1, \ldots, x_n \rangle \mathrel{\sqsubseteq^*} \langle x_1', \ldots, x_n' \rangle \text { iff } x_i \sqsubseteq x_i' \text{ for all } i \text{ such that } 0 \leq i \leq n \text. \]

As with sums, sequences must be pointed to become lattices. That is, there is no sequence which is greater (or lesser) than all other sequences because sequences of different lengths are always incomparable.

In Haskell:

instance (PartialOrder a) => PartialOrder [a] where
 []     ⊑ []       = True
 (x:xl) ⊑ (x':xl') = (x ⊑ x') && (xl ⊑ xl')
 _      ⊑ _        = False -- different lengths

instance (Lattice a) => Lattice (Pointed [a]) where
 PBot ⊔ x = x
 x ⊔ PBot = x

 PTop ⊔ x = PTop
 x ⊔ PTop = PTop 

 (PEl v) ⊔ (PEl v') = PEl [ x ⊔ x' | x <- v | x' <- v' ]

 PBot ⊓ x = PBot
 x ⊓ PBot = PBot

 PTop ⊓ x = x
 x ⊓ PTop = x

 (PEl v) ⊓ (PEl v') = PEl [ x ⊓ x' | x <- v | x' <- v' ]

instance (Lattice a) => BoundedLattice (Pointed [a]) where 
 bot = PBot
 top = PTop

Inclusion lattices

Given a set $S$, the subsets of $S$ form a lattice under inclusion: $(\mathcal{P}(S),\subseteq)$.

Preorder over partially ordered sets

Given a partial order $(X,\sqsubseteq)$, we can define the preordered set $(\mathcal{P}(X), \sqsubseteq')$:

\[ S \mathrel{\sqsubseteq'} S' \text{ iff for each } x \in S, \text{ there exists } x' \in S' \text{ such that } x \sqsubseteq x' \text. \]

Why is this not a partial order itself?

Consider sets over the natural numbers with the natural total order. Under this regime, $\{1,2,3\} \mathrel{\sqsubseteq'} \{3\}$ and $\{3\} \mathrel{\sqsubseteq'} \{1,2,3\}$, yet $\{1,2,3\} \neq \{3\}$, which violates antisymmetry.

Of course, it is possible to lift a preorder into a partial order over equivalences classes.

Alternatively, sets can be canonicalized, so that only that each equivalence class is represented by a single distinguished member.

Partial orders from preorders

If a preorder is not also a partial order, it is possible to lift a partial order to equivalence classes of the preorder.

Given a preordered set $(X,\leq)$, the natural partial order over equivalence classes is the poset $(X/{\equiv},\sqsubseteq)$, where $a \equiv b$ iff $a \leq b$ and $b \leq a$:

\[ [x]_\equiv \sqsubseteq [y]_\equiv \text{ iff } x \leq y \text. \]

Lattices over functions

Given a lattice $(Y,\sqsubseteq)$ and a set $X$, the natural point-wise lattice is the lattice $(X \to Y, \sqsubseteq')$:

\[ f \mathrel{\sqsubseteq'} g \text{ iff } f(x) \sqsubseteq g(x) \text{ for every } x \in \mathit{dom}(f) \text, \]

so that:

\[ (f \sqcup g)(x) = f(x) \sqcup g(x) \text, \] and: \[ (f \sqcap g)(x) = f(x) \sqcap g(x) \text. \]

In Haskell:

instance (Ord k, PartialOrder v) => PartialOrder (k :-> v) where
 f ⊑ g = isSubmapOfBy (⊑) f g

instance (Ord k, Lattice v) => Lattice (k :-> v) where
 f ⊔ g = unionWith (⊔) f g
 f ⊓ g = unionWith (⊓) f g

instance (Ord k, BoundedLattice v) => BoundedLattice (k :-> v) where
 bot = Map.empty
 top = error "top map: not finitely representable" 

What's next?

This post scratches the surface of order theory, and it leaves out even some applications in computer science.

The two biggest omissions are reserved for future posts: the ordinals and the Scott domain theory.

The ordinals extend the natural numbers into a transfinite arithmetic and provide a powerful structure for well-ordering.

That well-ordered structure is a powerful mechanism for reasoning about program termination.

Scott domain theory gives a meaningful interpretation to the infinitely recursive domain equations that arise in denotational semantics.

If you'd like to learn Haskell, I recommend Learn You a Haskell for Great Good!: A Beginner's Guide:

And, for using Haskell, I recommend Real World Haskell:

Related posts

---