Hostname: page-component-cd9895bd7-8ctnn Total loading time: 0 Render date: 2024-12-17T19:27:17.607Z Has data issue: false hasContentIssue false
  • English
  • Français

Practical coinduction

Published online by Cambridge University Press:  09 February 2016

DEXTER KOZEN  and
ALEXANDRA SILVA
DEXTER KOZEN
Affiliation:
Computer Science, Cornell University, Ithaca, New York 14853-7501, U.S.A. Email: [email protected]
ALEXANDRA SILVA
Affiliation:
Intelligent Systems, Radboud University Nijmegen, Postbus 9010, 6500 GL Nijmegen, the Netherlands Email: [email protected]
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively defined datatypes such as finite lists, finite trees and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood. In this paper, we illustrate through several examples the use of coinduction in informal mathematical arguments. Our aim is to promote the principle as a useful tool for the working mathematician and to bring it to a level of familiarity on par with induction. We show that coinduction is not only about bisimilarity and equality of behaviors, but also applicable to a variety of functions and relations defined on coinductive datatypes.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 27 , Special Issue 7: Special Issue: Coalgebraic Logic , October 2017 , pp. 1132 - 1152
Copyright
Copyright © Cambridge University Press 2016 

References

Aczel, P. (1988). Non-Well-Founded Sets, Number 14 in CSLI Lecture Notes, Center for the Study of Language and Information, Stanford, CA.Google Scholar
Amadio, R. M. and Cardelli, L. (1993). Subtyping recursive types. ACM Transactions on Programming Languages and Systems (TOPLAS) 15 (4), 575–631.CrossRefGoogle Scholar
Barwise, J. and Moss, L. (1996). Vicious Circles: On the Mathematics of Non-Wellfounded Phenomena, Number 60 in CSLI Lecture Notes, Center for the Study of Language and Information, Stanford, CA.Google Scholar
Brandt, M. and Henglein, F. (1998). Coinductive axiomatization of recursive type equality and subtyping. Fundamenta Informaticae 33 (4) 309–338.Google Scholar
Harel, D., Kozen, D. and Tiuryn, J. (2000). Dynamic Logic. MIT Press, Cambridge, MA.CrossRefGoogle Scholar
Hermida, C. and Jacobs, B. (1998). Structural induction and coinduction in a fibrational setting. Information and Computation 145 (2) 107–152.Google Scholar
Ichiro, H., Jacobs, B. and Sokolova, A. (2007). Generic trace semantics via coinduction. Logical Methods in Computer Science 3 (4:11) 1–36.Google Scholar
Jaffar, J., Santosa, A. and Voicu, R. (September 2008). A coinduction rule for entailment of recursively-defined properties. In: Stuckey, P.J. (ed.) Proceedings of the 14th International Conference on Principles and Practice of Constraint Programming. Lecture Notes in Computer Science 5202, Springer, Berlin, 493–508.Google Scholar
Jeannin, J.-B. and Kozen, D. (2012). Computing with capsules. J. Automata, Languages and Combinatorics 17 (2–4) 185–204.Google Scholar
Klin, B. (2007). Bialgebraic operational semantics and modal logic. In: LICS, IEEE Computer Society 336–345.Google Scholar
Kozen, D. (May 1997). Kleene algebra with tests. Transactions on Programming Languages and Systems 19 (3) 427–443.CrossRefGoogle Scholar
Kozen, D., Palsberg, J. and Schwartzbach, M.I. (1995). Efficient recursive subtyping. Mathematical Structures in Computer Science 5 (1) 113–125.Google Scholar
Kozen, D. and Ruozzi, N. (2009). Applications of metric coinduction. Logical Methods in Computer Science 5 (3:10) 1–19.Google Scholar
Kurz, A. (2001). Specifying coalgebras with modal logic. Theoretical Computer Science 260 (1–2) 119–138.Google Scholar
Lambek, J. (1968). A fixpoint theorem for complete categories. Mathematische Zeitschrift 103 151–161.Google Scholar
Mendler, N.P. (1988). Inductive Definition in Type Theory. PhD thesis, Cornell University.Google Scholar
Milner, R. and Tofte, M. (1991). Co-induction in relational semantics. Theoretical Computer Science 87 (1) 209–220.CrossRefGoogle Scholar
Niqui, M. and Rutten, J. (2009). Coinductive predicates as final coalgebras. In: Proceedings of the 6th Workshop on Fixed Points in Computer Science (FICS 2009) 79–85.Google Scholar
Paulson, L.C. (1997). Mechanizing coinduction and corecursion in higher-order logic. Journal of Logic and Computation 7 (2) 175–204.Google Scholar
Pous, D. and Sangiorgi, D. (2011). Enhancements of the coinductive proof method. In: Advanced Topics in Bisimulation and Coinduction, Cambridge University Press.Google Scholar
Roşu, G. and Lucanu, D. (September 2009). Circular coinduction: A proof theoretical foundation. In: Proceedings of the 3rd Conference on Algebra and Coalgebra in Computer Science (CALCO'09). Lecture Notes in Computer Science 5728, Springer, Berlin, 127–144.Google Scholar
Rutten, J.J.M.M. (2000). Universal coalgebra: A theory of systems. Theoretical Computer Science 249 (1) 3–80.CrossRefGoogle Scholar
Schröder, L. (2005). Expressivity of coalgebraic modal logic: The limits and beyond. In: Sassone, V. (ed.) FoSSaCS. Springer Lecture Notes in Computer Science 3441 440–454.Google Scholar
Schröder, L. (2008). Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science 390 (2–3) 230–247.Google Scholar
Schröder, L. and Pattinson, D. (2007). Rank-1 modal logics are coalgebraic. In: Thomas, W. and Weil, P. (eds.) STACS. Springer Lecture Notes in Computer Science 4393 573–585.Google Scholar
Turi, D. and Plotkin, G.D. (1997). Towards a mathematical operational semantics. In: LICS 280–291.Google Scholar