Document Open Access Logo

Coinduction in Flow: The Later Modality in Fibrations

Author Henning Basold

PDF
Thumbnail PDF

File

LIPIcs.CALCO.2019.8.pdf
  • Filesize: 0.59 MB
  • 22 pages

Document Identifiers

Author Details

Henning Basold
  • CNRS, ENS de Lyon, France
  • LIACS - Leiden University, The Netherlands

Funding

  • Basold, Henning: This work has been funded by the European Research Council (ERC) under the EU’s Horizon 2020 programme (CoVeCe, grant agreement No 678157), and was supported by the LABEX MILYON (ANR-10-LABX-0070) of Université de Lyon, within the program "Investissements d'Avenir" (ANR-11-IDEX-0007) operated by the French National Research Agency (ANR).

Cite AsGet BibTex

Henning Basold. Coinduction in Flow: The Later Modality in Fibrations. In 8th Conference on Algebra and Coalgebra in Computer Science (CALCO 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 139, pp. 8:1-8:22, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.CALCO.2019.8

Abstract

This paper provides a construction on fibrations that gives access to the so-called later modality, which allows for a controlled form of recursion in coinductive proofs and programs. The construction is essentially a generalisation of the topos of trees from the codomain fibration over sets to arbitrary fibrations. As a result, we obtain a framework that allows the addition of a recursion principle for coinduction to rather arbitrary logics and programming languages. The main interest of using recursion is that it allows one to write proofs and programs in a goal-oriented fashion. This enables easily understandable coinductive proofs and programs, and fosters automatic proof search. Part of the framework are also various results that enable a wide range of applications: transportation of (co)limits, exponentials, fibred adjunctions and first-order connectives from the initial fibration to the one constructed through the framework. This means that the framework extends any first-order logic with the later modality. Moreover, we obtain soundness and completeness results, and can use up-to techniques as proof rules. Since the construction works for a wide variety of fibrations, we will be able to use the recursion offered by the later modality in various context. For instance, we will show how recursive proofs can be obtained for arbitrary (syntactic) first-order logics, for coinductive set-predicates, and for the probabilistic modal mu-calculus. Finally, we use the same construction to obtain a novel language for probabilistic productive coinductive programming. These examples demonstrate the flexibility of the framework and its accompanying results.

Subject Classification

ACM Subject Classification
  • Theory of computation → Logic
Keywords
  • Coinduction
  • Fibrations
  • Later Modality
  • Recursive Proofs
  • Up-to techniques
  • Probabilistic Logic
  • Probabilistic Programming

Metrics

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

Related Versions

References

  1. Andreas Abel, Brigitte Pientka, David Thibodeau, and Anton Setzer. Copatterns: Programming Infinite Structures by Observations. In POPL'13, pages 27-38. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429075.
  2. Jiří Adámek, Stefan Milius, and Lawrence S. Moss. Introduction to Category Theroy, Algebras and Coalgebra. A monograph in preparation, 2010. URL: http://www.tu-braunschweig.de/Medien-DB/iti/survey_full.pdf.
  3. Jiŕı Adámek and Vera Trnková. Initial Algebras and Terminal Coalgebras in Many-Sorted Sets. MSCS, 21(2):481-509, 2011. URL: https://doi.org/10.1017/S0960129510000502.
  4. Bahareh Afshari and Graham E. Leigh. Cut-Free Completeness for Modal Mu-Calculus. In Proc. of LICS'17, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005088.
  5. Andrew W. Appel, Paul-André Melliès, Christopher D. Richards, and Jérôme Vouillon. A Very Modal Model of a Modern, Major, General Type System. In POPL, pages 109-122. ACM, 2007. URL: https://doi.org/10.1145/1190216.1190235.
  6. Robert Atkey and Conor McBride. Productive Coprogramming with Guarded Recursion. In ICFP, pages 197-208. ACM, 2013. URL: https://doi.org/10.1145/2500365.2500597.
  7. Michael Barr. Terminal Coalgebras in Well-Founded Set Theory. TCS, 114(2):299-315, 1993. URL: https://doi.org/10.1016/0304-3975(93)90076-6.
  8. Henning Basold. Code Repository, 2018. URL: https://perso.ens-lyon.fr/henning.basold/code/.
  9. Henning Basold. Mixed Inductive-Coinductive Reasoning: Types, Programs and Logic. PhD Thesis, Radboud University, 2018. URL: https://hdl.handle.net/2066/190323.
  10. Henning Basold, Ekaterina Komendantskaya, and Yue Li. Coinduction in Uniform: Foundations for Corecursive Proof Search with Horn Clauses. In ESOP'19, volume 11423 of LNCS. Springer, 2019. URL: http://arxiv.org/abs/1811.07644.
  11. Henning Basold, Damien Pous, and Jurriaan Rot. Monoidal Company for Accessible Functors. In CALCO 2017, volume 72 of LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017. URL: https://doi.org/10.4230/LIPIcs.CALCO.2017.5.
  12. Lev D. Beklemishev. Parameter Free Induction and Provably Total Computable Functions. TCS, 224(1-2):13-33, 1999. URL: https://doi.org/10.1016/S0304-3975(98)00305-3.
  13. Jean Bénabou. Fibered Categories and the Foundations of Naive Category Theory. Journal of Symbolic Logic, 50(1):10-37, 1985. URL: https://doi.org/10.2307/2273784.
  14. Lars Birkedal, Alěs Bizjak, Ranald Clouston, Hans Bugge Grathwohl, Bas Spitters, and Andrea Vezzosi. Guarded Cubical Type Theory: Path Equality for Guarded Recursion. In CSL 2016, volume 62 of LIPIcs, pages 23:1-23:17. Schloss Dagstuhl, 2016. URL: https://doi.org/10.4230/LIPIcs.CSL.2016.23.
  15. Lars Birkedal and Rasmus Ejlers Møgelberg. Intensional Type Theory with Guarded Recursive Types qua Fixed Points on Universes. In LICS, pages 213-222. IEEE Computer Society, 2013. URL: https://doi.org/10.1109/LICS.2013.27.
  16. Lars Birkedal, Rasmus Ejlers Møgelberg, Jan Schwinghammer, and Kristian Støvring. First Steps in Synthetic Guarded Domain Theory: Step-Indexing in the Topos of Trees. LMCS, 8(4), 2012. URL: https://doi.org/10.2168/LMCS-8(4:1)2012.
  17. Ales Bizjak, Hans Bugge Grathwohl, Ranald Clouston, Rasmus Ejlers Møgelberg, and Lars Birkedal. Guarded Dependent Type Theory with Coinductive Types. In FoSSaCS, volume 9634 of LNCS, pages 20-35. Springer, 2016. URL: http://arxiv.org/abs/1601.01586.
  18. Jasmin Christian Blanchette, Johannes Hölzl, Andreas Lochbihler, Lorenz Panny, Andrei Popescu, and Dmitriy Traytel. Truly Modular (Co)Datatypes for Isabelle/HOL. In Gerwin Klein and Ruben Gamboa, editors, Proceedings of ITP 2014, volume 8558 of LNCS, pages 93-110. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_7.
  19. Filippo Bonchi, Daniela Petrişan, Damien Pous, and Jurriaan Rot. Coinduction Up-to in a Fibrational Setting. In LICS '14, pages 20:1-20:9. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603149.
  20. Julian C. Bradfield and Colin Stirling. Modal Mu-Calculi. In Handbook of Modal Logic, pages 721-756. Elsevier, 2006. Google Scholar
  21. James Brotherston. Cyclic Proofs for First-Order Logic with Inductive Definitions. In Bernhard Beckert, editor, Proceedings of TABLEAUX 2005, volume 3702 of Lecture Notes in Computer Science, pages 78-92. Springer, 2005. URL: https://doi.org/10.1007/11554554_8.
  22. James Brotherston and Alex Simpson. Complete Sequent Calculi for Induction and Infinite Descent. In Proceedings of LICS 2007, pages 51-62. IEEE Computer Society, 2007. URL: https://doi.org/10.1109/LICS.2007.16.
  23. Ranald Clouston and Rajeev Goré. Sequent Calculus in the Topos of Trees. In Andrew M. Pitts, editor, Proc. of FoSSaCS 2015, volume 9034 of LNCS, pages 133-147. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-46678-0_9.
  24. J. Robin B. Cockett. Deforestation, Program Transformation, and Cut-Elimination. Electr. Notes Theor. Comput. Sci., 44(1):88-127, 2001. URL: https://doi.org/10.1016/S1571-0661(04)80904-6.
  25. The Coq Development Team. The Coq Proof Assistant Reference Manual. Technical report, LogiCal Project, 2012. Version 8.4. URL: http://coq.inria.fr.
  26. Christian Dax, Martin Hofmann, and Martin Lange. A Proof System for the Linear Time μ-Calculus. In S. Arun-Kumar and Naveen Garg, editors, Proceedings of FSTTCS 2006, volume 4337 of LNCS, pages 273-284. Springer, 2006. URL: https://doi.org/10.1007/11944836_26.
  27. Amina Doumane. On the Infinitary Proof Theory of Logics with Fixed Points. PhD Thesis, Université Paris Diderot, 2017. Google Scholar
  28. Jérôme Fortier and Luigi Santocanale. Cuts for Circular Proofs: Semantics and Cut-Elimination. In CSL, pages 248-262, 2013. URL: https://doi.org/10.4230/LIPIcs.CSL.2013.248.
  29. Clément Fumex, Neil Ghani, and Patricia Johann. Indexed Induction and Coinduction, Fibrationally. In Proc. of CALCO '11, volume 6859 of Lecture Notes in Computer Science, pages 176-191. Springer, 2011. URL: https://doi.org/10.1007/978-3-642-22944-2_13.
  30. Sergey Goncharov and Lutz Schröder. Guarded Traced Categories. In Christel Baier and Ugo Dal Lago, editors, Proc. of FOSSACS'18, volume 10803 of LNCS, pages 313-330. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89366-2_17.
  31. Programming Logic group on Agda. Agda Documentation. Technical report, Chalmers and Gothenburg University, 2015. Version 2.4.2.5. URL: http://wiki.portal.chalmers.se/agda/.
  32. Tatsuya Hagino. A Typed Lambda Calculus with Categorical Type Constructors. In Category Theory in Computer Science, Lecture Notes in Computer Science, pages 140-157. Springer, 1987. URL: https://doi.org/10.1007/3-540-18508-9_24.
  33. Helle Hvid Hansen, Clemens Kupke, and Jan Rutten. Stream Differential Equations: Specification Formats and Solution Methods. LMCS, 13(1), 2017. URL: https://doi.org/10.23638/LMCS-13(1:3)2017.
  34. Masahito Hasegawa. On Traced Monoidal Closed Categories. Mathematical Structures in Computer Science, 19(2):217-244, 2009. URL: https://doi.org/10.1017/S0960129508007184.
  35. Ichiro Hasuo, Kenta Cho, Toshiki Kataoka, and Bart Jacobs. Coinductive Predicates and Final Sequences in a Fibration. Electronic Notes in Theoretical Computer Science, 298:197-214, November 2013. URL: https://doi.org/10.1016/j.entcs.2013.09.014.
  36. Claudio Hermida and Bart Jacobs. Structural Induction and Coinduction in a Fibrational Setting. Information and Computation, 145:107-152, 1997. URL: https://doi.org/10.1006/inco.1998.2725.
  37. Chris Heunen, Ohad Kammar, Sam Staton, and Hongseok Yang. A Convenient Category for Higher-Order Probability Theory. In Proc. of LICS'17, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005137.
  38. Chung-Kil Hur, Georg Neis, Derek Dreyer, and Viktor Vafeiadis. The Power of Parameterization in Coinductive Proof. In Proc. of POPL'13, POPL '13, pages 193-206. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429093.
  39. Michael Huth and Marta Z. Kwiatkowska. Quantitative Analysis and Model Checking. In Proc. of LICS'97, pages 111-122. IEEE Computer Society, 1997. URL: https://doi.org/10.1109/LICS.1997.614940.
  40. J Martin E Hyland. The Effective Topos. In Studies in Logic and the Foundations of Mathematics, volume 110, pages 165-216. Elsevier, 1982. Google Scholar
  41. Bart Jacobs. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam, 1999. Google Scholar
  42. Bart Jacobs. Introduction to Coalgebra: Towards Mathematics of States and Observation. Number 59 in Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, 2016. URL: https://doi.org/10.1017/CBO9781316823187.
  43. Bart Jacobs and Jan Rutten. A Tutorial on (Co)Algebras and (Co)Induction. EATCS Bulletin, 62:62-222, 1997. Google Scholar
  44. Henning Kerstan, Barbara König, and Bram Westerbaan. Lifting Adjunctions to Coalgebras to (Re)Discover Automata Constructions. In Marcello M. Bonsangue, editor, Revised Selected Papers of CMCS'14, volume 8446 of LNCS, pages 168-188. Springer, 2014. URL: https://doi.org/10.1007/978-3-662-44124-4_10.
  45. Anders Kock. Strong Functors and Monoidal Monads. Archiv der Mathematik, 23(1):113-120, 1972. Google Scholar
  46. Dexter Kozen. Results on the Propositional μ-Calculus. Theor. Comput. Sci., 27:333-354, 1983. URL: https://doi.org/10.1016/0304-3975(82)90125-6.
  47. F William Lawvere. Diagonal Arguments and Cartesian Closed Categories. In Category Theory, Homology Theory and Their Applications II, pages 134-145. Springer, 1969. Google Scholar
  48. Nex Paul Mendler. Inductive Types and Type Constraints in the Second-Order Lambda Calculus. Ann. Pure Appl. Logic, 51(1-2):159-172, 1991. URL: https://doi.org/10.1016/0168-0072(91)90069-X.
  49. Matteo Mio and Alex Simpson. Łukasiewicz (μ)-calculus. Fundam. Inform., 150(3-4):317-346, 2017. URL: https://doi.org/10.3233/FI-2017-1472.
  50. Rasmus Ejlers Møgelberg. A Type Theory for Productive Coprogramming via Guarded Recursion. In CSL-LICS, pages 71:1-71:10. ACM, 2014. URL: https://doi.org/10.1145/2603088.2603132.
  51. Lawrence S. Moss. Parametric Corecursion. Theoretical Computer Science, 260:139-163, 2001. Google Scholar
  52. Hiroshi Nakano. A Modality for Recursion. In LICS, pages 255-266. IEEE Computer Society, 2000. URL: https://doi.org/10.1109/LICS.2000.855774.
  53. Damian Niwinski and Igor Walukiewicz. Games for the μ-Calculus. TCS, 163(1&2):99-116, 1996. URL: https://doi.org/10.1016/0304-3975(95)00136-0.
  54. Damien Pous. Complete Lattices and Up-To Techniques. In Zhong Shao, editor, APLAS'07, volume 4807 of LNCS, pages 351-366. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-76637-7_24.
  55. Damien Pous. Coinduction All the Way Up. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Proceedings of LICS '16, pages 307-316. ACM, 2016. URL: https://doi.org/10.1145/2933575.2934564.
  56. Damien Pous and Jurriaan Rot. Companions, Codensity, and Causality. In Proceedings of FOSSACS 2017, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_7.
  57. Grigore Roşu and Dorel Lucanu. Circular Coinduction: A Proof Theoretical Foundation. In CALCO, volume 5728 of LNCS, pages 127-144. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03741-2_10.
  58. Jurriaan Rot. Enhanced Coinduction. PhD, University Leiden, Leiden, 2015. Google Scholar
  59. Jurriaan Rot, Filippo Bonchi, Marcello Bonsangue, Damien Pous, Jan Rutten, and Alexandra Silva. Enhanced Coalgebraic Bisimulation. MSCS, 27(7):1236-1264, 2017. URL: https://doi.org/10.1017/S0960129515000523.
  60. Jan Rutten. Universal Coalgebra: A Theory of Systems. TCS, 249(1):3-80, 2000. URL: https://doi.org/10.1016/S0304-3975(00)00056-6.
  61. Jan Rutten. Behavioural Differential Equations: A Coinductive Calculus of Streams, Automata, and Power Series. TCS, 308(1-3):1-53, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00895-2.
  62. Jan Rutten. The Method of Coalgebra: Exercises in Coinduction. CWI, Amsterdam, February 2019. URL: http://persistent-identifier.org/?identifier=urn:nbn:nl:ui:18-28550.
  63. Davide Sangiorgi. On the Bisimulation Proof Method. Mathematical Structures in Computer Science, 8(5):447-479, 1998. Google Scholar
  64. Luigi Santocanale. A Calculus of Circular Proofs and Its Categorical Semantics. In FoSSaCS, pages 357-371, 2002. URL: https://doi.org/10.1007/3-540-45931-6_25.
  65. Luigi Santocanale. μ-Bicomplete Categories and Parity Games. RAIRO - ITA, 36(2):195-227, 2002. URL: https://doi.org/10.1051/ita:2002010.
  66. Luke Simon, Ajay Bansal, Ajay Mallya, and Gopal Gupta. Co-Logic Programming: Extending Logic Programming with Coinduction. In Lars Arge, Christian Cachin, Tomasz Jurdzinski, and Andrzej Tarlecki, editors, Proc. of ICALP'07, volume 4596 of LNCS, pages 472-483. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-73420-8_42.
  67. Alex Simpson. Cyclic Arithmetic Is Equivalent to Peano Arithmetic. In Proceedings of FoSSaCS'17, LNCS, 2017. URL: https://doi.org/10.1007/978-3-662-54458-7_17.
  68. Craig Smoryński. Self-Reference and Modal Logic. Universitext. Springer-Verlag, 1985. Google Scholar
  69. Ana Sokolova. Probabilistic Systems Coalgebraically: A Survey. TCS, 412(38):5095-5110, 2011. URL: https://doi.org/10.1016/j.tcs.2011.05.008.
  70. Robert M. Solovay. Provability Interpretations of Modal Logic. Israel Journal of Mathematics, 25(3):287-304, 1976. URL: https://doi.org/10.1007/BF02757006.
  71. Thomas Streicher. Fibred Categories à La Jean Bénabou. arXiv:math.CT/1801.02927, 2018. URL: http://arxiv.org/abs/1801.02927.
  72. Kasper Svendsen, Filip Sieczkowski, and Lars Birkedal. Transfinite Step-Indexing: Decoupling Concrete and Logical Steps. In Peter Thiemann, editor, Proc. of ESOP'16, volume 9632 of LNCS, pages 727-751. Springer, 2016. URL: https://doi.org/10.1007/978-3-662-49498-1_28.
  73. D. A. Turner. Elementary Strong Functional Programming. In Pieter H. Hartel and Marinus J. Plasmeijer, editors, Proceedings of FPLE'95, volume 1022 of LNCS, pages 1-13. Springer, 1995. URL: https://doi.org/10.1007/3-540-60675-0_35.
  74. Matthijs Vákár, Ohad Kammar, and Sam Staton. A Domain Theory for Statistical Probabilistic Programming. PACMPL, 3(POPL):36:1-36:29, 2019. URL: http://arxiv.org/abs/1811.04196.
  75. Igor Walukiewicz. On Completeness of the Mu-Calculus. In Proceedings of LICS '93, pages 136-146. IEEE Computer Society, 1993. URL: https://doi.org/10.1109/LICS.1993.287593.
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