一句话：通过构造星根，以目标导向的计算式证明建立由关系生成等价关系的自反性与传递性，并联系强连通分量算法。
论文考察如何从给定齐次二元关系构造等价关系：先取包含该关系的最小自反传递关系（星），再取包含于星中的最大对称关系。最终结果同时自反、传递且对称，因而为等价关系，但这一性质并非显然。作者不直接验证自反性与传递性的定义，而是通过给出一个“星根”来构造性地建立二者，从而突出目标导向的计算式证明中的创造性构造过程。该构造对求强连通分量以及将图分解为强连通分量与连接它们的无环图等算法具有基础意义。
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 starth root—in a way that emphasises the creative process in its construction. The resulting construction 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.
@article{paperbot2685,
title = {An example of goal-directed, calculational proof},
author = {ROLAND CARL BACKHOUSE and WALTER GUTTMANN and MICHAEL WINTER},
journal = {Journal of Functional Programming},
volume = {34},
year = {2024},
doi = {10.1017/s095679682400011x}
}