Analysing the CHR Implementation of Union-Find
Tom Schrijvers, Thom Frühwirth · Lirias · 2005
CHR (Constraint Handling Rules) is a committed-choice rule-based language that was originally intended for writing constraint solvers. Over time, CHR is used more and more as a general-purpose programming language. In companion paper [12] we show that it is possible to write the classic union-find algorithm and variants in CHR with bestknown time complexity, which is believed impossible in Prolog. In this paper, using CHR analysis techniques, we study logical correctness and confluence of these programs. We observe the essential destructive update of the algorithm which makes it non-logical.