Executable Transitive Closures of Finite Relations

Christian Sternagel and René Thiemann

The Archive of Formal Proofs, 2011. 



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.


  AFP entry


author = "Christian Sternagel and Ren{\'e} Thiemann",
title = "{E}xecutable {T}ransitive {C}losures of {F}inite {R}elations",
booktitle = "The Archive of Formal Proofs",
editor = "Gerwin Klein and Tobias Nipkow and Lawrence Paulson",
publisher = "\url{}",
year = 2011,
month = mar,
note = "Formal proof development"
ISSN = "2150-914x",
Nach oben scrollen