Proof Pearl: Constructive Extraction of Cycle Finding Algorithms

Perle de programmation: extraction constructive d'algorithme de recherche de cycles

Dominique Larchey-Wendling (1)

1 TYPES - Logic, Proof Theory and Programming

We present a short implementation of the well-known Tortoise and Hare cycle finding algorithm in the constructive setting of Coq. This algorithm is interesting from a constructive perspective because it is both very simple and potentially non-terminating (depending on the input). To overcome potential non-termination, we encode the given termination argument (there exists a cycle) into a bar inductive predicate that we use as termination certificate. From this development, we extract the standard OCaml implementation of this algorithm. We generalize the method to the full Floyd’s algorithm that computes the entry point and the period of the cycle in the iterated sequence, and to the more efficient Brent’s algorithm for computing the period only, again with accurate extractions of their respective standard OCaml implementations.

Mots clés: Partial algorithms in Coq; Bar inductive predicates; Cycle finding; Correctness by extraction

Domaines: Langage de programmation [cs.PL]; Génie logiciel [cs.SE]; Logique en informatique [cs.LO]

Dominique Larchey-Wendling. Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. 9th International Conference on Interactive Theorem Proving, ITP 2018, Jul 2018, Oxford, United Kingdom. pp.370-387, ⟨10.1007/978-3-319-94821-8_22⟩. ⟨hal-02333354⟩