Past exam of the year 1 of the computer science course of the University of Oxford / 2014 / Functional programming, design and analysis of algorithms / 2 / d

Maintain all pairs discovered so far. Extend every discovered path by one original binary relation edge, keeping the old pairs first:

transclose :: Eq a => [(a, a)] -> [(a, a)]
transclose r = grow (removedup r)
  where
    grow s =
      let t = removedup (s ++ relcomp r s)
      in if length t == length s then s else grow t

After $j$ extensions, the represented binary relation is $R\cup R^2\cup \cdots \cup R^{j+1}$. This loop invariant follows by distributivity of composition of relations over a union. The old list s is a duplicate-free prefix of t; therefore equality of lengths is equivalent to equality of the represented sets and signals a fixed point.

Let $V$ be the finite set of endpoints appearing in the input. No extension introduces a new endpoint, so there are at most $|V{|}^2$ distinct pairs. Every nonfinal iteration adds at least one pair, proving algorithm termination. At the fixed point $S$, we have $R\subseteq S$ and $R;S\subseteq S$. Mathematical induction gives $R^i\subseteq S$ for every positive $i$, while the loop invariant says that each discovered pair belongs to some $R^i$. HenceThis is the transitive closure of a relation, rather than a reflexive closure: diagonal pairs appear only when supported by nonempty cycles. The empty input is handled immediately.