nach oben

Erschienen in:

2018 | OriginalPaper | Buchkapitel

Proof Pearl: Constructive Extraction of Cycle Finding Algorithms

verfasst von : Dominique Larchey-Wendling

Erschienen in: Interactive Theorem Proving

Verlag: Springer International Publishing

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

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.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Software Verification with ITPs Should Use Binary Code Extraction to Reduce the TCB

Nächstes Kapitel Fast Machine Words in Isabelle/HOL

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

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

Descending induction is implemented by

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94821-8_22/470383_1_En_22_IEq142_HTML.gif

in file utils.v .

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

See th_rel.v where an arbitrary decidable relation

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94821-8_22/470383_1_En_22_IEq163_HTML.gif

replaces \(=_X\).

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

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-319-94821-8_22/470383_1_En_22_IEq254_HTML.gif

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

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-4CrossRefMATH

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-5CrossRefMATH

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

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

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

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

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

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)

15.

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

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

Titel: Proof Pearl: Constructive Extraction of Cycle Finding Algorithms
verfasst von: Dominique Larchey-Wendling
Verlag: Springer International Publishing
Buch: Interactive Theorem Proving
Print ISBN: 978-3-319-94820-1

Electronic ISBN: 978-3-319-94821-8

Copyright-Jahr: 2018
DOI: https://doi.org/10.1007/978-3-319-94821-8_22

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner