Skip to main content
SpringerLink
Log in

Proof Pearl: Constructive Extraction of Cycle Finding Algorithms

  • Conference paper
  • First Online:
Interactive Theorem Proving (ITP 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10895))

Included in the following conference series:

Abstract

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.

Work partially supported by the TICAMORE project ANR grant 16-CE91-0002.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 79.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 99.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    OCaml equality decider is partially correct, e.g. it throws exceptions on functions.

  2. 2.

    Conventional bar induction often requires Brouwer’s thesis which precisely postulates that bar predicates are inductive.

  3. 3.

    Descending induction is implemented by in file utils.v .

  4. 4.

    For \(=_X\), this is precisely the assumption of the \(\mathrel {=^?_X}\) equality decider.

  5. 5.

    See  th_rel.v where an arbitrary decidable relation replaces \(=_X\).

  6. 6.

    Least for the natural order \(\mathrel {\leqslant }\) over .

References

  1. Cycle detection – Wikipedia, The Free Encyclopedia. https://en.wikipedia.org/wiki/Cycle_detection

  2. Aumasson, J.-P., Meier, W., Phan, R.C.-W., Henzen, L.: The Hash Function BLAKE. ISC. Springer, Heidelberg (2014). https://doi.org/10.1007/978-3-662-44757-4

    Book  MATH  Google Scholar 

  3. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development - Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. An EATCS Series. Springer, Heidelberg (2004). https://doi.org/10.1007/978-3-662-07964-5

    Book  MATH  Google Scholar 

  4. Bove, A., Capretta, V.: Modelling general recursion in type theory. Math. Structures Comput. Sci. 15(4), 671–708 (2005). https://doi.org/10.1017/S0960129505004822

  5. Bove, A., Krauss, A., Sozeau, M.: Partiality and recursion in interactive theorem provers – an overview. Math. Structures Comput. Sci. 26(1), 38–88 (2016). https://doi.org/10.1017/S0960129514000115

  6. Brent, R.P.: An improved Monte Carlo factorization algorithm. BIT Numer. Math. 20(2), 176–184 (1980). https://doi.org/10.1007/BF01933190

  7. Castéran, P.: Utilisation en Coq de l’opérateur de description (2007). http://jfla.inria.fr/2007/actes/PDF/03_casteran.pdf

  8. Coen, C.S., Valentini, S.: General Recursion and Formal Topology. In: PAR-2010, Partiality and Recursion in Interactive Theorem Provers. EPiC Series in Computing, vol. 5, pp. 72–83. EasyChair (2012). https://doi.org/10.29007/hl75

  9. Dufourd, J.F.: Formal study of functional orbits in finite domains. Theoret. Comput. Sci. 564, 63–88 (2015). https://doi.org/10.1016/j.tcs.2014.10.041

  10. Dybjer, P.: A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log. 65(2), 525–549 (2000). https://doi.org/10.2307/2586554

  11. Filliâtre, J.C.: Tortoise and the hare algorithm (2007). https://github.com/coq-contribs/tortoise-hare-algorithm

  12. Fridlender, D.: An interpretation of the fan theorem in type theory. In: Altenkirch, T., Reus, B., Naraschewski, W. (eds.) TYPES 1998. LNCS, vol. 1657, pp. 93–105. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-48167-2_7

  13. Gammie, P.: The Tortoise and Hare Algorithm (2015). https://www.isa-afp.org/entries/TortoiseHare.html

  14. Joux, A.: Algorithmic Cryptanalysis. Cryptography and Network Security. Chapman & Hall/CRC (2009)

    Google Scholar 

  15. Knuth, D.E.: The Art of Computer Programming, Volume 2: Seminumerical Algorithms. Addison-Wesley Longman Publishing Co., Inc., Boston (1997)

    Google Scholar 

  16. Lagarias, J.: The Ultimate Challenge: The \(3x+1\) Problem. American Mathematical Society (2010). http://bookstore.ams.org/mbk-78

  17. Larchey-Wendling, D., Monin, J.F.: Simulating Induction-Recursion for Partial Algorithms. In: TYPES 2018, Braga, Portugal (2018). https://members.loria.fr/DLarchey/files/papers/TYPES_2018_paper_19.pdf

  18. Pollard, J.M.: A monte carlo method for factorization. BIT Numer. Math. 15(3), 331–334 (1975). https://doi.org/10.1007/BF01933667

Download references

Author information

Authors and Affiliations

  1. Université de Lorraine, CNRS, LORIA, Nancy, France

    Dominique Larchey-Wendling

Authors
  1. Dominique Larchey-Wendling
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dominique Larchey-Wendling .

Editor information

Editors and Affiliations

  1. Carnegie Mellon University, Pittsburgh, PA, USA

    Jeremy Avigad

  2. Inria, Nantes, France

    Assia Mahboubi

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer International Publishing AG, part of Springer Nature

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Larchey-Wendling, D. (2018). Proof Pearl: Constructive Extraction of Cycle Finding Algorithms. In: Avigad, J., Mahboubi, A. (eds) Interactive Theorem Proving. ITP 2018. Lecture Notes in Computer Science(), vol 10895. Springer, Cham. https://doi.org/10.1007/978-3-319-94821-8_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-94821-8_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-94820-1

  • Online ISBN: 978-3-319-94821-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation