pith. sign in

arxiv: 2301.10311 · v4 · submitted 2023-01-24 · 💻 cs.LO

Relation-Algebraic Verification of Disjoint-Set Forests

Walter Guttmann This is my paper

Pith reviewed 2026-05-24 10:02 UTC · model grok-4.3

classification 💻 cs.LO
keywords relation algebradisjoint-set forestunion-findprogram verificationassociative arraypath compressionIsabelle/HOL
0
0 comments X

The pith

Relation algebras verify the correctness of array-based disjoint-set forest implementations with union-by-rank and path compression.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper shows how relation algebras can move from high-level specifications to verifying lower-level array-based algorithm implementations. It defines a relation-algebraic semantics for read and write operations on associative arrays that integrates directly with assignments in while-program models. Using this semantics, the paper formally proves in Isabelle/HOL that an array-based disjoint-set forest is correct under the union-by-rank strategy together with find operations that use path compression, path splitting, or path halving.

Core claim

By supplying a relation-algebraic semantics for read and write on associative arrays, relation algebras become applicable to the verification of while-programs that manipulate arrays; this is demonstrated by proving the correctness of the standard array implementation of disjoint-set forests that uses union by rank and the three listed path-shortening strategies for find.

What carries the argument

The relation-algebraic semantics for read and write operations on associative arrays, which integrates with assignments in while-programs.

If this is right

  • The array-based disjoint-set forest with union-by-rank is correct for the three path strategies.
  • Relation algebras can verify programs that use associative arrays.
  • All proofs are machine-checked in Isabelle/HOL.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same array semantics could be reused to verify other array-based data structures in relation algebra.
  • The integration with while-programs suggests the method extends to other imperative computation models that support arrays.
  • Formal verification effort may decrease for algorithms already specified relation-algebraically once the array layer is added.

Load-bearing premise

The newly defined relation-algebraic semantics for read and write on associative arrays correctly models the actual behavior of arrays inside the while-program computation model.

What would settle it

A concrete read or write sequence on an associative array where the relation-algebraic model yields a different outcome from the standard array semantics inside the while-program model.

read the original abstract

This paper studies how to use relation algebras, which are useful for high-level specification and verification, for proving the correctness of lower-level array-based implementations of algorithms. We give a simple relation-algebraic semantics of read and write operations on associative arrays. The array operations seamlessly integrate with assignments in computation models supporting while-programs. As a result, relation algebras can be used for verifying programs with associative arrays. We verify the correctness of an array-based implementation of disjoint-set forests using the union-by-rank strategy and find operations with path compression, path splitting and path halving. All results are formally proved in Isabelle/HOL. This paper is an extended version of [1].

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The paper introduces a simple relation-algebraic semantics for read and write operations on associative arrays that integrates directly with assignments in a while-program model. It then uses this semantics to verify the correctness of an array-based implementation of disjoint-set forests under the union-by-rank strategy, including find operations with path compression, path splitting, and path halving. All results are claimed to be formally proved inside Isabelle/HOL; the manuscript is an extended version of a prior conference paper.

Significance. If the array semantics is faithful, the work supplies a reusable algebraic framework for verifying low-level array programs at the same level of abstraction used for high-level specifications. The machine-checked Isabelle/HOL proofs constitute a concrete strength, as they eliminate the usual gap between paper proofs and implementation. The approach is directly applicable to other array-based algorithms whose invariants can be expressed relationally.

minor comments (2)
  1. [array operations section] The integration of the new array read/write operators with the existing while-program assignment rules (mentioned in the abstract and the array-operations section) would benefit from an explicit statement of the substitution lemma that justifies replacing an array write by a relational update inside a subsequent read.
  2. [introduction] Because the manuscript is an extended version, a short paragraph contrasting the new material (array semantics plus the three path-compression variants) with the conference version would help readers assess the increment.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive review and the recommendation to accept the manuscript.

Circularity Check

0 steps flagged

No significant circularity

full rationale

The paper's central claim is a machine-checked formal verification in Isabelle/HOL of an array-based disjoint-set forest implementation (union-by-rank with path compression/splitting/halving) inside a while-program model. It introduces a new relation-algebraic semantics for associative-array read/write operations that integrates with assignments, then proves correctness of the implementation against this semantics. This is self-contained against external benchmarks (the theorem prover) with no reduction of the verification result to fitted parameters, self-defined quantities, or load-bearing self-citations. The note that the paper is an extended version of [1] is incidental and does not make the proofs depend on unverified prior content by the same author. No patterns of self-definitional derivation, fitted inputs called predictions, or ansatz smuggling apply.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

Abstract supplies no evidence of free parameters or newly invented entities; the work relies on the standard axioms of relation algebras and the Isabelle/HOL logic.

axioms (1)
  • standard math Standard axioms of relation algebras
    Invoked for high-level specification and verification as described in the abstract.

pith-pipeline@v0.9.0 · 5629 in / 1230 out tokens · 24913 ms · 2026-05-24T10:02:58.354679+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

61 extracted references · 61 canonical work pages

  1. [2]

    https://doi.org/10.1007/978-1- 4684-3384-5_11

    Back RJ, von Wright J. Refinement Calculus. Springer, New York, 1998. doi:10.1007/978-1- 4612-1674-2

    work page doi:10.1007/978-1- 1998

  2. [3]

    Unifying theories of programming

    Hoare CAR, He J. Unifying theories of programming. Prentice Hall Europe, 1998. ISBN- 10:0134587618, 13:978-0134587615

    work page 1998

  3. [4]

    Relation-algebraic semantics

    Maddux RD. Relation-algebraic semantics. Theoretical Computer Science, 1996. 160(1-2):1–

    work page 1996

  4. [5]

    doi:10.1016/0304-3975(95)00082-8

    work page doi:10.1016/0304-3975(95)00082-8

  5. [7]

    Reasoning algebraically about loops

    Back RJR, von Wright J. Reasoning algebraically about loops. Acta Informatica , 1999. 36(4):295–334. doi:10.1007/s002360050163

    work page doi:10.1007/s002360050163 1999

  6. [8]

    Kleene algebra with tests

    Kozen D. Kleene algebra with tests. ACM Transactions on Programming Languages and Sys- tems, 1997. 19(3):427–443. doi:10.1145/256167.256195

    work page doi:10.1145/256167.256195 1997

  7. [9]

    A completeness theorem for Kleene algebras and the algebra of regular events

    Kozen D. A completeness theorem for Kleene algebras and the algebra of regular events. Infor- mation and Computation, 1994. 110(2):366–390. doi:10.1006/inco.1994.1037

    work page doi:10.1006/inco.1994.1037 1994

  8. [10]

    Regular Algebra Applied to Path-finding Problems.Journal of the In- stitute of Mathematics and its Applications, 1975

    Backhouse RC, Carr ´e BA. Regular Algebra Applied to Path-finding Problems.Journal of the In- stitute of Mathematics and its Applications, 1975. 15(2):161–186. doi:10.1093/imamat/15.2.161

    work page doi:10.1093/imamat/15.2.161 1975

  9. [11]

    Combining relational calculus and the Dijkstra–Gries method for deriving relational programs

    Berghammer R. Combining relational calculus and the Dijkstra–Gries method for deriving relational programs. Information Sciences , 1999. 119(3-4):155–171. doi:10.1016/S0020- 0255(99)00012-2

    work page doi:10.1016/s0020- 1999

  10. [12]

    Relation-Algebraic Derivation of Spanning Tree Algo- rithms

    Berghammer R, von Karger B, Wolf A. Relation-Algebraic Derivation of Spanning Tree Algo- rithms. In: Jeuring J (ed.), Mathematics of Program Construction (MPC 1998), volume 1422 of Lecture Notes in Computer Science. Springer, 1998 pp. 23–43. doi:10.1007/BFb0054283

    work page doi:10.1007/bfb0054283 1998

  11. [13]

    Bayesian Segmentation of Atrium Wall Using Globally-Optimal Graph Cuts on 3D Meshes

    Berghammer R, Struth G. On Automated Program Construction and Verification. In: Bolduc C, Desharnais J, Ktari B (eds.), Mathematics of Program Construction (MPC 2010), volume 6120 of Lecture Notes in Computer Science. Springer, 2010 pp. 22–41. doi:10.1007/978-3-642- 13321-3 4

    work page doi:10.1007/978-3-642- 2010

  12. [14]

    Behavior,

    Gondran M, Minoux M. Graphs, Dioids and Semirings. Springer, 2008. doi:10.1007/978-0-387- 75450-5. W. Guttmann / Relation-Algebraic Verification of Disjoint-Set Forests 117

    work page doi:10.1007/978-0-387- 2008

  13. [15]

    Dijkstra, Floyd and Warshall meet Kleene

    H ¨ofner P, M¨oller B. Dijkstra, Floyd and Warshall meet Kleene. Formal Aspects of Computing,

    work page

  14. [16]

    doi:10.1007/s00165-012-0245-4

    24(4):459–476. doi:10.1007/s00165-012-0245-4

    work page doi:10.1007/s00165-012-0245-4

  15. [17]

    Derivation of Graph and Pointer Algorithms

    M ¨oller B. Derivation of Graph and Pointer Algorithms. In: M ¨oller B, Partsch HA, Schuman SA (eds.), Formal Program Development, volume 755 of Lecture Notes in Computer Science . Springer, 1993 pp. 123–160. doi:10.1007/3-540-57499-9 19

    work page doi:10.1007/3-540-57499-9 1993

  16. [18]

    Algebra of Programming

    Bird R, de Moor O. Algebra of Programming. Prentice Hall, 1997. ISBN-10:013507245X, 13:978-0135072455

    work page 1997

  17. [19]

    An Axiomatic Basis for Computer Programming

    Hoare CAR. An Axiomatic Basis for Computer Programming. Communications of the ACM ,

    work page

  18. [20]

    doi:10.1145/363235.363259

    12(10):576–580/583. doi:10.1145/363235.363259

    work page doi:10.1145/363235.363259

  19. [21]

    Introduction to Algorithms

    Cormen TH, Leiserson CE, Rivest RL. Introduction to Algorithms. MIT Press, 1990. ISBN- 10:0262031418, 13:978-0262031417

    work page 1990

  20. [22]

    Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science

    Nipkow T, Paulson LC, Wenzel M. Isabelle/HOL: A Proof Assistant for Higher-Order Logic, volume 2283 of Lecture Notes in Computer Science. Springer, 2002. doi:10.1007/3-540-45949-9

    work page doi:10.1007/3-540-45949-9 2002

  21. [23]

    Relational Disjoint Set Forests

    Guttmann W. Relational Disjoint Set Forests. Archive of Formal Proofs, 2020. First version 2020–08–26, updated 2021–06–19 and 2022–09–19 and 2023–08–10 and 2024–01–10, URL https://www.isa-afp.org/entries/Relational Disjoint Set Forests.html

    work page 2020

  22. [24]

    Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers

    Paulson LC, Blanchette JC. Three Years of Experience with Sledgehammer, a Practical Link between Automatic and Interactive Theorem Provers. In: Sutcliffe G, Ternovska E, Schulz S (eds.), Proceedings of the 8th International Workshop on the Implementation of Logics. 2010 pp. 3–13. doi:10.29007/36dt

    work page doi:10.29007/36dt 2010

  23. [25]

    Maximum Segment Sum is Back

    Mu SC. Maximum Segment Sum is Back. In: Gl ¨uck R, de Moor O (eds.), Proceedings of the 2008 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manip- ulation (PEPM 2008). ACM, 2008 pp. 31–39. doi:10.1145/1328408.1328414

    work page doi:10.1145/1328408.1328414 2008

  24. [26]

    An Algebraic Framework for Minimum Spanning Tree Problems

    Guttmann W. An Algebraic Framework for Minimum Spanning Tree Problems. Theoretical Computer Science, 2018. 744:37–55. doi:10.1016/j.tcs.2018.04.012

    work page doi:10.1016/j.tcs.2018.04.012 2018

  25. [27]

    On the calculus of relations

    Tarski A. On the calculus of relations. The Journal of Symbolic Logic , 1941. 6(3):73–89. doi:10.2307/2268577

    work page doi:10.2307/2268577 1941

  26. [28]

    Towards pointer algebra

    M ¨oller B. Towards pointer algebra. Science of Computer Programming , 1993. 21(1):57–90. doi:10.1016/0167-6423(93)90008-D

    work page doi:10.1016/0167-6423(93)90008-d 1993

  27. [29]

    Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem

    Foster JN, Greenwald MB, Moore JT, Pierce BC, Schmitt A. Combinators for Bidirectional Tree Transformations: A Linguistic Approach to the View-Update Problem. ACM Transactions on Programming Languages and Systems, 2007. 29(3:17):1–65. doi:10.1145/1232420.1232424

    work page doi:10.1145/1232420.1232424 2007

  28. [30]

    An Improved Equivalence Algorithm

    Galler BA, Fisher MJ. An Improved Equivalence Algorithm. Communications of the ACM ,

    work page

  29. [31]

    doi:10.1145/364099.364331

    7(5):301–303. doi:10.1145/364099.364331. 118 W. Guttmann / Relation-Algebraic Verification of Disjoint-Set Forests

    work page doi:10.1145/364099.364331

  30. [32]

    Refinement: Semantics, Languages and Applications

    Derrick J, Boiten E. Refinement: Semantics, Languages and Applications. Springer, 2018. doi:10.1007/978-3-319-92711-4

    work page doi:10.1007/978-3-319-92711-4 2018

  31. [33]

    Software Development: A Rigorous Approach

    Jones CB. Software Development: A Rigorous Approach. Prentice Hall, 1980. ISBN- 10:0138218846, 13:978-0138218843

    work page 1980

  32. [34]

    Specification and Transformation of Programs: A Formal Approach to Software Development

    Partsch HA. Specification and Transformation of Programs: A Formal Approach to Software Development. Springer, 1990. doi:10.1007/978-3-642-61512-2

    work page doi:10.1007/978-3-642-61512-2 1990

  33. [35]

    Winskel is (almost) Right: Towards a Mechanized Semantics Textbook

    Nipkow T. Winskel is (almost) Right: Towards a Mechanized Semantics Textbook. Formal Aspects of Computing, 1998. 10(2):171–186. doi:10.1007/s001650050009

    work page doi:10.1007/s001650050009 1998

  34. [36]

    Asher & D

    Nipkow T. Hoare Logics in Isabelle/HOL. In: Schwichtenberg H, Steinbr ¨uggen R (eds.), Proof and System-Reliability. Kluwer Academic Publishers, 2002 pp. 341–367. doi:10.1007/978-94- 010-0413-8 11

    work page doi:10.1007/978-94- 2002

  35. [37]

    Verifying Minimum Spanning Tree Algorithms with Stone Relation Algebras

    Guttmann W. Verifying Minimum Spanning Tree Algorithms with Stone Relation Algebras. Journal of Logical and Algebraic Methods in Programming , 2018. 101:132–150. doi:10.1016/ j.jlamp.2018.09.005

    work page 2018

  36. [38]

    Programming from specifications

    Morgan C. Programming from specifications. Prentice Hall, second edition, 1994. ISBN-10: 0131232746, 13:978-0131232747

    work page 1994

  37. [39]

    Alternative Path Compression Techniques

    van Leeuwen J, van der Weide T. Alternative Path Compression Techniques. Technical Report RUU-CS-77-3, University of Utrecht, 1977. ISSN:0924-3275

    work page 1977

  38. [40]

    Worst-Case Analysis of Set Union Algorithms

    Tarjan RE, van Leeuwen J. Worst-Case Analysis of Set Union Algorithms. Journal of the ACM,

    work page

  39. [41]

    doi:10.1145/62.2160

    31(2):245–281. doi:10.1145/62.2160

    work page doi:10.1145/62.2160

  40. [42]

    A Separation Logic Framework for Imperative HOL

    Lammich P, Meis R. A Separation Logic Framework for Imperative HOL. Archive of Formal Proofs, 2012. URL https://www.isa-afp.org/entries/Separation Logic Imperative HOL.html

    work page 2012

  41. [43]

    The (generaliz ed) Post correspondence problem with lists consisting of two words is decidable

    Berghammer R, Zierer H. Relational Algebraic Semantics of Deterministic and Nondeter- ministic Programs. Theoretical Computer Science , 1986. 43:123–147. doi:10.1016/0304- 3975(86)90172-6

    work page doi:10.1016/0304- 1986

  42. [44]

    A Relation-Algebraic Treatment of the Dedekind Recursion Theorem

    Berghammer R. A Relation-Algebraic Treatment of the Dedekind Recursion Theorem. In: Fahrenberg U, Jipsen P, Winter M (eds.), Relational and Algebraic Methods in Computer Science (RAMiCS 2020), volume 12062 of Lecture Notes in Computer Science. Springer, 2020 pp. 15–

    work page 2020

  43. [45]

    doi:10.1007/978-3-030-43520-2 2

    work page doi:10.1007/978-3-030-43520-2

  44. [46]

    On the Cardinality of Relations

    Kawahara Y . On the Cardinality of Relations. In: Schmidt RA (ed.), Relations and Kleene Al- gebra in Computer Science (RelMiCS/AKA 2006), volume 4136 of Lecture Notes in Computer Science. Springer, 2006 pp. 251–265. doi:10.1007/11828563 17

    work page doi:10.1007/11828563 2006

  45. [47]

    Towards a Mathematical Science of Computation

    McCarthy J. Towards a Mathematical Science of Computation. In: Popplewell CM (ed.), In- formation Processing (IFIP 1962), volume 2 of IFIP congress series. North-Holland Publishing Company, 1963 pp. 21–28. W. Guttmann / Relation-Algebraic Verification of Disjoint-Set Forests 119

    work page 1962

  46. [48]

    Notes on Data Structuring

    Hoare CAR. Notes on Data Structuring. In: Dahl OJ, Dijkstra EW, Hoare CAR (eds.), Structured Programming, chapter 2, pp. 83–174. Academic Press, 1972

    work page 1972

  47. [49]

    Reasoning About Arrays

    Reynolds JC. Reasoning About Arrays. Communications of the ACM , 1979. 22(5):290–299. doi:10.1145/359104.359110

    work page doi:10.1145/359104.359110 1979

  48. [50]

    The Z Notation: A Reference Manual

    Spivey JM. The Z Notation: A Reference Manual. Prentice Hall, 1989. ISBN-10:013983768X, 13:978-0139837685

    work page 1989

  49. [51]

    Specification Case Studies

    Hayes I. Specification Case Studies. Technical Report PRG-46, Programming Research Group, University of Oxford, 1985

    work page 1985

  50. [52]

    Pointer Kleene Algebra

    Ehm T. Pointer Kleene Algebra. In: Berghammer R, M ¨oller B, Struth G (eds.), Relational and Kleene-Algebraic Methods in Computer Science (RelMiCS 2003), volume 3051 of Lecture Notes in Computer Science. Springer, 2004 pp. 99–111. doi:10.1007/978-3-540-24771-5 9

    work page doi:10.1007/978-3-540-24771-5 2003

  51. [53]

    Calculating With Pointer Structures

    M ¨oller B. Calculating With Pointer Structures. In: Bird R, Meertens LGLT (eds.), Algorithmic Languages and Calculi, volume 95 of IFIP Conference Proceedings. Chapman and Hall, 1997 pp. 24–48. doi:10.1007/978-0-387-35264-0 2

    work page doi:10.1007/978-0-387-35264-0 1997

  52. [54]

    Calculating with acyclic and cyclic lists

    M ¨oller B. Calculating with acyclic and cyclic lists. Information Sciences, 1999. 119(3-4):135–

    work page 1999

  53. [55]

    doi:10.1016/S0020-0255(99)00011-0

    work page doi:10.1016/s0020-0255(99)00011-0

  54. [56]

    A Persistent Union-Find Data Structure

    Conchon S, Filli ˆatre JC. A Persistent Union-Find Data Structure. In: Dreyer D, Russo C (eds.), Proceedings of the 2007 Workshop on ML (ML 2007). ACM, 2007 pp. 37–45. doi:10.1145/1292535.1292541

    work page doi:10.1145/1292535.1292541 2007

  55. [57]

    Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits

    Chargu ´eraud A, Pottier F. Verifying the Correctness and Amortized Complexity of a Union-Find Implementation in Separation Logic with Time Credits. Journal of Automated Reasoning, 2019. 62(3):331–365. doi:10.1007/s10817-017-9431-7

    work page doi:10.1007/s10817-017-9431-7 2019

  56. [58]

    Systematic Software Development Using VDM

    Jones CB. Systematic Software Development Using VDM. Prentice Hall, second edition, 1990. ISBN-10:0138807337, 13:978-0138807337

    work page 1990

  57. [59]

    In: Proc

    Zhan B, Haslbeck MPL. Verifying Asymptotic Time Complexity of Imperative Programs in Is- abelle. In: Galmiche D, Schulz S, Sebastiani R (eds.), Automated Reasoning (IJCAR 2018), vol- ume 10900 ofLecture Notes in Computer Science. Springer, 2018 pp. 532–548. doi:10.1007/978- 3-319-94205-6 35

    work page doi:10.1007/978- 2018

  58. [60]

    For a Few Dollars More: Verified Fine-Grained Algorithm Anal- ysis Down to LLVM

    Haslbeck MPL, Lammich P. For a Few Dollars More: Verified Fine-Grained Algorithm Anal- ysis Down to LLVM. ACM Transactions on Programming Languages and Systems , 2022. 44(3:14):1–36. doi:10.1145/3486169

    work page doi:10.1145/3486169 2022

  59. [61]

    Building program construction and verification tools from algebraic principles

    Armstrong A, Gomes VBF, Struth G. Building program construction and verification tools from algebraic principles. Formal Aspects of Computing, 2016. 28(2):265–293. doi:10.1007/s00165- 015-0343-1. 120 W. Guttmann / Relation-Algebraic Verification of Disjoint-Set Forests

    work page doi:10.1007/s00165- 2016

  60. [62]

    Relational Mathematics

    Schmidt G. Relational Mathematics. Cambridge University Press, 2011. ISBN-10:0521762685, 13:978-0521762687. doi:10.1017/CBO9780511778810

    work page doi:10.1017/cbo9780511778810 2011

  61. [63]

    Kruskal’s Algorithm for Minimum Spanning Forest

    Haslbeck MPL, Lammich P, Biendarra J. Kruskal’s Algorithm for Minimum Spanning Forest. Archive of Formal Proofs, 2019. URL https://www.isa-afp.org/entries/Kruskal.html

    work page 2019