Document Open Access Logo

Defining Corecursive Functions in Coq Using Approximations

Authors Vlad Rusu , David Nowak



PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.12.pdf
  • Filesize: 0.82 MB
  • 24 pages

Document Identifiers

Author Details

Vlad Rusu
  • Inria, Lille, France
David Nowak
  • Univ. Lille, CNRS, Centrale Lille, UMR 9189 CRIStAL, F-59000 Lille, France

Cite AsGet BibTex

Vlad Rusu and David Nowak. Defining Corecursive Functions in Coq Using Approximations. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 12:1-12:24, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.ECOOP.2022.12

Abstract

We present two methods for defining corecursive functions that go beyond what is accepted by the builtin corecursion mechanisms of the Coq proof assistant. This gain in expressiveness is obtained by using a combination of axioms from Coq’s standard library that, to our best knowledge, do not introduce inconsistencies but enable reasoning in standard mathematics. Both methods view corecursive functions as limits of sequences of approximations, and both are based on a property of productiveness that, intuitively, requires that for each input, an arbitrarily close approximation of the corresponding output is eventually obtained. The first method uses Coq’s builtin corecursive mechanisms in a non-standard way, while the second method uses none of the mechanisms but redefines them. Both methods are implemented in Coq and are illustrated with examples.

Subject Classification

ACM Subject Classification
  • Theory of computation → Functional constructs
Keywords
  • corecursive function
  • productiveness
  • approximation
  • Coq proof assistant

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads

References

  1. The Coq Proof Assistant. URL: https://coq.inria.fr/.
  2. S. Banach. Sur les opérations dans les ensembles abstraits et leur applications aux équations intégrales. Fundam. Math., 3:133-181, 1922. Google Scholar
  3. Y. Bertot. Filters on coinductive streams, an application to Eratosthenes' sieve. In Typed Lambda Calculi and Applications, 7th International Conference, TLCA 2005, Nara, Japan, April 21-23, 2005, Proceedings, volume 3461 of Lecture Notes in Computer Science, pages 102-115, 2005. Google Scholar
  4. Y. Bertot and E. Komendantskaya. Inductive and coinductive components of corecursive functions in Coq. In Proceedings of the Ninth Workshop on Coalgebraic Methods in Computer Science, CMCS 2008, Budapest, Hungary, April 4-6, 2008, volume 203 of Electronic Notes in Theoretical Computer Science, pages 25-47, 2008. Google Scholar
  5. Y. Bertot and V. Komendantsky. Fixed point semantics and partial recursion in Coq. In Proceedings of the 10th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, July 15-17, 2008, Valencia, Spain, pages 89-96, 2008. Google Scholar
  6. J. Biendarra, J. C. Blanchette, M. Desharnais, L. Panny, A. Popescu, and D. Traytel. Defining (Co)datatypes and Primitively (Co)recursive Functions in Isabelle/HOL. URL: https://isabelle.in.tum.de/doc/datatypes.pdf.
  7. J. C. Blanchette, A. Bouzy, A. Lochbihler, A. Popescu, and D. Traytel. Defining Nonprimitively (Co)recursive Functions in Isabelle/HOL. URL: https://isabelle.in.tum.de/dist/Isabelle2021/doc/corec.pdf.
  8. A. Chlipala. Certified Programming with Dependent Types. MIT Press, 2013. Google Scholar
  9. J. Forget. A Synchronous Language for Critical Embedded Systems with Multiple Real-Time Constraints. PhD thesis, Institut Supérieur de l’Aéronautique et de l’Espace, Toulouse, France, 2009. Google Scholar
  10. S. R. Ghorpade and B. V. Limaye. A Course in Calculus and Real Analysis. Undergraduate Texts in Mathematics. Springer, 2018. Google Scholar
  11. E. Giménez. Codifying guarded definitions with recursive schemes. In Types for Proofs and Programs, International Workshop TYPES'94, Båstad, Sweden, June 6-10, 1994, Selected Papers, volume 996 of Lecture Notes in Computer Science, pages 39-59. Springer, 1994. Google Scholar
  12. C.-K. Hur, G. Neis, D. Dreyer, and V. Vafeiadis. The power of parameterization in coinductive proof. In The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 193-206. ACM, 2013. Google Scholar
  13. D. Kozen and N. Ruozzi. Applications of metric coinduction. Log. Methods Comput. Sci., 5(3), 2009. Google Scholar
  14. The Lean Proof Assistant. URL: https://leanprover.github.io/.
  15. K. Rustan M. Leino and M. Moskal. Co-induction simply - automatic co-inductive proofs in a program verifier. In FM 2014: Formal Methods - 19th International Symposium, Singapore, May 12-16, 2014. Proceedings, volume 8442 of Lecture Notes in Computer Science, pages 382-398. Springer, 2014. Google Scholar
  16. C. Paulin-Mohring. A constructive denotational semantics for Kahn networks in Coq. Available at URL: https://www.lri.fr/~paulin/PUBLIS/paulin07kahn.pdf.
  17. T. Uustalu and V. Vene. The essence of dataflow programming. In Programming Languages and Systems, Third Asian Symposium, APLAS 2005, Tsukuba, Japan, November 2-5, 2005, Proceedings, volume 3780 of Lecture Notes in Computer Science, pages 2-18. Springer, 2005. Google Scholar
  18. N. Veltri and N. van der Weide. Guarded recursion in agda via sized types. In 4th International Conference on Formal Structures for Computation and Deduction, FSCD 2019, June 24-30, 2019, Dortmund, Germany, volume 131 of LIPIcs, pages 32:1-32:19. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2019. Google Scholar
  19. G. Winskel. The Formal Semantics of Programming Languages, an introduction. MIT Press, 1993. Google Scholar
  20. The Agda Proof Assistant. URL: https://agda.readthedocs.io/en/v2.6.2/getting-started/what-is-agda.html.
  21. The Isabelle/HOL Proof Assistant. URL: https://isabelle.in.tum.de/.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail