# How to Reason Coinductively Informally

Chapter
Part of the Progress in Computer Science and Applied Logic book series (PCS, volume 28)

## Abstract

We start by giving an overview of the theory of indexed inductively and coinductively defined sets. We consider the theory of strictly positive indexed inductive definitions in a set theoretic setting. We show the equivalence between the definition as an indexed initial algebra, the definition via an induction principle, and the set theoretic definition of indexed inductive definitions. We review as well the equivalence of unique iteration, unique primitive recursion, and induction. Then we review the theory of indexed coinductively defined sets or final coalgebras. We construct indexed coinductively defined sets set theoretically, and show the equivalence between the category theoretic definition, the principle of unique coiteration, of unique corecursion, and of iteration together with bisimulation as equality. Bisimulation will be defined as an indexed coinductively defined set. Therefore proofs of bisimulation can be carried out corecursively. This fact can be considered together with bisimulation implying equality as the coinduction principle for the underlying coinductively defined set. Finally we introduce various schemata for reasoning about coinductively defined sets in an informal way: the schemata of corecursion, of indexed corecursion, of coinduction, and of corecursion for coinductively defined relations. This allows to reason about coinductively defined sets similarly as one does when reasoning about inductively defined sets using schemata of induction. We obtain the notion of a coinduction hypothesis, which is the dual of an induction hypothesis.

## References

1. 1.
A. Abel, B. Pientka, Wellfounded recursion with copatterns: a unified approach to termination and productivity, in ACM SIGPLAN International Conference on Functional Programming, ICFP’13, Boston, MA, USA, 25–27 Sept 2013, ed. by G. Morrisett, T. Uustalu (ACM, 2013), pp. 185–196Google Scholar
2. 2.
A. Abel, B. Pientka, D. Thibodeau, A. Setzer, Copatterns: programming infinite structures by observations, in Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL’13, ed. by R. Giacobazzi, R. Cousot (ACM, New York, NY, USA, 2013), pp. 27–38Google Scholar
3. 3.
P. Aczel, Non-wellfounded Set Theory, vol. 14, CSLI Lecture Notes (Stanford University, Center for the Study of Language and Information, Stanford, CA, 1988)Google Scholar
4. 4.
P. Aczel, Algebras and coalgebras, Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, vol. 2297, Lecture Notes in Computer Science, ed. by R. Backhouse, R. Crole, J. Gibbons (Springer, 2002), pp. 79–88Google Scholar
5. 5.
P. Aczel, N. Mendler, A final coalgebra theorem, in Category Theory and Computer Science, vol. 389, Lecture Notes in Computer Science, ed. by D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts, A. Poigné (Springer, Berlin/Heidelberg, 1989), pp. 357–365. doi:
6. 6.
T. Altenkirch, P. Morris, Indexed containers, in 24th Annual IEEE Symposium on Logic in Computer Science, 2009. LICS’09, pp. 277–285 (2009)Google Scholar
7. 7.
M. Barr, Terminal coalgebras in well-founded set theory. Theor. Comput. Sci. 114(2), 299–315 (1993)
8. 8.
P.J. de Bruin, Inductive types in constructive languages. Ph.D. thesis, Faculty of Mathematics and Natural Sciences, University of Groningen, Groningen, The Netherlands, Mar 1995. https://www.rug.nl/research/portal/publications/pub%2887db58af-1fd6-4030-a862-98b5651d6be8%29.html and http://www.peterdebruin.net/
9. 9.
P. Dybjer, Inductive sets and families in Martin-Löf’s type theory and their set-theoretic semantics, in Logical Frameworks, ed. by G. Huet, G. Plotkin (Cambridge University Press, 1991), pp. 280–306Google Scholar
10. 10.
P. Dybjer, A. Setzer, A finite axiomatization of inductive-recursive definitions, in Typed Lambda Calculi and Applications, vol. 1581, Lecture Notes in Computer Science, ed. by J.-Y. Girard (Springer, Apr 1999), pp. 129–146Google Scholar
11. 11.
P. Dybjer, A. Setzer, Indexed induction-recursion, in Proof Theory in Computer Science, vol. 2183, Lecture Notes in Computer Science, ed. by R. Kahle, P. Schroeder-Heister, R. Stärk (Springer, 2001), pp. 93–113Google Scholar
12. 12.
P. Dybjer, A. Setzer, Induction-recursion and initial algebras. Ann. Pure Appl. Logic 124, 1–47 (2003)
13. 13.
P. Dybjer, A. Setzer, Indexed induction-recursion. J. Logic Algebraic Program. 66, 1–49 (2006)
14. 14.
P. Hancock, C. McBride, N. Ghani, L. Malatesta, T. Altenkirch, Small induction recursion, in Typed Lambda Calculi and Applications, vol. 7941, Lecture Notes in Computer Science, ed. by M. Hasegawa (Springer, 2013), pp. 156–172Google Scholar
15. 15.
P. Hancock, A. Setzer, Interactive programs in dependent type theory, in Computer Science Logic, vol. 1862, Lecture Notes in Computer Science, ed. by P. Clote, H. Schwichtenberg (Springer, 2000), pp. 317–331Google Scholar
16. 16.
P. Hancock, A. Setzer, Specifying interactions with dependent types, in Workshop on Subtyping and Dependent Types in Programming, Portugal, 7 July 2000. Electronic Proceedings. http://www-sop.inria.fr/oasis/DTP00/Proceedings/proceedings.html
17. 17.
P. Hancock, A. Setzer, Interactive programs and weakly final coalgebras (extended version), in Dependently Typed Programming, Number 04381 in Dagstuhl Seminar Proceedings, ed. by T. Altenkirch, M. Hofmann, J. Hughes. Internationales Begegnungs- und Forschungszentrum (IBFI), Schloss Dagstuhl, Germany, 2004. http://drops.dagstuhl.de/opus/volltexte/2005/176/
18. 18.
P. Hancock, A. Setzer, Interactive programs and weakly final coalgebras in dependent type theory, in From Sets and Types to Topology and Analysis, Towards Practicable Foundations for Constructive Mathematics, ed. by L. Crosilla, P. Schuster (Clarendon Press, Oxford, 2005), pp. 115–134
19. 19.
L. Malatesta, T. Altenkirch, N. Ghani, P. Hancock, C. McBride, Small induction recursion, indexed containers and dependent polynomials are equivalent. Submitted for publication (2012). http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.366.3934&rep=rep1&type=pdf
20. 20.
R. Milner, Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25(3), 267–310 (1983)
21. 21.
P. Morris, T. Altenkirch, N. Ghani, Constructing strictly positive families, in Proceedings of the Thirteenth Australasian Symposium on Theory of Computing, CATS’07, vol. 65, Darlinghurst, Australia (Australian Computer Society Inc, Australia, 2007), pp. 111–121Google Scholar
22. 22.
D. Park, Concurrency and automata on infinite sequences, in Theoretical Computer Science, vol. 104, Lecture Notes in Computer Science, ed. by P. Deussen (Springer, Berlin, Heidelberg, 1981), pp. 167–183
23. 23.
K. Petersson, D. Synek, A set constructor for inductive sets in Martin-Löf’s Type Theory, in Category Theory and Computer Science, vol. 389, Lecture Notes in Computer Science, ed. by D.H. Pitt, D.E. Rydeheard, P. Dybjer, A.M. Pitts, A. Poigné (Springer, London, UK, 1989), pp. 128–140
24. 24.
J. Rutten, Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3–80 (2000)
25. 25.
D. Sangiorgi, Introduction to Bisimulation and Coinduction (Cambridge University Press, Cambridge, 2011)Google Scholar
26. 26.
D. Sangiorgi, J. Rutten, Advanced Topics in Bisimulation and Coinduction, vol. 52 (Cambridge University Press, Cambridge, 2011)Google Scholar
27. 27.
A. Setzer, Coalgebras as types determined by their elimination rules, in Epistemology versus Ontology, vol. 27, Logic, Epistemology, and the Unity of Science, ed. by P. Dybjer, S. Lindström, E. Palmgren, G. Sundholm (Springer, Netherlands, 2012), pp. 351–369. doi: Google Scholar
28. 28.
A. Setzer, A. Abel, B. Pientka, D. Thibodeau. Unnesting of copatterns, in Rewriting and Typed Lambda Calculi. Proceedings RTA-TLCA 2014, vol. 8560, Lecture Notes in Computer Science, ed. by G. Dowek (Springer, 2014), pp. 31–45Google Scholar