## 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$:

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 poset is a **meet semilattice**
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 poset is a **join semilattice**
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)$:

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:

and the function $f : L \to L$ is continuous,

then $\mathit{lfp}(f) = \mathit{sup}(K(\bot))$.

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)$:

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: