Document Open Access Logo

Flexible Coinduction in Agda

Authors Luca Ciccone , Francesco Dagnino , Elena Zucca

PDF
Thumbnail PDF

File

LIPIcs.ITP.2021.13.pdf
  • Filesize: 0.79 MB
  • 19 pages

Document Identifiers

Author Details

Luca Ciccone
  • University of Torino, Italy
Francesco Dagnino
  • DIBRIS, University of Genova, Italy
Elena Zucca
  • DIBRIS, University of Genova, Italy

Acknowledgements

We warmly thank the anonymous ITP reviewers and Andreas Abel for the suggestions which greatly improved the paper, in particular for pointing out the relation with indexed containers.

Cite AsGet BibTex

Luca Ciccone, Francesco Dagnino, and Elena Zucca. Flexible Coinduction in Agda. In 12th International Conference on Interactive Theorem Proving (ITP 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 193, pp. 13:1-13:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.ITP.2021.13

Abstract

We provide an Agda library for inference systems, also supporting their recent generalization allowing flexible coinduction, that is, interpretations which are neither inductive, nor purely coinductive. A specific inference system can be obtained as an instance by writing a set of meta-rules, in an Agda format which closely resembles the usual one. In this way, the user gets for free the related properties, notably the inductive and coinductive intepretation and the corresponding proof principles. Moreover, a significant modularity is achieved. Indeed, rather than being defined from scratch and with a built-in interpretation, an inference system can also be obtained by composition operators, such as union and restriction to a smaller universe, and its semantics can be modularly chosen as well. In particular, flexible coinduction is obtained by composing in a certain way the interpretations of two inference systems. We illustrate the use of the library by several examples. The most significant one is a big-step semantics for the λ-calculus, where flexible coinduction allows to obtain a special result (∞) for all and only the diverging computations, and the proof of equivalence with small-step semantics is carried out by relying on the proof principles offered by the library.

Subject Classification

ACM Subject Classification
  • Theory of computation → Semantics and reasoning
Keywords
  • inference systems
  • induction
  • coinduction

Metrics

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

Supplementary Materials

References

  1. Andreas Abel. Type-based termination, inflationary fixed-points, and mixed inductive-coinductive types. In Dale Miller and Zoltán Ésik, editors, Proceedings 8th Workshop on Fixed Points in Computer Science, FICS 2012, volume 77 of EPTCS, pages 1-11, 2012. URL: https://doi.org/10.4204/EPTCS.77.1.
  2. Andreas Abel and Brigitte Pientka. Well-founded recursion with copatterns and sized types. Journal of Functional Programming, 26:e2, 2016. URL: https://doi.org/10.1017/S0956796816000022.
  3. Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: programming infinite structures by observations. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM Symposium on Principles of Programming Languages, POPL'13, pages 27-38. ACM Press, 2013. URL: https://doi.org/10.1145/2429069.2429075.
  4. Andreas Abel, Andrea Vezzosi, and Théo Winterhalter. Normalization by evaluation for sized dependent types. Proceedings of ACM on Programming Languages, 1(ICFP):33:1-33:30, 2017. URL: https://doi.org/10.1145/3110277.
  5. Peter Aczel. An introduction to inductive definitions. In Jon Barwise, editor, Handbook of Mathematical Logic, volume 90 of Studies in Logic and the Foundations of Mathematics, pages 739-782. Elsevier, 1977. Google Scholar
  6. Thorsten Altenkirch, Neil Ghani, Peter G. Hancock, Conor McBride, and Peter Morris. Indexed containers. Journal of Functional Programming, 25, 2015. URL: https://doi.org/10.1017/S095679681500009X.
  7. Davide Ancona, Francesco Dagnino, Jurriaan Rot, and Elena Zucca. A big step from finite to infinite computations. Science of Computer Programming, 197:102492, 2020. URL: https://doi.org/10.1016/j.scico.2020.102492.
  8. Davide Ancona, Francesco Dagnino, and Elena Zucca. Generalizing inference systems by coaxioms. In Hongseok Yang, editor, Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, volume 10201 of Lecture Notes in Computer Science, pages 29-55, Berlin, 2017. Springer. URL: https://doi.org/10.1007/978-3-662-54434-1_2.
  9. Davide Ancona, Francesco Dagnino, and Elena Zucca. Reasoning on divergent computations with coaxioms. Proceedings of ACM on Programming Languages, 1(OOPSLA):81:1-81:26, 2017. URL: https://doi.org/10.1145/3133905.
  10. Davide Ancona, Francesco Dagnino, and Elena Zucca. Modeling infinite behaviour by corules. In Todd D. Millstein, editor, 32nd European Conference on Object-Oriented Programming, ECOOP 2018, volume 109 of LIPIcs, pages 21:1-21:31, Dagstuhl, 2018. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2018.21.
  11. G. Bracha. The Programming Language JIGSAW: Mixins, Modularity and Multiple Inheritance. PhD thesis, Department of Comp. Sci., Univ. of Utah, 1992. Google Scholar
  12. Luca Ciccone. Flexible coinduction in Agda. Master’s thesis, University of Genova, 2019. URL: https://arxiv.org/abs/2002.06047.
  13. Francesco Dagnino. Coaxioms: flexible coinductive definitions by inference systems. Logical Methods in Computer Science, 15(1), 2019. URL: https://doi.org/10.23638/LMCS-15(1:26)2019.
  14. Francesco Dagnino. Foundations of regular coinduction. Technical report, DIBRIS, University of Genova, June 2020. Submitted for journal publication. URL: https://arxiv.org/abs/2006.02887.
  15. Francesco Dagnino. Flexible Coinduction. PhD thesis, DIBRIS, University of Genova, 2021. Google Scholar
  16. Nils Anders Danielsson. Up-to techniques using sized types. Proceedings of ACM on Programming Languages, 2(POPL):43:1-43:28, 2018. URL: https://doi.org/10.1145/3158131.
  17. Denis Firsov and Tarmo Uustalu. Dependently typed programming with finite sets. In Patrick Bahr and Sebastian Erdweg, editors, Proceedings of the 11th ACM Workshop on Generic Programming, WGP@ICFP 2015, pages 33-44. ACM, 2015. URL: https://doi.org/10.1145/2808098.2808102.
  18. Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The power of parameterization in coinductive proof. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM Symposium on Principles of Programming Languages, POPL'13, pages 193-206. ACM Press, 2013. URL: https://doi.org/10.1145/2429069.2429093.
  19. Xavier Leroy and Hervé Grall. Coinductive big-step operational semantics. Information and Computation, 207(2):284-304, 2009. URL: https://doi.org/10.1016/j.ic.2007.12.004.
  20. Damien Pous. Coinduction all the way up. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS'16, pages 307-316. ACM Press, 2016. URL: https://doi.org/10.1145/2933575.2934564.
  21. Davide Sangiorgi. Introduction to Bisimulation and Coinduction. Cambridge University Press, USA, 2011. Google Scholar
  22. Régis Spadotti. A mechanized theory of regular trees in dependent type theory. (Une théorie mécanisée des arbres réguliers en théorie des types dépendants). PhD thesis, Paul Sabatier University, Toulouse, France, 2016. URL: https://tel.archives-ouvertes.fr/tel-01589656.
  23. The Agda Team. The Agda Reference Manual. URL: http://agda.readthedocs.io/en/latest/index.html.
  24. Tarmo Uustalu and Niccolò Veltri. Finiteness and rational sequences, constructively. Journal of Functional Programming, 27:e13, 2017. URL: https://doi.org/10.1017/S0956796817000041.
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
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact