An example of goal-directed, calculational proof

Backhouse, Roland Carl; Guttmann, Walter; Winter, Michael

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.

Citation

Backhouse, R. C., Guttmann, W., & Winter, M. (2024). An example of goal-directed, calculational proof. Journal of Functional Programming, 34, Article e13. https://doi.org/10.1017/s095679682400011x

• Journal Article Type: Article
• Acceptance Date: Aug 29, 2024
• Online Publication Date: Dec 11, 2024
• Publication Date: 2024
• Deposit Date: Dec 12, 2024
• Publicly Available Date: Dec 12, 2024
• Journal: Journal of Functional Programming
• Print ISSN: 0956-7968
• Electronic ISSN: 1469-7653
• Publisher: Cambridge University Press
• Peer Reviewed: Peer Reviewed
• Volume: 34
• Article Number: e13
• DOI: https://doi.org/10.1017/s095679682400011x
• Public URL: https://nottingham-repository.worktribe.com/output/42836553
• Publisher URL: https://www.cambridge.org/core/journals/journal-of-functional-programming/article/an-example-of-goaldirected-calculational-proof/A20D6BD38245A04263684CFDC5375C0D
• Additional Information: Copyright: © The Author(s), 2024. Published by Cambridge University Press; License: This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (https://creativecommons.org/licenses/by/4.0/), which permits unrestricted re-use, distribution and reproduction, provided the original article is properly cited.; Free to read: This content has been made available to all.