An example of goal-directed, calculational proof

TL;DR

The paper presents a goal-directed, calculational proof of the identity $R^{*}\cap (R^{\mathrm{Prev}})^{*} = (R\cap (R^{\mathrm{Prev}})^{*})^{*}$, establishing this relation as an equivalence and linking it to strongly connected components in directed graphs. An initial attempt to apply fixed-point fusion fails due to stringent conditions, so the authors weaken the objective to prove complementary inclusions using the Heyting Galois connection and modularity, including a crucial idempotency-based cancellation step. The resulting constructive proof yields a starth root characterization that underpins SCC detection and graph decomposition algorithms, illustrating a highly goal-directed style intended to illuminate the creative reasoning in correct-by-construction proofs. This approach highlights the value of exposing calculational insight for pedagogy and practical algorithm design in relation algebra contexts.

Abstract

An equivalence relation can be constructed from a given (homogeneous, binary) relation in two steps: first, construct the smallest reflexive and transitive relation containing the given relation (the "star" of the relation) and, second, construct the largest symmetric relation that is included in the result of the first step. The fact that the final result is also reflexive and transitive (as well as symmetric), and thus an equivalence relation, is not immediately obvious, although straightforward to prove. Rather than prove that the defining properties of reflexivity and transitivity are satisfied, we establish reflexivity and transitivity constructively by exhibiting a particular starth root -- in a way that emphasises the creative process in its construction. The constructed starth root is fundamental to algorithms that determine the strongly connected components of a graph as well as the decomposition of a graph into its strongly connected components together with an acyclic graph connecting such components.