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.
Dedicated to Gerhard Jäger on occasion of his 60th Birthday
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Notes
- 1.
This holds only in indexed inductive-definitions; in indexed inductive-recursive definitions arguments can depend on \(\mathrm {T}\) applied to previous inductive arguments.
- 2.
Note that we deviate from standard category theory in so far as we fix the function \(\mathrm {tree}\): \(\mathrm {tree}\) is the curried version of the constructor, which we introduced before. In standard category theory both the set \(\mathrm {Tree}\) and the function \(\mathrm {tree}\) can be arbitrary, and therefore the initial algebra is only unique up to isomorphism. Note as well that above we had the convention that we identify \(\mathrm {tree}\) with its uncurried form \(\widehat{\mathrm {tree}}\). Without this convention one would say that \((\mathrm {Tree},\widehat{\mathrm {tree}})\) is an \(\mathrm {F}\)-algebra.
- 3.
Here \(\mathrm {F}\) is as above, i.e. strictly positive.
- 4.
Again \(\mathrm {tree}\) is the curried version of the constructor defined before.
- 5.
Note that in contrast to other sections, \(\mathrm {tree}\) can be an arbitrary function of this type, and \(\mathrm {Tree}\) is assumed just to be an element of \(\mathrm {Set}^\mathrm {I}\).
References
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–196
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–38
P. Aczel, Non-wellfounded Set Theory, vol. 14, CSLI Lecture Notes (Stanford University, Center for the Study of Language and Information, Stanford, CA, 1988)
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–88
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:10.1007/BFb0018361
T. Altenkirch, P. Morris, Indexed containers, in 24th Annual IEEE Symposium on Logic in Computer Science, 2009. LICS’09, pp. 277–285 (2009)
M. Barr, Terminal coalgebras in well-founded set theory. Theor. Comput. Sci. 114(2), 299–315 (1993)
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/
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–306
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–146
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–113
P. Dybjer, A. Setzer, Induction-recursion and initial algebras. Ann. Pure Appl. Logic 124, 1–47 (2003)
P. Dybjer, A. Setzer, Indexed induction-recursion. J. Logic Algebraic Program. 66, 1–49 (2006)
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–172
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–331
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
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/
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
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
R. Milner, Calculi for synchrony and asynchrony. Theor. Comput. Sci. 25(3), 267–310 (1983)
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–121
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
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
J. Rutten, Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3–80 (2000)
D. Sangiorgi, Introduction to Bisimulation and Coinduction (Cambridge University Press, Cambridge, 2011)
D. Sangiorgi, J. Rutten, Advanced Topics in Bisimulation and Coinduction, vol. 52 (Cambridge University Press, Cambridge, 2011)
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:10.1007/978-94-007-4435-6_16
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–45
Acknowledgments
The author wants to thank the anonymous referee for valuable comments which greatly have improved this article. The diagrams in this article were typeset using the diagrams package by Paul Taylor.
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2016 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Setzer, A. (2016). How to Reason Coinductively Informally. In: Kahle, R., Strahm, T., Studer, T. (eds) Advances in Proof Theory. Progress in Computer Science and Applied Logic, vol 28. Birkhäuser, Cham. https://doi.org/10.1007/978-3-319-29198-7_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-29198-7_12
Published:
Publisher Name: Birkhäuser, Cham
Print ISBN: 978-3-319-29196-3
Online ISBN: 978-3-319-29198-7
eBook Packages: Mathematics and StatisticsMathematics and Statistics (R0)