Abstract
The Structural Induction Theorem (Lehmann and Smyth, 1981; Plotkin, 1981) characterizes initial F-algebras of locally continuous functors F on the category of cpo's with strict and continuous maps. Here a dual of that theorem is presented, giving a number of equivalent characterizations of final coalgebras of such functors. In particular, final coalgebras are order strongly-extensional (sometimes called internal full abstractness): the order is the union of all (ordered) F-bisimulations. (Since the initial fixed point for locally continuous functors is also final, both theorems apply.) Further, a similar co-induction theorem is given for a category of complete metric spaces and locally contracting functors.
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
S. Abramsky. A Cook's tour of the finitary non-well-founded sets. Department of Computing, Imperial College, London, 1988.
S. Abramsky. A domain equation for bisimulation. Information and Computation, 92:161–218, 1991.
P. Aczel. Non-well-founded sets. Number 14 in CSLI Lecture Notes. Stanford University, 1988.
P. Aczel and N. Mendler. A final coalgebra theorem. In D.H. Pitt, D.E. Ryeheard, P. Dybjer, A.M. Pitts, and A. Poigné, editors, Proceedings Category Theory and Computer Science, volume 389 of Lecture Notes in Computer Science, pages 357–365, 1989.
P. America and J.J.M.M. Rutten. Solving reflexive domain equations in a category of complete metric spaces. Journal of Computer and System Sciences, 39(3):343–375, 1989.
R. Engelking. General Topology, volume 6 of Sigma Series in Pure Mathematics. Heldermann Verlag, Berlin, revised and completed edition, 1989.
M. Forti and F. Honsell. Set theory with free construction principles. Annali Scuola Normale Superiore, Pisa, X(3):493–522, 1983.
M. Forti and F. Honsell. A general construction of hyperuniverses. Technical Report 1992/9, Istituto di Matematiche Applicate ‘U. Dini', Facoltà di Ingegneria, Università di Pisa, 1992.
M. Fiore. A coinduction principle for recursive data types based on bisimulation. In Proceedings of the Eighth IEEE Symposium on Logic In Computer Science, 1993.
S. Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer-Verlag, 1971.
D. Lehmann and A. Pasztor. Epis need not to be dense. Theoretical Computer Science, 17:151–161, 1982.
D. Lehmann and M.B. Smyth. Algebraic specifications of data types: a synthetic approach. Mathematical Systems Theory, 14:97–139, 1981.
R. Milner. Communication and Concurrency. Prentice Hall, 1989.
M.W. Mislove, L.S. Moss, and F.J. Oles. Non-well-founded sets obtained from ideal fixed points. In Proc. of the Fourth IEEE Symposium on Logic in Computer Science, pages 263–272, 1989. To appear in Information and Computation.
R. Milner and M. Tofte. Co-induction in relational semantics. Theoretical Computer Science, 87:209–220, 1991.
D.M.R. Park. Concurrency and automata on infinite sequences. In P. Deussen, editor, Proceedings 5th GI Conference, volume 104 of Lecture Notes in Computer Science, pages 167–183. Springer-Verlag, 1981.
A.M. Pitts. A co-induction principle for recursively defined domains. Technical Report 252, Computer Laboratory, University of Cambridge, 1992.
A.M. Pitts. Relational properties of recursively defined domains. In Proceedings 8th Annual Symposium on Logic in Computer Science, pages 86–97. IEEE Computer Society Press, 1993.
G.D. Plotkin. Post-graduate lecture notes in advanced domain theory (incorporating the “Pisa Notes”). Department of Computer Science, University of Edinburgh, 1981.
G.D. Plotkin. Some notes on recursive domain equations. Handwritten notes for the Domain Theory PG Course. University of Edinburgh, 1991.
J.J.M.M. Rutten and D. Turi. On the foundations of final semantics: Non-standard sets, metric spaces, partial orders. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors, Proceedings of the REX workshop on Semantics: Foundations and Applications, volume 666 of Lecture Notes in Computer Science, pages 477–530. Springer-Verlag, 1993.
J.J.M.M. Rutten. Hereditarily-finite sets and complete metric spaces. Technical Report CS-R9148, Centre for Mathematics and Computer Science, Amsterdam, 1991.
M.B. Smyth. I-categories and duality. In M.P. Fourman, P.T. Johnstone, and A.M. Pitts, editors, Applications of categories in computer science, volume 177 of London Mathematical Society Lecture Note Series, pages 270–287. Cambridge University Press, 1992.
M.B. Smyth and G.D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM J. Comput., 11:761–783, 1982.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1994 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Rutten, J. (1994). A structural co-induction theorem. In: Brookes, S., Main, M., Melton, A., Mislove, M., Schmidt, D. (eds) Mathematical Foundations of Programming Semantics. MFPS 1993. Lecture Notes in Computer Science, vol 802. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-58027-1_4
Download citation
DOI: https://doi.org/10.1007/3-540-58027-1_4
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-58027-0
Online ISBN: 978-3-540-48419-6
eBook Packages: Springer Book Archive