Abstract
Final coalgebras for a functor serve as semantic domains for state based systems of various types. For example, formal languages, streams, non-well-founded sets and behaviors of CCS processes form final coalgebras. We present a uniform account of the semantics of recursive definitions in final coalgebras by combining two ideas: (1) final coalgebras are also initial completely iterative algebras (cia); (2) additional algebraic operations on final coalgebras may be presented in terms of a distributive law λ. We first show that a distributive law leads to new extended cia structures on the final coalgebra. Then we formalize recursive function definitions involving operations given by λ as recursive program schemes for λ, and we prove that unique solutions exist in the extended cias. We illustrate our results by the four concrete final coalgebras mentioned above, e. g., a finite stream circuit defines a unique stream function and we show how to define new process combinators from given ones by sos rules involving recursion.
In this extended abstract all proofs are omitted. They can be found in the full version of our paper at www.stefan-milius.eu.
Chapter PDF
Similar content being viewed by others
References
Aceto, L., Fokking, W., Verhoef, C.: Structural Operational Semantics. In: Handbook of Process Algebra. Elsevier, Amsterdam (2001)
Aczel, P.: Non-Well-Founded Sets. CLSI Lecture Notes, vol. 14. CLSI Publications, Stanford (1988)
Aczel, P., Adámek, J., Milius, S., Velebil, J.: Infinite trees and completely iterative theories: A coalgebraic view. Theoret. Comput. Sci. 300, 1–45 (2003)
Adámek, J.: Free algebras and automata realizations in the language of categories. Comment. Math. Univ. Carolin. 15, 589–602 (1974)
Adámek, J.: Introduction to coalgebra. Theory Appl. Categ. 14, 157–199 (2005)
Adámek, J., Milius, S., Velebil, J.: On coalgebras based on classes. Theoret. Comput. Sci. 316, 3–23 (2004)
Adámek, J., Milius, S., Velebil, J.: Elgot algebras. Log. Methods Comput. Sci. 2(5:4), 31 (2006)
Bartels, F.: Generalized coinduction. Math. Structures Comput. Sci. 13(2), 321–348 (2003)
Bartels, F.: On generalized coinduction and probabilistic specification formats. PhD thesis, Vrije Universiteit Amsterdam (2004)
Barwise, J., Moss, L.S.: Vicious circles. CLSI Publications, Stanford (1996)
Capretta, V., Uustalu, T., Vene, V.: Recursive coalgebras from comonads. Inform. and Comput. 204, 437–468 (2006)
Jacobs, B.: A bialgebraic review of deterministic automata, regular expressions and languages. In: Futatsugi, K., Jouannaud, J.-P., Meseguer, J. (eds.) Algebra, Meaning, and Computation. LNCS, vol. 4060, pp. 375–404. Springer, Heidelberg (2006)
Jacobs, B.: Distributive laws for the coinductive solution of recursive equations. Inform. and Comput. 204(4), 561–587 (2006)
Lambek, J.: A fixpoint theorem for complete categories. Math. Z. 103, 151–161 (1968)
Lenisa, M., Power, A.J., Watanabe, H.: Distributivity for endofunctors, pointed and co-pointed endofunctors, monads and comonads. In: Reichel, H. (ed.) Proc. Coalgebraic Methods in Computer Science. Electron. Notes Theor. Comput. Sci., vol. 33. Elsevier, Amsterdam (2000)
Lenisa, M., Power, A.J., Watanabe, H.: Category theory for operational semantics. Theoret. Comput. Sci. 327, 135–154 (2004)
MacLane, S.: Categories for the working mathematician, 2nd edn. Springer, Heidelberg (1998)
Milius, S.: Completely iterative algebras and completely iterative monads. Inform. and Comput. 196, 1–41 (2005)
Milius, S., Moss, L.S.: The category theoretic solution of recursive program schemes. Theoret. Comput. Sci. 366, 3–59 (2006) (fundamental study)
Milius, S., Moss, L.S.: Equational properties of recursive program scheme solutions. Cah. Topol. Gèom. Diffèr. Catèg. 50, 23–66 (2009)
Milner, R.: Communication and Concurrency. International Series in Computer Science. Prentice Hall, Englewood Cliffs (1989)
Plotkin, G.D., Turi, D.: Towards a mathematical operational semantics. In: Proc. Logic in Computer Science, LICS (1997)
Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theoret. Comput. Sci. 249(1), 3–80 (2000)
Rutten, J.J.M.M.: A coinductive calculus of streams. Math. Structures Comput. Sci. 15(1), 93–147 (2005)
Schwencke, D.: Coequational logic for accessible functors. Accepted for publication in Inform. and Comput. (2009)
Uustalu, T., Vene, V., Pardo, A.: Recursion schemes from comonads. Nordic J. Comput. 8(3), 366–390 (2001)
Worrell, J.: On the final sequence of a finitary set functor. Theoret. Comput. Sci. 338, 184–199 (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Milius, S., Moss, L.S., Schwencke, D. (2010). CIA Structures and the Semantics of Recursion. In: Ong, L. (eds) Foundations of Software Science and Computational Structures. FoSSaCS 2010. Lecture Notes in Computer Science, vol 6014. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-12032-9_22
Download citation
DOI: https://doi.org/10.1007/978-3-642-12032-9_22
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-12031-2
Online ISBN: 978-3-642-12032-9
eBook Packages: Computer ScienceComputer Science (R0)Springer Nature Proceedings Computer Science