Document Open Access Logo

Strong Induction Is an Up-To Technique

Authors Filippo Bonchi , Elena Di Lavore , Anna Ricci

PDF
Thumbnail PDF

File

LIPIcs.CSL.2025.28.pdf
  • Filesize: 0.76 MB
  • 21 pages

Document Identifiers

Author Details

Filippo Bonchi
  • Universitá di Pisa, Italy
Elena Di Lavore
  • Universitá di Pisa, Italy
Anna Ricci
  • Universitá di Pisa, Italy

Funding

This study was carried out within the National Centre on HPC, Big Data and Quantum Computing - SPOKE 10 (Quantum Computing) and received funding from the European Union Next-GenerationEU - National Recovery and Resilience Plan (NRRP) – MISSION 4 COMPONENT 2, INVESTMENT N. 1.4 – CUP N. I53C22000690001. This research was partly funded by the Advanced Research + Invention Agency (ARIA) Safeguarded AI Programme.
  • Bonchi, Filippo: Supported by the Ministero dell'Università e della Ricerca of Italy grant PRIN 2022 PNRR No. P2022HXNSC - RAP (Resource Awareness in Programming).

Acknowledgements

The authors would like to thank Jurriaan Rot for the inspiring discussions.

Cite As Get BibTex

Filippo Bonchi, Elena Di Lavore, and Anna Ricci. Strong Induction Is an Up-To Technique. In 33rd EACSL Annual Conference on Computer Science Logic (CSL 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 326, pp. 28:1-28:21, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025) https://doi.org/10.4230/LIPIcs.CSL.2025.28

Abstract

Up-to techniques are enhancements of the coinduction proof principle which, in lattice theoretic terms, is the dual of induction. What is the dual of coinduction up-to? By means of duality, we illustrate a theory of induction up-to and we observe that an elementary proof technique, commonly known as strong induction, is an instance of induction up-to. We also show that, when generalising our theory from lattices to categories, one obtains an enhancement of the induction definition principle known in the literature as comonadic recursion.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
  • Theory of computation → Logic and verification
Keywords
  • Induction
  • Coinduction
  • Up-to Techniques
  • Induction up-to
  • Lattices
  • Algebras

Metrics

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

References

  1. Roberto M Amadio and Luca Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems (TOPLAS), 15(4):575-631, 1993. URL: https://doi.org/10.1145/155183.155231.
  2. Falk Bartels. Generalised coinduction. Mathematical Structures in Computer Science, 13(2):321-348, 2003. URL: https://doi.org/10.1017/S0960129502003900.
  3. Filippo Bonchi, Pierre Ganty, Roberto Giacobazzi, and Dusko Pavlovic. Sound up-to techniques and complete abstract domains. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, pages 175-184, 2018. URL: https://doi.org/10.1145/3209108.3209169.
  4. Filippo Bonchi, Barbara König, and Daniela Petrisan. Up-to techniques for behavioural metrics via fibrations. Math. Struct. Comput. Sci., 33(4-5):182-221, 2023. URL: https://doi.org/10.1017/s0960129523000166.
  5. Filippo Bonchi, Daniela Petrisan, Damien Pous, and Jurriaan Rot. A general account of coinduction up-to. Acta Informatica, 54(2):127-190, 2017. URL: https://doi.org/10.1007/S00236-016-0271-4.
  6. Filippo Bonchi and Damien Pous. Checking NFA equivalence with bisimulations up to congruence. In Roberto Giacobazzi and Radhia Cousot, editors, The 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, Rome, Italy - January 23 - 25, 2013, pages 457-468. ACM, 2013. URL: https://doi.org/10.1145/2429069.2429124.
  7. Daniela Cancila, Furio Honsell, and Marina Lenisa. Generalized coiteration schemata. Electronic Notes in Theoretical Computer Science, 82(1):76-93, 2003. URL: https://doi.org/10.1016/S1571-0661(04)80633-9.
  8. Venanzio Capretta, Tarmo Uustalu, and Varmo Vene. Recursive coalgebras from comonads. Information and Computation, 204(4):437-468, 2006. URL: https://doi.org/10.1016/j.ic.2005.08.005.
  9. Didier Caucal. Graphes canoniques de graphes algébriques. RAIRO Theor. Informatics Appl., 24:339-352, 1990. URL: https://doi.org/10.1051/ita/1990240403391.
  10. Konstantinos Chatzikokolakis, Catuscia Palamidessi, and Valeria Vignudelli. Up-to techniques for generalized bisimulation metrics. In Josée Desharnais and Radha Jagadeesan, editors, 27th International Conference on Concurrency Theory, CONCUR 2016, August 23-26, 2016, Québec City, Canada, volume 59 of LIPIcs, pages 35:1-35:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.CONCUR.2016.35.
  11. Thierry Coquand. Infinite objects in type theory. In International Workshop on Types for Proofs and Programs, pages 62-78. Springer, 1993. URL: https://doi.org/10.1007/3-540-58085-9_72.
  12. Erik P. de Vink and Jan J.M.M. Rutten. Bisimulation for probabilistic transition systems: a coalgebraic approach. Theoretical Computer Science, 221(1):271-293, 1999. URL: https://doi.org/10.1016/S0304-3975(99)00035-3.
  13. Adrien Durier, Daniel Hirschkoff, and Davide Sangiorgi. Divergence and unique solution of equations. Logical Methods in Computer Science, 15, 2019. URL: https://doi.org/10.23638/LMCS-15(3:12)2019.
  14. Marco Forti and Furio Honsell. Set theory with free construction principles. Annali della Scuola Normale Superiore di Pisa-Classe di Scienze, 10(3):493-522, 1983. Google Scholar
  15. Herman Geuvers and Bart Jacobs. Relating apartness and bisimulation. Logical Methods in Computer Science, 17, 2021. URL: https://doi.org/10.46298/lmcs-17(3:15)2021.
  16. Ichiro Hasuo, Bart Jacobs, and Ana Sokolova. Generic trace semantics via coinduction. Logical Methods in Computer Science, 3, 2007. URL: https://doi.org/10.2168/LMCS-3(4:11)2007.
  17. Ichiro Hasuo, Shunsuke Shimizu, and Corina Cîrstea. Lattice-theoretic progress measures and coalgebraic model checking. In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 718-732, 2016. URL: https://doi.org/10.1145/2837614.2837673.
  18. Claudio Hermida and Bart Jacobs. Structural induction and coinduction in a fibrational setting. Information and computation, 145(2):107-152, 1998. URL: https://doi.org/10.1006/inco.1998.2725.
  19. Arend Heyting. Zur intuitionistischen axiomatik der projektiven geometrie. Mathematische Annalen, 98(1):491-538, 1928. Google Scholar
  20. Bart Jacobs, Alexandra Silva, and Ana Sokolova. Trace semantics via determinization. In International Workshop on Coalgebraic Methods in Computer Science, pages 109-129. Springer, 2012. URL: https://doi.org/10.1007/978-3-642-32784-1_7.
  21. Bartek Klin. Bialgebras for structural operational semantics: An introduction. Theor. Comput. Sci., 412(38):5043-5069, 2011. URL: https://doi.org/10.1016/j.tcs.2011.03.023.
  22. Dexter Kozen and Alexandra Silva. Practical coinduction. Mathematical Structures in Computer Science, 27(7):1132-1152, 2017. URL: https://doi.org/10.1017/S0960129515000493.
  23. Robin Milner. Communication and concurrency, volume 84 of PHI Series in computer science. Prentice Hall, 1989. Google Scholar
  24. Robin Milner and Mads Tofte. Co-induction in relational semantics. Theoretical computer science, 87(1):209-220, 1991. URL: https://doi.org/10.1016/0304-3975(91)90033-X.
  25. Keiko Nakata and Tarmo Uustalu. Resumptions, weak bisimilarity and big-step semantics for while with interactive I/O: An exercise in mixed induction-coinduction. In In Proceedings of SOS 2010, pages 57-75, 2010. URL: https://doi.org/10.4204/EPTCS.32.5.
  26. David Park. Fixpoint induction and proofs of program properties. Machine intelligence, 5, 1969. Google Scholar
  27. David Park. Concurrency and automata on infinite sequences. In Theoretical Computer Science: 5th GI-Conference Karlsruhe, March 23-25, 1981, pages 167-183. Springer, 2005. Google Scholar
  28. Damien Pous. Complete lattices and up-to techniques. In Zhong Shao, editor, Programming Languages and Systems, 5th Asian Symposium, APLAS 2007, Singapore, November 29-December 1, 2007, Proceedings, volume 4807 of Lecture Notes in Computer Science, pages 351-366. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-76637-7_24.
  29. Damien Pous. Coinduction all the way up. In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, pages 307-316, 2016. URL: https://doi.org/10.1145/2933575.2934564.
  30. Damien Pous and Davide Sangiorgi. Enhancements of the bisimulation proof method. In Davide Sangiorgi and Jan J. M. M. Rutten, editors, Advanced Topics in Bisimulation and Coinduction, volume 52 of Cambridge tracts in theoretical computer science, pages 233-289. Cambridge University Press, UK, 2012. Google Scholar
  31. Jan J.M.M. Rutten. Behavioural differential equations: a coinductive calculus of streams, automata, and power series. Theoretical Computer Science, 308(1):1-53, 2003. URL: https://doi.org/10.1016/S0304-3975(02)00895-2.
  32. Davide Sangiorgi. On the bisimulation proof method. Mathematical Structures in Computer Science , Volume 8 , Issue 5, 1998. URL: https://doi.org/10.1017/S0960129598002527.
  33. Davide Sangiorgi. On the origins of bisimulation and coinduction. ACM Transactions on Programming Languages and Systems (TOPLAS), 31(4):1-41, 2009. URL: https://doi.org/10.1145/1516507.1516510.
  34. Davide Sangiorgi. Equations, contractions, and unique solutions. ACM Transactions on Computational Logic (TOCL), 18(1):1-30, 2017. URL: https://doi.org/10.1145/2971339.
  35. Davide Sangiorgi. From enhanced coinduction towards enhanced induction. Proceedings of the ACM on Programming Languages, 6(POPL):1-29, 2022. URL: https://doi.org/10.1145/3498679.
  36. Alexandra Silva, Filippo Bonchi, Marcello M. Bonsangue, and Jan J. M. M. Rutten. Generalizing the powerset construction, coalgebraically. In Kamal Lodaya and Meena Mahajan, editors, IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2010, December 15-18, 2010, Chennai, India, volume 8 of LIPIcs, pages 272-283. Schloss-Dagstuhl-Leibniz Zentrum für Informatik, Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2010. URL: https://doi.org/10.4230/LIPIcs.FSTTCS.2010.272.
  37. Daniele Turi and Gordon Plotkin. Towards a mathematical operational semantics. In Proceedings of Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 280-291. IEEE, 1997. URL: https://doi.org/10.1109/LICS.1997.614955.
  38. Tarmo Uustalu and Varmo Vene. Primitive (co) recursion and course-of-value (co) iteration, categorically. Informatica, 10(1):5-26, 1999. URL: https://doi.org/10.3233/INF-1999-10102.
  39. Tarmo Uustalu, Varmo Vene, and Alberto Pardo. Recursion schemes from comonads. Nordic Journal of Computing, 8(3):366-390, 2001. URL: http://www.cs.helsinki.fi/njc/References/uustaluvp2001:366.html.
  40. Johan Van Benthem. Modal logic and classical logic. 1983. Google Scholar
  41. Rob J van Glabbeek. The linear time - branching time spectrum II: The semantics of sequential systems with silent moves extended abstract. In International Conference on Concurrency Theory, pages 66-81. Springer, 1993. Google Scholar
  42. Rob J Van Glabbeek. The linear time - branching time spectrum I. In Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, editors, Handbook of Process Algebra, pages 3-99. North-Holland / Elsevier, 2001. URL: https://doi.org/10.1016/b978-044482830-9/50019-9.
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 About DROPS Imprint Privacy Contact