From: Tobias Nipkow <nipkow@in.tum.de>
Executable Transitive Closures of Finite Relations
Christian Sternagel and René Thiemann
We provide a generic work-list algorithm to compute the transitive 
closure of finite relations where only successors of newly detected 
states are generated. This algorithm is then instantiated for lists over 
arbitrary carriers and red black trees (which are faster but require a 
linear order on the carrier), respectively. Our formalization was 
performed as part of the IsaFoR/CeTA project where reflexive transitive 
closures of large tree automata have to be computed.
http://afp.sourceforge.net/entries/Transitive-Closure.shtml
Last updated: Oct 31 2025 at 12:44 UTC