LIPIcs.ITP.2023.21.pdf
- Filesize: 0.65 MB
- 17 pages
Document
Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq
Authors
-
Part of:
Volume:
14th International Conference on Interactive Theorem Proving (ITP 2023)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2023-07-26
Cite AsGet BibTex
Dominique Larchey-Wendling and Jean-François Monin. Proof Pearl: Faithful Computation and Extraction of μ-Recursive Algorithms in Coq. In 14th International Conference on Interactive Theorem Proving (ITP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 268, pp. 21:1-21:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)
https://doi.org/10.4230/LIPIcs.ITP.2023.21
https://doi.org/10.4230/LIPIcs.ITP.2023.21
Abstract
Basing on an original Coq implementation of unbounded linear search for partially decidable predicates, we study the computational contents of μ-recursive functions via their syntactic representation, and a correct by construction Coq interpreter for this abstract syntax. When this interpreter is extracted, we claim the resulting OCaml code to be the natural combination of the implementation of the μ-recursive schemes of composition, primitive recursion and unbounded minimization of partial (i.e., possibly non-terminating) functions. At the level of the fully specified Coq terms, this implies the representation of higher-order functions of which some of the arguments are themselves partial functions. We handle this issue using some techniques coming from the Braga method. Hence we get a faithful embedding of μ-recursive algorithms into Coq preserving not only their extensional meaning but also their intended computational behavior. We put a strong focus on the quality of the Coq artifact which is both self contained and with a line of code count of less than 1k in total.
Subject Classification
ACM Subject Classification
- Theory of computation → Models of computation
- Theory of computation → Type theory
- Theory of computation → Functional constructs
- Software and its engineering → Formal methods
- Software and its engineering → Functional languages
- Theory of computation → Higher order logic
Keywords
- Unbounded linear search
- μ-recursive functions
- computational contents
- Coq
- extraction
- OCaml
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- George S. Boolos, John P. Burgess, and Richard C. Jeffrey. Computability and Logic. Cambridge University Press, 4 edition, 2002. URL: https://doi.org/10.1017/CBO9781139164931.
- Mario Carneiro. Formalizing Computability Theory via Partial Recursive Functions. In ITP 2019, volume 141, pages 12:1-12:17. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik, 2019. URL: https://doi.org/10.4230/LIPIcs.ITP.2019.12.
-
Robert L. Constable et al. Implementing Mathematics with the Nuprl Development System. Prentice-Hall, NJ, 1986.
- Yannick Forster. Church’s Thesis and Related Axioms in Coq’s Type Theory. In CSL 2021, volume 183, pages 21:1-21:19. Schloss Dagstuhl-Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.21.
-
Yannick Forster. Parametric church’s thesis: Synthetic computability without choice. In Sergei Artemov and Anil Nerode, editors, Logical Foundations of Computer Science, pages 70-89, Cham, 2022. Springer International Publishing.
-
Susumu Hayashi. Extracting Lisp Programs from Constructive Proofs: A Formal Theory of Constructive Mathematic Based on Lisp, volume 19, pages 169-191. Publications of the Research Institute for Mathematical Sciences, 1983.
- Stephen C. Kleene. λ-definability and recursiveness. Duke Mathematical Journal, 2(2):340-353, 1936. URL: https://doi.org/10.1215/S0012-7094-36-00227-2.
- Stephen C. Kleene. Recursive predicates and quantifiers. Trans. Amer. Math. Soc., 53:43-73, 1943. URL: https://doi.org/10.1090/S0002-9947-1943-0007371-8.
- Dominique Larchey-Wendling. Typing Total Recursive Functions in Coq. In ITP 2017, pages 371-388. Springer, 2017. URL: https://doi.org/10.1007/978-3-319-66107-0_24.
- Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq (Extended Version). Logical Methods in Computer Science, Volume 18, Issue 1:35:1-35:41, March 2022. URL: https://doi.org/10.46298/lmcs-18(1:35)2022.
- Dominique Larchey-Wendling and Jean-François Monin. The Braga Method: Extracting Certified Algorithms from Complex Recursive Schemes in Coq, chapter 8, pages 305-386. World Scientific, 2021. URL: https://doi.org/10.1142/9789811236488_0008.
-
Joseph R. Shoenfield. Mathematical Logic. Addison-Wesley series in logic. Addison-Wesley, 1967.
- Vincent Zammit. A Proof of the S-m-n theorem in Coq. Technical report, The Computing Laboratory, The University of Kent, Canterbury, Kent, UK, March 1997. URL: http://kar.kent.ac.uk/21524/.