Reflexive Transitive Closure

definition example theorem

Level shifting (7 Sketches §1.4.5): for any Set $S$ there is a Preorder $\mathrm{Rel}(S)$ of all binary relations on $S$, ordered by inclusion $R\subseteq R^{\prime }$. There is also a set $\mathrm{Pos}(S)$ of all preorder relations on $S$, itself a preorder under inclusion $\le ⊑{\le }^{\prime }$ (iff $a\le b$ implies $a{\le }^{\prime }b$) — “a preorder of preorder structures: that’s what we mean by a level shift”.

Sources: 7 Sketches §1.4.5, Exercises 1.124, 1.125; CTfS Example 3.4.1.13, Exercise 3.4.1.14

Every preorder relation is a relation, giving an inclusion $U:\mathrm{Pos}(S)\to \mathrm{Rel}(S)$. This is the right adjoint of a Galois Connection whose left adjoint

$$\mathrm{Cl}:\mathrm{Rel}(S)\to \mathrm{Pos}(S)$$

takes a relation $R$ to its reflexive and transitive closure: add $s\le s$ for every $s$ and $s\le u$ whenever $s\le t$ and $t\le u$. The adjunction says $\mathrm{Cl}(Q)⊑\le$ iff $Q\subseteq U(\le )$: a preorder contains the closure of $Q$ exactly when it contains $Q$ (7S Exercise 1.125). The composite $U\circ \mathrm{Cl}$ is a Closure Operator on $\mathrm{Rel}(S)$.

Example. $\mathrm{Rel}(\{1\})$ has two elements $\varnothing \le \{(1,1)\}$; $\mathrm{Rel}(\{1,2\})$ has 16 (7S Exercise 1.124).

Computing it (CTfS Example 3.4.1.13): add the diagonal, then add $(x,y)$ whenever $(x,z),(z,y)$ are present — and repeat until nothing changes; a single round of composition is not enough in general (for $1\to 2\to 3\to 4$ one round adds $(1,3)$ and $(2,4)$ but not $(1,4)$). Over a Quantale this iteration is the stabilizing matrix power of Matrix Multiplication in a Quantale. The preorder generated by ”$x$ is a child of $y$” is ”$x$ is a descendant of $y$ (or $x=y$)“.

This is the preorder analogue of the Free Category on a Graph (the reflexive-transitive closure with named paths), of the Free Monoid, and of the Hasse Diagram construction: a graph presents the preorder $\mathrm{Cl}(A)$.

JuliaLeanHaskell

Docs: Vignette: preorders

# reflexive transitive closure of a relation on {1..n} given as a BitMatrix (Warshall)
function refl_trans_closure(R::BitMatrix)
  n = size(R, 1); C = copy(R)
  for i in 1:n; C[i,i] = true; end
  for k in 1:n, i in 1:n, j in 1:n
    C[i,j] |= C[i,k] && C[k,j]
  end
  C
end
R = BitMatrix([0 1 0; 0 0 1; 0 0 0])
refl_trans_closure(R)      # the chain 1 ≤ 2 ≤ 3

#check @Relation.ReflTransGen      -- inductive reflexive-transitive closure
#check @Relation.ReflTransGen.mono
-- the adjunction: ReflTransGen r ≤ s ↔ r ≤ s for a preorder s (transitive & reflexive)
#check @Relation.reflTransGen_eq_self

-- closure of a finite relation (as a list of pairs) on a finite carrier
reflTransClosure :: Eq a => [a] -> [(a, a)] -> [(a, a)]
reflTransClosure xs r = fixpoint step (r ++ [(x, x) | x <- xs])
  where
    step s = foldr addNew s [ (a, c) | (a, b) <- s, (b', c) <- s, b == b' ]
    addNew p s = if p `elem` s then s else p : s
    fixpoint f s = let s' = f s in if length s' == length s then s else fixpoint f s'