### Abstract

We provide a generic work-list algorithm to compute the (reflexive-)transitive closure of relations where only successors of newly detected states are generated. In contrast to our previous work, the relations do not have to be finite, but each element must only have finitely many (indirect) successors. Moreover, a subsumption relation can be used instead of pure equality. An executable variant of the algorithm is available where the generic operations are instantiated with list operations.

This formalization was performed as part of the IsaFoR/CeTA project, and it has been used to certify size-change termination proofs where large transitive closures have to be computed.

### License

GNU Lesser General Public License (LGPL)

### Topics

- Computer science/Algorithms/Graph

### Session Transitive-Closure-II

- RTrancl

### Depends on

- Regular Sets and Expressions

### Auto-related entries

- Executable Transitive Closures of Finite Relations
- A Generic Framework for Verified Compilers
- Deriving class instances for datatypes
- Certification Monads
- XML

## Cite

×

Transitive-Closure-II-AFP

    @article{Transitive-Closure-II-AFP,
      author  = {René Thiemann},
      title   = {Executable Transitive Closures},
      journal = {Archive of Formal Proofs},
      month   = {February},
      year    = {2012},
      note    = {\url{https://isa-afp.org/entries/Transitive-Closure-II.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 20, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Feb 22, 2016 : Isabelle2016
- May 27, 2015 : Isabelle2015
- Aug 28, 2014 : Isabelle2014
- Dec 11, 2013 : Isabelle2013-2
- Nov 17, 2013 : Isabelle2013-1
- Feb 16, 2013 : Isabelle2013
- May 24, 2012 : Isabelle2012
- Mar 15, 2012 : Isabelle2011-1
- Feb 29, 2012 : Isabelle2011-1